dependent-type - 有没有一种很好的方法可以将 `->` 直接用作 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

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

虽然有点繁琐，但您正在做的是正确的方法。我不相信我们应该为 (->) 制定特殊语法。作为类型构造函数 - 部分是因为它确实不是一个，部分是因为当它不适用于依赖类型时，它会导致更多的困惑。