依赖类型 – 是否有一个很好的方法来直接使用` – `作为Idris的函数？

发布时间：2020-05-24 02:36:13 所属栏目：程序设计来源：互联网

导读：例如,可以在Idris中的函数中返回一个类型 t : Type - Type - Typet a b = a - b 但是,我想要使用的情况出现(在尝试编写一些解析器时) – 折叠类型列表,即 typeFold : List Type - TypetypeFold = foldr1 (-) 所以typeFold [String,Int]会给出String – Int：T

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

有没有更好的工作方式 – >如果不是值得提升作为功能请求？

使用的问题 – >以这种方式,它不是一个类型构造函数,而是一个binder,其中绑定域名的范围在范围内,所以 – >本身没有直接的类型.例如,您对t的定义不会捕获像(x：Nat) – > P x.

虽然有点吝啬,但你在做什么是正确的做法.我不相信我们应该使用( – >)作为类型构造函数的特殊语法 – 部分原因是因为它不是一个,并且部分原因是因为它不会导致更多的混乱,当它不能与依赖类型.

（编辑：安卓应用网）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!