但是我的问题是关于数据的依赖类型,而不是程序,我们如何或可以将它们用于结构化数据验证？
意思就像json或xml或任何种类的结构化数据,是否可以使用一些依赖型系统有效地验证它们？
编辑：
我的意思是依赖类型,它是最广泛的定义“依赖于一个价值的类型”,而不是那些定理证明者和CoC的工作人员.我不认识他们,我不想走那条路,我不相信那些唯一也没有’最终’的方法来得到体面的依赖类型.在FP中,编码人员以非常优雅,建设性的方式,每天都以自己的最复杂的逻辑写出最复杂的逻辑,所有的简单性都没有问题.我相信他们会有最终的“优雅”依赖打字.
然而,我的问题是关于纯数据,不像代码当大量的检查只是不必要的,并且可以隐藏在程序流和逻辑,即使动态打字也可以正常工作.在数据中,当您要检查一些文档的正确性并给出明确的错误消息时,情况并非如此.另一方面,当您必须处理非常极端的依赖型系统(CoC系列)中的“功能”时,数据没有复杂性问题.
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的静态结构(您可能需要依赖类型才能执行此操作,因为复杂性很容易地转化为这样的进化而不是设计格式),但是这只是很少使用没有人关心它,使用它,理解它,更重要的是保持它.
(关于你的trollish介绍的二级阵容：请前往ATS,Guru或Agda,这是相当实用的程序设计,如果你想去弗兰肯斯坦的路线,也有SHE; Coq不是设计为“实用的软件开发”,但已知以这种方式被滥用 – 我不会建议它为依赖类型的编程,但它是不利于非常依赖的编程加上伴随的正确性证明 – 如果你想卖你的灵魂也是F*即将推出)
