Haskell和Idris的区别：运行时/编译时在类型宇宙中的反映
因此，在Idris中编写以下内容是完全有效的。item : (b : Bool) -> if b then Nat else List Nat item True = 42 item False = [1,2,3] // cf. https://www.youtube.com/watc...
在Idris中进行n阶量化
在Idris 0.9.12中，我只能以相当笨拙的方式实现排名n类型： tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b) tupleId f (a, b) = (f _ a, f _ b) 在类型应用的任何位置...
在 Haskell 中，列表是归纳的还是余归纳的？
最近我在阅读有关共归的内容，现在我想知道：Haskell中的列表是归纳的还是共归的？我也听说过Haskell不区分这两者，但如果是这样，他们如何在形式上区分呢？ 列表是归纳定义的，data [a] = [] | a : [a]，但可以用于共归，ones = a:ones。我们可以创建无限的列...
Idris 热心求值
在Haskell中，我可能会这样实现if语句：if。 if' True x y = x if' False x y = y spin 0 = () spin n = spin (n - 1) 这个表现符合我的预期： haskell> if' True (spin 100000...
为什么较新的依赖类型语言没有采用SSReflect的方法？
在Coq的SSReflect扩展中，我发现了两种约定，它们似乎特别有用，但我没有看到它们被广泛采用于新的依赖类型语言（如Lean、Agda、Idris）。首先，尽可能使用返回布尔值的函数来表示谓词，而不是归纳定义数据类型。这默认带来可决定性，为计算证明提供了更多机会，并通过避免证明引擎携带大型...
那么，重点是什么呢？ (关于IT技术的问题)
So类型的预期目的是什么？将其译为Agda：data So : Bool → Set where oh : So true So将布尔命题提升为逻辑命题。Oury和Swierstra的入门论文The Power of Pi给出了一个以表格列索引的关系代数的示例。取两个表格的乘积需要它们拥...
按类型索引与在 Idris 中包含类型的区别
我是一名有用的助手，可以为您翻译文本。 我目前正在学习使用Idris进行类型驱动开发这本书。 我有两个问题与第6章中示例数据存储的设计有关。该数据存储是一个命令行应用程序，允许用户设置存储在其中的数据类型，然后添加新数据。 以下是相关代码的部分内容（稍作简化）。 您可以在Github上查...
为什么GHC Haskell不支持重载记录参数名称？
我所说的是无法定义以下内容： data A = A {name :: String} data B = B {name :: String} 我知道GHC会将其简化为普通函数，解决这个问题的惯用方法是： data A = A {aName :: String} data B = B {...
Idris向量 vs 链表
Idris在向量的底层是否进行任何优化？因为从外表看，Idris向量只是一个已知大小（在编译时已知）的链表。实际上，一般情况下，您可以表示以下等式（我猜测一下语法）： Vector : Nat -> Type -> Type Vector n t = (l: List t ** ...
通過效應進行泛型編程
在 Idris Effects 库中，效应被表示为||| This type is parameterised by: ||| + The return type of the computation. ||| + The input resource. ||| + The computati...