问题标签 [dependent-type]

我最近发现，类型孔与证明上的模式匹配相结合在 Haskell 中提供了非常好的类似 Agda 的体验。例如：

真正好的事情是我可以用类型孔替换结构的右侧Refl -> exp，并且我的孔目标类型会随着证明进行更新，就像使用rewriteAgda 中的表单一样。

但是，有时该孔无法更新：

此外，即使目标类型不一定在证明中排列，如果我从 Agda 粘贴整个内容，它仍然可以正常检查：

你有什么想法为什么会发生这种情况（或者我如何以一种健壮的方式进行证明重写）？

出于我邪恶且大多难以理解的原因，我决定想要一个类型级别的函数来指示类型的类型类实例的存在。它会像这样工作：

考虑到最近添加到 GHC 的约束类型等，我觉得这可能是可能的，但没有想到任何整洁的实现。可以做到吗？

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

我正在考虑两种方法

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

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

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

这是一个诚实的问题，而不是一个巨魔。我在请求你的耐心。

当Cedric 谈到依赖类型时，他说的好处是在编译时检查列表长度：

包含一个元素的列表将是类型错误，因此上面代码段中的第二行不应该编译。

当Ana Bove 和 Peter Dybjer 谈论依赖类型时，他们说的好处是在编译时检查列表长度：

依赖类型是依赖于其他类型元素的类型。一个例子是长度为 n 的向量类型 An，其分量类型为 A。另一个例子是 m n 矩阵的类型 Amn。我们说类型 An 取决于数 n，或者说 An 是由数 n 索引的类型族。

更大的一点是，由于在编译时提供了额外的信息和检查，我们对程序的正确性有了额外的保证。

现在我的经验是人们（来自 Haskell 背景）对 Lisp 嗤之以鼻，因为它是一种“动态语言”。它们的来源是它看起来不健全，因为它与丰富的 Haskell 类型系统相比如何。（我不反对他们——我认为这很有趣）。

关键是他们声称Haskell（或 Agda 等）在编译时有额外的信息，而 Lisp 这样的动态语言不可用。（我将使用 Lisp 作为“语言家族”并假设 Clojure 是一个 Lisp）。

现在我可以在 Clojure 中执行以下操作来在编译时检查数组的长度：

现在这将失败，因为我期待一个长度为 3 的向量，但底层向量的长度为 2。我在编译时得到了这个信息。

现在我似乎从“动态语言”中获得了依赖类型的好处。

我的问题是是否有可能在 Lisp 中使用宏来实现依赖类型的好处？

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

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

在 Ulf Norell 的论文中，他提到 Agda 是基于 Luo 的 UTT。但是，我找不到在那里使用 Prop 的方法。有什么办法吗？

我只能以相当笨拙的方式在 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的 .

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

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

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

我正在尝试通过实现一个简单的纸牌游戏来编写更多静态类型安全的代码。在这个游戏中，有几张独特的牌，每张牌都有一个特定于牌的效果，可能需要额外的参数（例如，效果的目标）。一名玩家持有两张牌，轮到他们选择打出其中一张，导致该牌的效果发生。

注意：这篇文章中的大部分细节都来自于在 REPL 中的尝试。我编写了一个静态类型安全性较低的实现，但我想在完全深入研究之前确保我想要的东西是可行的。

以下是一些相关定义：

我想将选择使用哪张牌的任务委托给某个策略，这样我就可以看到不同策略的比较。这就是我卡住的地方：我想将您可以返回的卡片限制为Hand参数中传递的对象中的卡片，我可以通过将其键入为hand.CardInHand：

但我还想传递额外的参数：例如，一张牌可能允许我只针对一名玩家（例如，跳过他们的回合），但另一张牌可能让我针对两名玩家（例如，交换他们的牌）。这些由 建模CardEffectParams。所以我想同时返回我要返回hand.CardsInHand的实例cardInHand.card.Params在哪里，如下所示：cardInHand

所以第一个问题是，这能做到吗？你会如何表达这种关系？

我还坚持如何实例化子CardEffectParams类，因为每个子类可能有不同的参数列表。我的第一个想法是进行模式匹配，但这失败了，因为匹配块的类型是所有可能结果的共同祖先：

我目前的想法是在每个卡片对象中定义一个工厂方法，该方法接受一个参数列表，从中生成正确的类型：

然后我可以从中执行以下操作？

但我觉得我在兔子洞里走得太远了。我想要实现的目标可能吗？有必要吗？我是否需要深入研究打字以确保静态类型安全，还是我错过了一些非常基本的东西？