-
0 votesanswersviews
在Idris中使用间接相互递归数据类型进行总体检查
我正在使用抽象语法树，我想给 Binders 提供他们自己的类型 . 这似乎给伊德里斯的整体检查带来了问题...... 有一个典型的自我参照 Tree 伊德里斯完全检查完成 . data TreeShape = Last | More TreeShape TreeShape Show TreeShape where show Last = "Leaf" show (M... -
1 votesanswersviews
证明函数的总体最多需要n个递归调用
假设我们正在编写lambda演算的实现，作为其中的一部分，我们希望能够选择一个新的非冲突名称： record Ctx where constructor MkCtx bindings : List String emptyCtx : Ctx emptyCtx = MkCtx [] addCtx : String -> Ctx -> Ctx addCtx name = rec... -
24 votesanswersviews
什么是智能合约的合适类型？
我想知道在Haskell或Idris等类型语言中表达智能合约的最佳方式是什么（例如，您可以将其编译为在以太坊网络上运行） . 我主要担心的是：哪种类型可以捕获 Contract 可以执行的所有操作？ 天真的解决方案：EthIO 一个天真的解决方案是将 Contract 定义为 EthIO 类型的成员 . 这种类型就像Haskell的 IO ，但它不是启用系统调用，而是包括区块链调用，即它可以读取和... -
10 votesanswersviews
Haskell式的家庭
在Haskell中，我可能会编写一个带有 type 声明的类型类来创建一个类型族，如下所示： class ListLike k where type Elem :: * -> * fromList :: [Elem k] -> k 然后写这样的实例： instance ListLike [a] where type Elem [a] = a from... -
10 votesanswersviews
为什么伊德里斯需要相互的？
为什么Idris要求函数按照其定义的顺序出现，并使用 mutual 声明相互递归？ 我希望Idris能够在函数之间执行第一次依赖性分析，并自动重新排序 . 我一直相信Haskell会这样做 . 为什么在伊德里斯这不可能？ -
1 votesanswersviews
在编译时和运行时使用数字的最佳方法是什么？
我刚刚开始学习Idris，我认为一个很好的小项目开始将实现有限序列作为2-3个手指树 . 树中的每个内部节点都需要在运行时进行注释，并在其下面存储元素的总数，以便支持快速拆分和索引 . 此大小信息也需要在编译时进行管理，以便（最终）证明使用适当的索引进行拆分并使用另一个序列压缩序列是总操作 . 我可以想到两种方法来解决这个问题： 我目前正在做的事情，编写了必要代码总数的一小部分：完全处理类型中... -
3 votesanswersviews
为什么这个相互递归的数据定义不完整，我该如何解决？
我最近正在尝试使用Idris，并提出了以下“类型级别定义”： mutual data Set : Type -> Type where Empty : Set a Insert : (x : a) -> (xs : Set a) -> Not (Elem x xs) -> Set a data Elem : (x : a) -> Set a ... -
0 votesanswersviews
这个递归函数不是完全的，还是编译器无法证明它？如何将其重写为总计？
出现以下代码时： module TotalityOrWhat %default total data Instruction = Jump Nat | Return Char | Error parse : List Char -> Instruction parse ('j' :: '1' :: _) = Jump 1 parse ('j' :: '2' :: _) = Jump 2... -
7 votesanswersviews
如果伊德里斯认为事情可能完全没有，那么伊德里斯可以用于证明吗？
http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出： 其次，到目前为止，目前的实施工作投入有限，因此可能仍然存在这样的情况：它认为功能是总的而不是 . 不要依赖它来证明你的证明！ 这是否意味着不能依赖Idris作为证据，或者有没有办法创建不需要整体检查的证明？ -
1 votesanswersviews
如何在计算日期时正确处理Fin n和Integer？
在我探索伊德里斯的旅程中，我试图以“惯用”的方式编写一个小日期处理模块 . 这是我到目前为止所拥有的 . 首先，我有一些基本类型来表示日，月和年： module Date import Data.Fin Day : Type Day = Fin 32 data Month : Type where January : Month February : Month ..... -
2 votesanswersviews
Idris：尝试从Intete for Nat重新实现整体检查失败
我有以下代码： module Test data Nat' = S' Nat' | Z' Num Nat' where x * y = ?hole x + y = ?hole fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1)) 我收到有关最后一行的错误消息： Test.idr:6:5:... -
1 votesanswersviews
如何在Idris中定义非泛型递归数据类型？
这实际上是我的第一行Idris代码 . 当我查阅文档时，所有内容都显示正确： Idris> data T = Foo Bool | Bar (T -> T) (input):1:6: | 1 | data T = Foo Bool | Bar (T -> T) | ^ unexpected reserved data expecting dependent ty... -
4 votesanswersviews
伊德里斯Gcd的总体定义
我正在一个小项目中工作，其目标是给出Gcd的定义，它给出了两个数字的gcd以及结果正确的证明 . 但我无法给出Gcd的完整定义 . Idris 1.3.0中Gcd的定义是完全的，但是使用assert_total来强制总体性，这违背了我的项目的目的 . 有人有Gcd的总定义，不使用assert_total吗？ 附： - 我的代码在https://github.com/anotherArka/Idr...