文件名称：ditto:超级卡哇伊依存类型编程语言
文件大小：56KB
文件格式：ZIP
更新时间：2024-05-21 18:02:37
programming-language dependent-types proof-assistant type-theory Haskell
同上 同上是一种超级卡哇伊相关类型的编程语言。 由于其小巧而直接的实现以及可爱的语法，因此它是超级卡哇伊（）：) 利用其简单的实现，我们将Ditto用作试验类型系统功能的工具。 尽管实现简单，但Ditto是支持简洁程序的高级语言，而是需要冗长编码的核心语言。 放在一起，这些东西使Ditto成为研究的好语言。 当面对一个简单的绩效决定时，我们倾向于选择前者。 目前，我们关注的是类型检查代码，而不是运行代码。 特征 打开类型的世界。 相关模式匹配。 搜索所有可能的覆盖物。 增强的“包罗万象”条款（新颖）。 隐式参数。 米勒模式统一。 约束推迟。 相互定义。 职能。 归纳递归。 感应感应。 功能的平等性。 通过命令行界面进行交互。 Kong。 区分大小写。 跟踪用户与机器引入的变量。 缺少功能 宇宙层次结构（当前类型：类型） 终止检查器 阳性检查器 发展 确
【文件预览】：
ditto-master
----.travis.yml(713B)
----package.yaml(890B)
----editor()
--------emacs()
----stack.yaml(50B)
----tests()
--------fail()
--------pass()
----LICENSE(34KB)
----src()
--------test()
--------Ditto()
--------main()
----.gitignore(183B)
----README.md(2KB)