问题标签 [idris]

例如：

[]Haskell 中似乎使用了额外的模式，Data.List但那是一种什么样的优化？这里和伊德里斯有什么不同？

我之所以问，是因为我听说“这会使推理变得更加困难”，并且说我的人没有时间充分解释它。

我怀疑我是否能理解它对功能的“减少证明”。

有人可以从 Haskell 和 Idris 的立场向我解释这里额外模式的政治，以便我能够理解并看到差异。

标准库中的natToFin函数具有以下签名：

natToFin 4 5返回Just (FS (FS (FS (FS FZ)))) : Maybe (Fin 5)，而 natToFin 5 5返回Nothing。

我想要一个具有以下签名的函数：

它的行为与标准 lib 函数相同，但不需要返回 aMaybe因为总是可以Fin n从m给定n的大于m.

我该如何实施myNatToFin？

假设我有一个带有这个签名的函数：

我尝试像这样myNatToFin k (S k)在另一个函数的主体中应用它，但出现错误：

所以，我相信我必须明确地通过一个证明GT (S k) k，但我不知道如何做到这一点。如何显式传递隐式证明参数以便编译？

我正在尝试定义 Idris 类型内部的已验证类别，但我的方法不进行类型检查。

ob是对象mor a b的类型，是从a到的态射类型b。仍然会有正确的单位和结合律，但我的定义已经l不起作用了。它说：

我觉得这很混乱。unit a有类型mor a a，f有类型mor a b，为什么没有comp (unit a) f类型mor a b呢？

我正在尝试在 Idris 中编写一个函数，该函数通过传递 Vect 的大小和一个函数以参数中的索引来创建 Vect。到目前为止，我有这个：

但我想确保传入参数的函数只采用小于 Vect 大小的索引。我试过了：

但它不会与错误一起编译

我的问题是：我想做的事情是否可能以及如何做？

我正在尝试实现一个玩具常规类型系统，以确保一些良好的侧向约束并允许在其中展开 mu 绑定。表示这些类型的数据类型包含用于定点 ( ) 的构造函数、由最近的封闭 Mu 绑定项 ( ) 以及零和一个参数类型运算符（分别为和Mu）替换。VarNullaryUnary

为了确保这些类型的格式正确，它们作为三个Bool参数跟踪它们是否具有 aMu作为它们的头构造函数、aVar作为它们的头构造函数，或者它们中的Var任何地方。

为了实现 Mu-headed 类型的展开，我需要执行替换，特别是我需要实现“Mu x. F ====> F[(Mu x. F)/x]”。

除了需要一些来生成第三个类型参数有效的证明之外，该函数subst似乎很简单：

我尝试并未能编写一个稍微清理此返回类型的包装器。

当我尝试解决这个元变量时，我发现它aeq : x = c2 && Delay c2不像aeq : x = c2 && Delay c1我预期的那样（回想一下 ( &&) 在它的第二个参数中是惰性的）。

难道我做错了什么？这是预期的行为吗？FWIW，我成功地为展开（未显示）编写了一个非常相似的包装器。

在 idris 0.9.17.1 中，

受https://wiki.haskell.org/Prime_numbers的启发，我编写了以下代码来生成素数

在 REPL 中，如果我写take 10 primes，REPL 正确显示[2, 3, 5, 11, 13, 17, 19, 29, 31, 37] : List Int

但是如果我尝试:exec，什么也不会发生，如果我尝试编译并执行我得到的程序Segmentation fault: 11

有人可以帮我调试这个问题吗？

是否有一种简单的方法可以DecEq为数据类型编写相等 ( ) 实例？例如，我希望下面的DecEq声明中有 O(n) 行，?p这很简单：

有没有比 :set showimplicits 更有用的信息来追踪统一错误？我目前正在得到这个并且不知道从这里去哪里：

表示自由岩浆（二叉叶树）、自由半群（非空列表）和自由幺半群（列表）很容易，并且不难证明它们实际上就是它们声称的那样。但自由团体似乎要棘手得多。似乎至少有两种使用通常List (Either a)表示的方法：

1. 编码类型的要求，如果你有Left a :: Right b :: ...那么Not (a = b)和反之亦然。构建这些似乎有点困难。
2. 处理允许任意插入/删除对（反之亦然）的等价关系Left a :: Right a :: ...。表达这种关系似乎非常复杂。

还有人有更好的主意吗？

编辑

我刚刚意识到唯一答案使用的选项（1）在最一般的设置中根本无法工作。特别是，如果不施加可判定的相等性，就不可能定义组操作！

编辑 2

我应该首先想到谷歌。看起来 Joachim Breitner几年前在 Agda 做过，从他的介绍性描述来看，他似乎从选项 1 开始，但最终选择了选项 2。我想我会自己尝试，如果我太卡住了我看看他的代码。