haskell - 结构化数据验证的依赖类型

Question

首先，我真的不知道依赖类型有什么问题，也不知道为什么我们没有看到它们在现有语言中实现用于实际编程，而不是发明各种技巧(模式!)来绕过当前类型系统的局限性，充其量只是非常简单且有限的泛化。

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

编辑:

我所说的依赖类型是指最广泛的定义“依赖于值的类型”，而不需要那些定理证明者和 CoC 工作人员。我不认识他们，我不想走那条路，我不相信这些是获得体面的依赖类型的唯一或“最终”方法。在 FP 中，程序员每天都以非常优雅、有建设性的方式编写最复杂的逻辑，而且非常简单，没有任何问题。我相信他们将拥有最终的“优雅”依赖打字。

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

Answer 1

您可能会对这篇论文感兴趣: The Next 700 Data Description Languages (PDF) ，凯瑟琳·费舍尔、伊扎克·曼德尔鲍姆和大卫·沃克，2006 年。

The primary goal of this paper is to begin to understand the family of ad hoc data processing languages. We do so, as Landin did, by developing a semantic framework for defining, comparing, and contrasting languages in our domain. This semantic framework revolves around the definition of a data description calculus (DDC^α). This calculus uses types from a dependent type theory to describe various forms of ad hoc data: base types to describe atomic pieces of data and type constructors to describe richer structures. We show how to give a denotational semantics to DDC^α by interpreting types as parsing functions that map external representations (bits) to data structures in a typed lambda calculus. More precisely, these parsers produce both internal representations of the external data and parse descriptors that pinpoint errors in the original source.

简而言之:是的，如果您想对数据的细粒度不变量进行静态编码，则依赖类型是必要的。它们比代数数据类型和 GADT 更具表现力，还允许表达它们和相关结构(例如未标记联合和标记乘积的组合)，在某种意义上能够成为数据描述的汇编语言，甚至如果面向用户的规范不直接公开术语依赖关系。

然而，请注意，这种正式的方法是以更陡峭的学习曲线和更高的前期复杂性为代价的，即使理论上它会以更简单、更安全、更好的规范、操作工具等来返回。该领域的从业者常常会忽视所有类型系统的美感，而求助于不明确的替代方案。 XML 正在输给 JSON，还有其他原因，因为指定模式很无聊，而且人们看不到它们带来的优势。是的，您可以稍后指定所采用的 JSON API 的静态结构(并且您很可能需要依赖类型来执行此操作，因为复杂性很容易渗透到这种演变而不是设计的格式中)，但这在以下情况下没有什么用处:没有人关心它、使用它、理解它，更重要的是，维护它。

(关于你的恶搞介绍的第二个方面:请继续玩 ATS 、 Guru 或 Agda ，它们是为了相对实用的编程而设计的。如果你想走弗兰肯斯坦路线，有另外 SHE ; Coq 的设计初衷并不是“适用于软件开发”，但众所周知，这种方式会被滥用——我不建议将其用于依赖类型编程，但它很好对于不太依赖的编程加上附带的正确性证明——如果你想出卖你的灵魂，还有 F* 即将推出。)