Nor*_*sey 11
Joe Wells表明类型推断对于系统F来说是不可判定的,这是Girard和Reynolds独立发现的最基本的多态lambda演算.这是显示类型推断极限的最重要结果.
这是一个仍然存在的重要问题:将广义代数数据类型集成到Hindley-Milner类型推理中的最佳方法是什么？Simon Peyton Jones每年都会提出一个新的答案,据说比前一年的答案更好.我还没看过2009年3月的版本,所以不能说我相信它会是明确的.
值依赖类型系统(或简称依赖类型系统)可以描述类似以下内容的类型:"在评估时(运行时),此变量的值将始终等于该变量的值,即用不同的评估过程计算".从代码中自动推导出这种类型需要自动定理证明.如果您可以表达的定理集仅限于那些可自动证明的定理,那么这不是问题,但在依赖类型语言的情况下,通常不是这种情况.
因此,依赖类型的系统不能具有一般(和完整)类型推断.
我相信有人可以提供道德正式和完整的答案......
| 归档时间： |
|
| 查看次数： |
1380 次 |
| 最近记录： |