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?

Answer 1

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.

Answer 2

The Data.Morphisms module provides something like this, except you have to do all the wrapping/unwrapping around the Morphism "newtype".