10

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

有没有更好的使用方法->，如果没有，是否值得作为功能请求提出？

4

2 回答 2

10

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

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

于 2014-12-03T12:29:54.477 回答
1

该Data.Morphisms模块提供了类似的东西，除了您必须围绕Morphism“newtype”进行所有包装/展开。

于 2016-12-26T22:34:52.553 回答