KA1*_*KA1 12 ocaml haskell type-systems functional-programming dependent-type
首先,我真的不知道依赖类型有什么问题,为什么我们看不到用现有语言实现实际编程,而不是发明所有类型的技巧(模式!)来绕过当前类型系统的限制这至多具有非常简单和有限的概括.
但我的问题是关于数据的依赖类型而不是程序,我们如何或可以将它们用于结构化数据验证？像json或xml或任何类型的结构化数据这样的含义是否可以使用某些依赖类型系统有效地验证它们？
编辑:
我的意思是依赖类型,它是最宽泛的定义"依赖于一个值的类型",而不是那些定理证明者和CoC工作人员.我不知道他们,我不想走那条路,我不相信那些唯一的或"最终"的方式来获得体面的依赖类型.在FP中,编码人员每天以非常优雅,建设性的方式编写他们最复杂的逻辑,简单而且完全没有问题.我相信他们将拥有他们最终的"优雅"依赖打字.
但是,我的问题是关于纯数据,不像在代码中很多检查可能是不必要的,并且只能隐藏在程序流和逻辑中,甚至动态类型也可以正常工作.在数据中,当您想要检查某些文档的正确性并给出明确的错误消息时,情况并非如此.另一方面,当你必须在极端依赖型系统(CoC系列)中处理"功能"时,数据没有复杂性问题.
gas*_*che 14
您可能会对本文感兴趣: 下一页700数据描述语言(PDF),Kathleen Fisher,Yitzhak Mandelbaum和David Walker,2006.
本文的主要目标是开始理解ad hoc数据处理语言系列.正如兰丁所做的那样,我们通过开发一个语义框架来定义,比较和对比我们领域的语言.该语义框架围绕数据描述演算(DDC ^α)的定义.此演算使用来自依赖类型理论的类型来描述各种形式的即席数据:用于描述原子数据的基本类型和用于描述更丰富结构的类型构造函数.我们展示了如何通过将类型解释为将外部表示(位)映射到类型化lambda演算中的数据结构的解析函数来向DDC ^α提供指称语义.更确切地说,这些解析器产生外部数据的内部表示和解析原始源中的错误的解析描述符.
简而言之:是的,如果要静态编码关于数据的细粒度不变量,则必须使用依赖类型.它们比代数数据类型和GADT更具表现力,它们还允许表达它们和相关结构(例如无标记联合和标记产品的组合),能够以某种方式呈现数据描述的汇编语言,甚至如果面向用户的规范不直接暴露术语依赖项.
但请注意,这种正式的方法是以更陡峭的学习曲线和更高的前期复杂性为代价的,即使理论上它还可以用更简单,更安全,更好的规范,操作工具等来回报.该领域的从业者往往会忽略所有那种类型的系统美,并依赖于不明确的替代品.由于指定模式很无聊而且人们看不到它们带来什么好处,因此XML正在失去JSON.是的,您可以稍后指定所采用的JSON API的静态结构(并且您可能需要依赖类型来执行此操作,因为复杂性很容易进入这样的演化 - 而不是设计格式),但这只是很少用没有人关心它,使用它,理解它,更重要的是,维护它.
(关于你的推特介绍的次要方面:请继续前进并与ATS,Guru或Agda一起玩,它们是用于相对实用的编程.如果你想去frankenstein路线,还有SHE ; Coq不是设计成的"对于软件开发很实用"但是已经知道这种方式被滥用了 - 我不建议它依赖于类型编程,但它对于非依赖性编程加上伴随的正确性证明是好的 - 如果你想卖掉你的灵魂也有F*即将到来.)