有没有一种很好的方法可以直接使用` - >`作为Idris中的函数？

Question

例如,可以在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

有没有更好的合作方式->,如果不是,值得提出作为功能请求？

Answer 1

->以这种方式使用的问题在于它不是类型构造函数而是绑定器,其中域的绑定名称在范围内,因此->它本身没有直接类型.t例如,您的定义不会捕获依赖类型(x : Nat) -> P x.

虽然它有点繁琐,但你正在做的是正确的方法.我不相信我们应该(->)为类型构造函数创建特殊的语法- 部分原因是因为它实际上不是一个,部分是因为当它不能与依赖类型一起使用时会感觉更加混乱.