例如,可以在Idris中的函数中返回一个类型
t : Type -> Type -> Type t a b = a -> b
但是,我想要使用的情况出现(在尝试编写一些解析器时) – >折叠类型列表,即
typeFold : List Type -> Type typeFold = foldr1 (->)
所以typeFold [String,Int]会给出String – > Int：Type.虽然如此,
error: no implicit arguments allowed
here,expected: ")",dependent type signature,expression,name
typeFold = foldr1 (->)
^
但这样做很好：
t : Type -> Type -> Type t a b = a -> b typeFold : List Type -> Type typeFold = foldr1 t
有没有更好的工作方式 – >如果不是值得提升作为功能请求？
