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