问题标签 [idris]

在 Idris/Haskell 中，可以通过注释类型和使用 GADT 构造函数来证明数据的属性，例如使用 Vect，但是，这需要将属性硬编码到类型中（例如，Vect 必须是与 List 不同的类型）。是否可以拥有具有一组开放属性的类型（例如同时带有长度和运行平均值的列表），例如通过重载构造函数或使用 Effect 中的某些东西？

我是依赖类型的新手，并且拥有 Haskell 经验，正在慢慢学习 Idris。对于练习，我想编写一个霍夫曼编码。目前，我正在尝试编写一个证明，证明代码树的“扁平化”会产生前缀代码，但已经被量词卡住了。

我有一个简单的归纳命题，即一个列表是另一个列表的前缀：

1. 这是一种有效的方法吗？或者像“ xs是ys的前缀，如果有zs这样xs ++ zs = ys ”会更好？

2. 引入“forall”量词是否正确（据我所知，在 Agda 中它类似于pNext : ∀ {x xs ys} → Prefix xs ys → Prefix (x :: xs) (y :: ys)）？pNext 第一个参数应该是隐式的吗？两个变体之间的语义差异是什么？

然后，我想为一个向量构建一个，其中没有任何元素构成另一个元素的前缀：

空向量没有前缀：

并给定一个元素 x、一个向量 xs，并证明 xs 的任何元素都不是 x 的前缀（反之亦然），x :: xs 将拥有该属性：

这是一个无效类型，我希望在处理第一个类型后修复它，但是关于 pvNext 中的量词有类似的问题：这个变体是否可以接受，或者有更好的方法来形成“关系否定”？

谢谢你。

我foo在下面的代码中得到了一个未解决的元变量：

如何说服foo没有有效模式可匹配的 Idris？

我试过添加

然后在 Emacs 上进行案例拆分f（只是为了看看可能会出现什么），但这只是删除了这条线，留下foo了一个未解决的元数据。

它们在 Idris 0.9.14 中实现，我成功地用于induction一些证明。但是，它们仅适用于某些库类型；例如，虽然Vect支持它们，但几乎同构All不支持：

不幸的是，没有大量的语言文档，而且我找不到如何为自定义类型实现消除/案例分析。深入研究 Prelude，我找到了%elim修饰符，但没有帮助。有人可以举个例子All吗？

Idris 是否在向量引擎下进行了任何类型的优化？因为从外观上看，Idris 向量只是一个已知大小（在编译时已知）的链表。事实上，一般来说，您似乎可以表达以下等价（我在语法上猜测了一下）：

因此，虽然这在防止范围错误的意义上很好，但向量的真正优势（在该术语的传统用法中）是在性能方面；特别是 O(1) 随机访问。似乎 idris 向量不支持这一点（你将如何编写索引函数来获得这种性能？）。

• 假设引擎盖下没有魔法（就像 发生的那样Nat）来重新配置Vectors，Idris 中是否存在随机访问数据类型？
• 在代数类型系统中如何定义这样的东西？当然，似乎不可能归纳地定义它。
• 在像 Idris 这样的类型系统中，是否有可能创建一个支持 O(1) 随机访问的数据类型，并且知道它的长度以便所有访问都可以证明是有效的？（Haskell 有数组样式的向量，但它们的具体实现对普通用户来说是不透明的，包括我在内）

我想要一个函数来确定一个类型是否是函数类型，如下所示：

但是，这将返回True所有输入。我怎样才能使这项工作？

我正在尝试创建一个函数

我使用以下reflect策略进行了尝试：

但这反映在变量t本身上：

我可以写函数

并简单地证明：

到目前为止，一切都很好。现在，我尝试将这个函数推广到负指数。当然，必须提供逆：

然后我试图证明一个类似的陈述：

但是，Idris 拒绝评估 的应用程序powApplyI，将类型保留?powApplyIZero_rhs为powApplyI (Pos 0) i x = x（是的，Z更改为0）。我试过powApplyI用非无点风格写作，并ZZ用%elim修饰符定义我自己的风格（我不明白），但这些都不起作用。为什么不通过检查第一个案例来处理证明powApplyI？

伊德里斯版本：0.9.15.1

这里有一些事情：

第一个证明很好，但?powApplyZFZero_rhs顽固地保留了 type powApplyZF (Pos 0) f x = x。显然，ZZ（或我对它的使用）存在一些问题。