问题标签 [dependent-type]

异构列表是 ghc 7.6 的新依赖类型工具的示例之一：

示例列表“li”编译良好：

显然我们希望 HList 在 Show 类中，但我只能提出以下使用相互递归约束（超类）的工作类实例：

代码编译良好，li 显示正确。需要的编译标志是：

我尝试了以下更直接定义的许多变体，但如果我无法理解 ghc 错误消息，它就无法编译：

一些 Haskell / ghc 专家可能会理解为什么这不起作用，我很乐意听到原因。

谢谢

汉斯·彼得

谢谢你，hammar，你的两个很好的工作示例，改进了我的第一个示例。

但我仍然不明白为什么我的第二个例子不起作用。您说“... show' 只知道如何显示当前元素类型，而不知道如何显示其余元素类型。” 但是该评论是否也不适用于以下（工作）代码：

So I have a situation very similar to this (much simplified) code:

How can I use Haskell's type system (or GHC extensions) to restrict before and similar operations from taking Elements from different Containers? I've been looking into GADTs and DataKinds but, well, that's going to take a long while and I could use some suggestions or pointers. (Another idea I've thought of but haven't worked out: use a similar trick as the ST monad's s parameter...)

Am I too pessimistic if I conclude that this would require a dependently typed language? Because, as my limited understanding of dependent typing goes, I think that I'm trying to index the Element type by values of the Container type.

EDIT: Just for extra color, this all ultimately arises because I'm trying to define something very much like this:

All of this code requires that you never "mix" Elements from different Containers.

我编写了一个 Agda 函数applyPrefix，将一个固定大小向量函数应用于向量大小为的较长向量的初始部分m，n并且k 可能保持隐式。这是定义和辅助函数split：

我需要一个对称函数applyPostfix，它将固定大小的向量函数应用于较长向量的尾部。

正如applyPrefix已经表明的定义，k-Argument 在使用时不能保持隐含applyPostfix。例如：

有谁知道一种技术，如何实现applyPostfix以使k- 参数在使用时保持隐式applyPostfix？

我所做的是校对/编程：

并在定义时使用该引理applyPostfix：

不幸的是，这没有帮助，因为我使用k-Parameter 来调用引理:-(

任何更好的想法如何避免k明确？也许我应该在 Vectors 上使用 snoc-View？

有一个 Idris 教程、一个 Agda 教程和许多其他教程风格的论文和介绍性材料，其中不断引用尚未学习的东西。我有点在所有这些中间爬行，而且大多数时候我都被数学符号和突然出现的新术语所困，没有任何解释。也许我的数学很烂:-)

是否有任何规范的方法来处理依赖类型编程？就像当你想学习 Haskell 时，你从“自学 Haskell”开始，当你想学习 Scala 时，你从 Odersky 的书开始，对于 Ruby，你阅读那个带有变异错误的奇怪教程。但我不能从他们的书开始 Agda 或 Idris。他们在我的头上。我尝试了 Coq 并陷入了它的所有关于 teorm 证明的风格。Agda 需要大量的数学背景，而 Idris，好吧，让我们暂时离开吧！

我非常了解静态类型系统，我精通 Scala，如有必要，我可以使用 Haskell。我了解函数范式并每天使用它，我了解代数数据类型和 GADT（实际上非​​常顺利），并且我最近设法理解了 Lambda Cube。不过，我缺乏数学和逻辑部分。

在我对依赖型土地永无止境的奇迹中，一个奇怪的想法出现在我的脑海中。我做了很多数据库编程，如果我能摆脱所有那些健全性检查和有效性检查，那就太好了。一个特别烦人的情况是那些接受 Integer 并期望它是某个特定表的有效行 ID 的函数。一个非常愚蠢的例子是：

假设我选择的语言完全支持依赖类型，是否可以利用类型系统loadStudent只接受有效值studentId：

如果是，我如何为ValidRowId类型编写数据构造函数？到目前为止，我看到的所有示例都是纯的（不涉及 IO）。

我正在尝试为二进制自然数（位列表）定义前置函数。我想将我的函数的输入限制为修剪过的数字（没有前导零）并且是正数（所以，我不必担心零的前身）。

这是运算符的定义pred：

我的第一个义务如下：

但是，我不知道如何解决它。

矛盾显然在H2。但是，因为它取决于H1，所以我不能只rewrite nat1使用Empt，然后(is_pos Empt H1)使用False。

我应该如何证明这一点？

假设我有一个数据类型

这些是半（右）开区间。Nat是标准的归纳自然数，SNat是相应的单例。

现在我想得到一个Nat给定间隔长度的单例：

这不起作用，因为该Plus函数不是单射的。我可能可以像这样定义它

但我猜这需要一些引理（和额外的约束）。此外，我的间隔以前一种形式出现。

背景：我尝试在 Omega 中执行此操作，但没有成功（我提交了 omega 错误）

此外，如何使用修改后的类型检查器来破解这些问题？供应的 RHS 能否对 LHS 模式的类型方程提供关键提示，从而消除非内射性？

Agda 程序员如何解决这些问题？

我被困在一个关于归纳谓词的简单证明上。我必须证明自然 0 不是正数，其中自然是位列表，而 0 是任何只有位为 0 的列表。

Certified Programming with Dependents Types这一章似乎建议我使用inversion，但我收到一条错误消息。

之前，我能够证明forall nat1: Nat, Trim nat1 -> Trim (pred nat1)的以下定义pred。

但是用下面的新定义pred我不知道如何证明forall nat1: {nat2: Nat | Trim nat2 /\ Pos nat2}, Trim (pred nat1)。

有人可以给我一个提示吗？我不知道用sig. 或者，也许我做错了什么。我不知道。完整的代码在这里。之前的代码在这里。

为了让我的问题有意义，我必须提供一些背景信息。

我认为拥有一种依赖类型的语言来推断一个函数的参数的存在和类型是很有用的a，该函数的其他参数和/或返回值的类型依赖于a. 考虑我正在设计的语言中的以下代码段：

如果我们做出两个（诚然，毫无根据的）假设：

1. 必须不存在无法从显式提供的信息中推断出的依赖关系。
2. 每个自由变量都必须转换为使用defor引入的最后一个标识符的隐式参数exs。

我们可以将上面的代码片段解释为等同于以下代码片段：

这或多或少与以下 Agda 代码段相同：

显然，两个毫无根据的假设为我们节省了很多打字时间！

注意：当然，这种机制只有在原始假设成立时才有效。例如，我们无法正确推断出依赖函数组合运算符的隐含参数：

在这种情况下，我们必须明确提供一些附加信息：

可以扩展为以下内容：

这是等效的 Agda 定义，用于比较：

笔记结束

上述机制可行吗？更好的是，是否有任何语言可以实现类似这种机制的东西？