我从“残酷的 Agda 简介” http://oxij.org/note/BrutalDepTypes/

假设我们想在偶数上定义除以二。我们可以这样做：

N是自然数，偶数是以下“命题”

当你评估表达式 div (succ (succ zero)) 你得到 \p -> succ zero 这就是你所期望的。但是，我不明白的是如何解释 \p. 我也不明白代码 f : \bot -> N f = div (succ zero) 是什么意思。我知道 \bot 对任何 A 都意味着 A ...因此类型是有效的。我想我认为依赖类型将允许我以这样的方式编写 div，即 div (succ zero) 会更明确地失败类型检查。

任何人都可以就如何在 agda 中使用和查看谓词提出建议吗？

我最近问了这个问题： 类型中使用的 agda 命题——这是什么意思？ 并收到了关于如何使类型隐式并获得真正的编译时错误的深思熟虑的答案。

但是，我仍然不清楚如何创建具有依赖类型的值。

考虑：

其中N是自然数，偶数是下面的命题。

假设我想写一个函数如下：

我不知道如何以我想要的方式做这样的事情......在我看来，最好的办法是证明（不是（甚至 n））\甚至（成功 n）。我真的不知道如何在 agda 中表达这一点。我能写

由此，我可以做如下事情：

并评估为正常形式......以获得答案。如果我想写 f，我可以这样做

我得到 fn = gn { }1 { }2 其中 ?1 = 偶数 n，而 ?2 = 偶数 (succ n)。然后我可以做 f 5 之类的事情并评估为正常形式。我真的不明白为什么这是有效的......有没有办法告诉agda更多关于f以这种方式定义的信息。我可以确定如果 ?1 失败 ?2 会成功，那么告诉 agda 评估 f 总是有意义的吗？

我将 g 解释为一个函数，它接受一个数字 n，一个 n 是偶数的证明，一个 (succ n) 是偶数的证明，并返回一个数字。（这是阅读本文的正确方法吗？或者有人可以提出更好的阅读方法吗？）我真的很想准确（或更准确地）理解上述类型的检查方式。它是否使用感应 - 它是否将 (evenB n) 与 p 连接：甚至 n？等等。我现在很困惑，因为它知道

不正确。首先我明白为什么 - q 代表 succ n，所以它不匹配。但是第二次失败了，而且原因更加神秘，而且似乎阿格达比我想象的还要强大……

如果我能弄清楚该怎么做（如果有意义的话），这是我非常喜欢的第一步。

其中奇数 p 证明如果偶数 n 是荒谬的，那么 succ n 是偶数。我想，这将要求我能够使用依赖类型的值。

最终，我希望能够写出这样的东西：

或类似的规定。甚至

我真的很想知道如何制作与依赖类型相对应的证明，以便我可以在程序中使用它。有什么建议么？

我已经看到在最新版本的 GHC 中支持类型级列表。但是，我需要为应用程序使用类型级别集，并且希望实现基于类型级别列表的类型级别集库。但我不知道从哪里开始:(

Haskell 中是否有任何支持类型级别集的库？

我对依赖类型的语言感兴趣。有限数字对我来说似乎非常有用。例如，安全地索引固定大小的数组。但是这个定义对我来说不是很清楚。

Idris 中有限数的数据类型如下：（在 Agda 中可能类似）

它似乎有效：

但这是如何工作的？k 是什么意思？为什么类型检查器接受第一个实现而拒绝第二个实现？

是否有一种类型化的编程语言，我可以像以下两个示例一样约束类型？

1. 概率是一个浮点数，最小值为 0.0，最大值为 1.0。

   /li>

2. 离散概率分布是一个映射，其中：键都应该是相同的类型，值都是概率，并且值的总和 = 1.0。

   /li>

据我了解，这对于 Haskell 或 Agda 是不可能的。

假设我想用常数 c、一元函数符号 f 和谓词 P 表示一阶语言的有限模型。我可以将载体表示为列表m，常数表示为 的元素m，函数表示为有序列表的元素对m（可以通过辅助函数应用ap），谓词作为m满足它的元素的列表：

然后我可以在模型上构建特定的模型和操作。细节对我的问题并不重要，只是类型（但我已经包含了定义，因此您可以看到类型约束的来源）：

现在，我想为所有这些模型命名：

最后，我想编写这段代码，将每个名称映射到它命名的模型：

在定义类型的意义上，我尝试了多种方法来使其工作，以便我可以准确地使用 model_of 的这个定义，包括使用幻像类型、GADT 和类型系列——但还没有找到一种方法去做吧。（但话又说回来，我是 Haskell 的新手。）可以做到吗？我该怎么做？

我定义了一个简单的结构：

CS_wf基于这两个参数，在构造时强制执行语义格式良好的属性。现在稍后，我需要比较两条记录是否相等——我用证明组件做什么？

我从以下内容开始---我猜这两个良构也应该出现在 lhs 上？

这需要我：

我想证明无关性也起作用了？

从我收集到的关于 agda 的点点滴滴的信息中，我（显然是错误地）得出结论，这∀ {A}相当于{A : Set}. 现在我注意到了

是无效的（关于 Set\omega 的东西又似乎是一些内部的东西，但是

很好。谁能帮我解决这个问题？

我将这个n-ary 补充概括为n-ary compose，但我在使界面变得漂亮时遇到了麻烦。也就是说，我不知道如何在类型级别使用数字文字，同时仍然能够对后继进行模式匹配。

滚动我自己的 nats

使用 roll-my-own nats，我可以使n-ary compose 工作，但我只能n作为迭代后继者传递，而不是作为文字传递：

使用GHC.TypeLits.Nat

使用GHC.TypeLits.Nat，我得到了类型级别的 nat 文字，但是我找不到后继构造函数，并且使用 type 函数(1 +)不起作用，因为 GHC (7.6.3) 无法推断类型函数的注入性：

我同意语义编辑器组合器(.) . (.) . ...在这里更优雅、更通用——具体来说，写( times)总是很容易n而不是compose (Proxy::Proxy n)——但我很沮丧我不能让n-ary 组合工作和我预期的一样。此外，对于 的其他用途，我似乎会遇到类似的问题GHC.TypeLits.Nat，例如在尝试定义类型函数时：

更新：接受答案的总结和改编

在接受的答案中有很多有趣的东西，但对我来说关键是 GHC 7.6 解决方案中的 Template Haskell 技巧：它有效地让我将类型级文字添加到我的 GHC 7.6.3 版本中，它已经具有单射性继任者。

使用上面的类型，我通过 TH 定义文字：

我将Nat声明移到新模块中以避免导入循环。然后我修改我的RollMyOwnNats模块：

我们已经看到Martin Odersky 宣布 了 Dotty Compiler - 一个可能的未来 Scala 编译器，没有所有的包袱。

我们还看到 Nada Amin 发布了已在 Scala 中实现的Dependent Object Types Calculus (Dot Calculus) 。

我的问题是：Scala Dotty 编译器和 Nada Amin 的 Dependent Objects 项目之间是否存在关系？