我正在尝试在 Scala 中定义一个通用的残留类环。残基类环由某个基环（例如整数）和模数（例如二）定义，该模数是来自基环的值。环及其元素都是对象，因此模数的类型通常是依赖类型，具体取决于基环。我知道这在 Scala 中是不允许的（有充分的理由），所以我试图通过近似类型并在构造残基类环时进行运行时检查来模拟它。

的定义ResidueClassRing被接受而没有错误，但是，Scala 不允许我实例化它，因为two我收到错误消息的参数

难道我做错了什么？这可能是 Scala 类型检查器中的错误吗？有没有更好的定义方式ResidueClassRing？

这是用于 Helios 的 Eclipse IDE 中的 Scala 2.8.0。2.7.x 已经出现该问题。这是代码的简化版本：

哪些依赖类型的编程语言可用于现实世界的应用程序开发？

这些是我认为很重要的几点：

• 文件
• 示例程序
• 一个标准库
• 或者至少一个易于使用的外部函数接口
• 使用该语言完成现实世界任务的社区
• 工具支持

我在 Coq 中玩耍，试图创建一个排序列表。我只想要一个接受列表[1,2,3,2,4]并返回类似内容的函数Sorted [1,2,3,4]- 即取出坏部分，但实际上并未对整个列表进行排序。

我想我会先定义一个lesseqtype的函数(m n : nat) -> option (m <= n)，然后我可以很容易地对其进行模式匹配。也许这是个坏主意。

我现在遇到的问题的症结在于（片段，底部的整个功能）

不是类型检查；它说它期待一个option (m <= n)，但它Some (le_n 0)有 type option (0 <= 0)。我不明白，因为在这种情况下显然两者m和n都是零，但我不知道如何告诉 Coq。

整个功能是：

也许我正在超越自己，只需要在解决这个问题之前继续阅读。

我试图在 Scala 中获得最小形式的依赖类型。如果我有

我可以

现在有可能x从它的单例中恢复x.type吗？

或者，如果这不可能，是否可以以某种方式将稳定标识符与类型相关联，然后提取它？

首先，我真的不知道依赖类型有什么问题以及为什么我们没有看到它们在现有语言中实现以进行实际编程，而不是发明各种技巧（模式！）来绕过当前类型系统的限制充其量只有非常简单和有限的概括。

但我的问题是关于数据的依赖类型而不是程序，我们如何或可以将它们用于结构化数据验证？意思是，像 json 或 xml 或任何类型的结构化数据，是否可以使用某些依赖类型系统有效地验证它们？

编辑：

我的意思是依赖类型是最广泛的定义“依赖于值的类型”，而不是那些定理证明者和 CoC 人员。我不认识他们，我不想走那条路，我不相信那些获得体面依赖类型的唯一或“终极”方式。在 FP 中，编码人员每天都以非常优雅、建设性的方式编写他们最复杂的逻辑，并且非常简单且完全没有问题。我相信他们将拥有最终的“优雅”依赖类型。

但是，我的问题是关于纯数据的，与代码不同，很多检查可能只是不必要的，并且可以隐藏在程序流和逻辑中，即使是动态类型也可以这样工作。在数据中，当您想要检查某些文档的正确性并给出明确的错误消息时，情况并非如此。另一方面，当您必须处理非常依赖的类型系统（CoC 系列）中的“功能”时，数据不存在复杂性问题。

例如，我想做一种MyType整数三元组。但不仅仅是三个整数的笛卡尔积，我希望类型代表所有 (x, y, z) 使得x + y + z = 5.

我怎么做？除了使用 just (x, y)since z = 5 - x - y。

如果我有三个构造函数A, B, C并且类型应该都是(A x, B y, C z)这样的，那么同样的问题x + y + z = 5。

阅读完 ghc 7.4. pre-release notes 和Giving Haskell a Promotion论文，我仍然对你实际上对提升类型做了什么感到困惑。例如，GHC 手册给出了关于提升数据类型的以下示例：

这些有什么样的用途？你能给出（代码）例子吗？

我试图回答我自己关于在 GHC 中使用 PolyKinds 扩展的示例的问题，并提出了一个更具体的问题。我正在尝试对一个由两个列表构建的队列进行建模，头列表dequeue从中获取元素，尾列表enqueue将它们放置在其中。为了让这件事变得有趣，我决定添加一个约束，即尾部列表不能长于头部列表。

enqueue如果队列是否应该平衡，似乎必须返回不同的类型。是否有可能为enqueue具有此约束的函数提供正确的类型？

我目前拥有的代码在这里：

辅助类型级别列表和 nat 定义如下。

有人可以向我解释依赖类型吗？我在 Haskell、Cayenne、Epigram 或其他函数式语言方面几乎没有经验，所以您使用的术语越简单，我就越会感激它！

我在这里有一个设计模式，其中有一个对象生成器（MorselGenerator 及其子代），其任何实例总是生成相同类型的对象（Morsels 及其子代），但类型检查器不会让我执行任何操作这些生成的对象中的两个或多个，相信它们可能不同。

我如何通过类型检查器？

编译器生成以下编译错误

更新

这是或多或少等同于我正在尝试做的 C++ 代码。请注意，eatTwo 函数是完全多态的，并且不引用 Morsel 或 MorselGenerator 的特定派生类型。