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

前端之家收集整理的这篇文章主要介绍了依赖类型 – 是否有一个很好的方法来直接使用` – >`作为Idris的函数?前端之家小编觉得挺不错的,现在分享给大家,也给大家做个参考。
例如,可以在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.

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

原文链接:https://www.f2er.com/javaschema/281451.html

猜你在找的设计模式相关文章