Existe uma boa maneira de usar `->` diretamente como uma função no Idris?
Pode-se retornar um tipo em uma função em Idris, por exemplo
t : Type -> Type -> Type
t a b = a -> b
Mas surgiu a situação (ao experimentar escrever alguns analisadores) que eu queria usar->
dobrar uma lista de tipos, ou seja,
typeFold : List Type -> Type
typeFold = foldr1 (->)
De modo atypeFold [String, Int]
dariaString -> Int : Type
. Isso não compila:
error: no implicit arguments allowed
here, expected: ")",
dependent type signature,
expression, name
typeFold = foldr1 (->)
^
Mas isso funciona bem:
t : Type -> Type -> Type
t a b = a -> b
typeFold : List Type -> Type
typeFold = foldr1 t
Existe uma maneira melhor de trabalhar com->
, e se não, vale a pena aumentar como uma solicitação de recurso?