Is there a nice way to use `->` directly as a function in Idris?

Question

One can return a type in a function in Idris, for example

t : Type -> Type -> Type
t a b = a -> b

But the situation came up (when experimenting with writing some parsers) that I wanted to use -> to fold a list of types, ie

typeFold : List Type -> Type
typeFold = foldr1 (->)

So that typeFold [String, Int] would give String -> Int : Type. This doesn't compile though:

error: no implicit arguments allowed
    here, expected: ")",
    dependent type signature,
    expression, name
typeFold = foldr1 (->)
                   ^

But this works fine:

t : Type -> Type -> Type
t a b = a -> b

typeFold : List Type -> Type
typeFold = foldr1 t

Is there a better way to work with ->, and if not is it worth raising as a feature request?

Edwin Brady Edwin Brady · Accepted Answer · 2014-12-03T12:29:54

The problem with using -> in this way is that it's not a type constructor but a binder, where the name bound for the domain is in scope in the range, so -> itself doesn't have a type directly. Your definition of t for example wouldn't capture a dependent type like (x : Nat) -> P x.

While it is a bit fiddly, what you're doing is the right way to do this. I'm not convinced we should make special syntax for (->) as a type constructor - partly because it really isn't one, and partly because it feels like it would lead to more confusion when it doesn't work with dependent types.

Is there a nice way to use `->` directly as a function in Idris?

2 Answers