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

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*即将推出)