Is there a nice way to use `->` directly as a function in Idris?
dependent-type, idris
Solution
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.
Problem
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?