Testing if a type is a function type in Idris

Question

I want to have a function that determines if a type is a function type, like this:

isFunction : Type -> Bool
isFunction (a -> b) = True
isFunction _ = False

This returns True for all inputs, however. How can I make this work?

Answer 1

Matching on a Type is known as type-casing. Being able to do this would break a concept called parametricity which is very valuable.

https://stackoverflow.com/a/23224110/108359

Idris does not support type-casing. I think it may have tried at one stage, but people gave up on that quickly. It also used to give errors when type-casing was attempted but the check caused bugs and so has been disabled for now.

While you don't get errors any more, you can't provide an implementation of Type -> Bool which will work differently to const True or const False.

So sorry, this function is not possible. It might sound like a limitation but every time I thought I had a motivation for a function similar to this, I eventually figured out that I could have structured my program in a more explicit way instead.

Answer 2

The question here would be: Why do you need something like this?

Do you need to find out if any arbitrary Idris type is a function or not? Or do you just need to find this out from a specific subset of Idris types? I can't figure out possible applications for the 1st one, but if it's the 2nd one you need, then you could define your own embedded language for dealing with values with these types, like this:

data Ty = TyNat | TyString | TyFun Ty Ty | ...

isFunction : Ty -> Bool
isFunction (TyFun _ _) = True
isFunction _ = False

Check out this talk for more information about how to implement these kind of embedded languages: https://vimeo.com/61663317