问题标签 [idris]

我本着这篇文章的精神实现了依赖类型的 lambda 演算：http ://www.andres-loeh.de/LambdaPi/LambdaPi.pdf 演算，有效，我用它做了实验，并扩展了几件事：许多宇宙，硬编码归纳公理。但是，我想添加归纳类型来做更复杂的事情。

我正在考虑两种方法

• 介绍 Fin-N、Product 和 W-类型，并用它们表示归纳类型。
• 生成归纳和递归公理。

这两种方式我都不喜欢。第一个太低级，需要大量的努力才能从高级语言转换为核心语言。第二种方式工作量很大，而且容易出错，因为复杂归纳类型的递归原理的生成有很多极端情况，即正/负出现。

如何做到这一点？这些类型如何在 Coq、Agda 和 Idris 等现有系统中实现？

在 Idris 中将 String 转换为 Integer 或 Natural的最佳方法是什么？

我知道标准库仍在进行中，所以如果答案是我应该将它添加到标准库中，那很好，我会尝试这样做，但在我想我会确认没有办法之前。

如果我想从用户那里读取索引，我能想到的最好的方法是：

但是这样，我没有从 cast 中得到失败的迹象。不仅 indexAsString 的格式可能不允许将其转换为 Integer，而且最重要的是，它甚至不会在运行时失败，由于 "bad cast" 而产生 0。

请告诉我有更好的方法和/或指出我正确的方向。

附带说明一下，Idris 中没有 Read 类型类是否有特殊原因？还是只是还没有进入？

提前谢谢。

据我了解，几乎所有依赖类型的语言都使用弱头范式进行转换。为什么会这样？为什么检查可兑换性就足够了（对我来说似乎还不够）？你有什么推荐阅读的？

在依赖类型理论中有一个相等类型。通常在定义这种类型时，会引入一些实用程序，即 cong 和 subst。它们的表现力如何？是否有可能用消除器表达我们所能表达的一切以与他们平等？

我只能以相当笨拙的方式在 Idris 0.9.12 中进行 rank-n 类型：

只要有类型应用程序，我就需要下划线，因为当我尝试将（嵌套）类型参数设为隐式时，Idris 会引发解析错误：

一个可能更大的问题是我根本无法在更高级别的类型中进行类约束。我无法将以下 Haskell 函数转换为 Idris：

这也阻止了我使用 Idris 函数作为类型的同义词，例如HaskellLens中Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t的 .

有什么办法可以补救或规避上述问题？

如果我理解正确（主要是从applyTactic函数的存在），可以为 Idris 中的定理证明器编写自定义策略。我可以使用哪些（或在哪里）示例来学习如何做到这一点？

在这里，作者提出了主张：

将 TLS 规范形式化并证明实现与它一致仅表明该实现在逻辑上是正确的。但是，它并不表明实现是安全的。您的实现可能容易受到旁道攻击（特别是定时攻击），同时仍然在逻辑上是正确的。

我的问题是：如果使用“安全语言”（即 Haskell、Idris）或使用定理证明器（Coq、Agda）进行了验证的 SSL/TLS 实现，它仍然容易受到 heartbleed 攻击吗？

在Haskell中，我可能会if这样实现：

这符合我的预期：

在Racket中，我可以实现这样的缺陷if：

这符合我的预期：

在Idris中，我可能会if这样实现：

这种行为让我感到惊讶：

我希望 Irdis 表现得像 Racket，两个参数都被评估。但事实并非如此！

伊德里斯如何决定何时评估事物？

∀ a b ∈ ℕ, b ≠ 0 → ∃ ! q r ∈ ℕ, a = q × b + r ∧ r < b是使用依赖类型的标准示例。如何扩展这种类型，使其也表达时间和空间复杂性要求？

阿格达和伊德里斯_有效地禁止对 type 值进行模式匹配Type。似乎 Agda 总是在第一种情况下匹配，而 Idris 只是抛出一个错误。

那么，为什么 typecase 是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的太多信息。