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?
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 oft
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.