依赖类型 编辑
在计算机科学和逻辑中，依赖类型是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 自动列车停止装置、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。
6
图片 0 图片
评论 0 评论
匿名用户 · [[ show_time(comment.timestamp) ]]
[[ nltobr(comment.content) ]]
相关
F*是一个由微软研究院和法国国家信息与自动化研究所主导开发的、基于ML语言的依赖类型函数式编程程序语言，主要用于程序的形式化验证。
Idris是一个通用的依赖类型纯函数式编程语言，其类型系统与Agda以及Epigram相似。
Agda 是一个依赖类型的纯函数式编程语言。目前的版本，Agda 2，最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年开发，而现今的版本则是对其的彻底重写，因此可视作一个全新的语言，但保留了 Agda 的命名和传统。
在类型论中，LF 逻辑框架提供了定义逻辑的一种方式。它基于了通过有依赖类型的Lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。