Epigram: Practical Programming with Dependent Types
Epigram: Practical Programming with Dependent Types
复制标题
警句：依赖类型的实用编程
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Conor McBride
中科院分区：
文献类型：
--
作者：
Conor McBride
查找以下Haskell表达式中的类型错误：
如果X为空，则尾部为X，否则为X
当然，你不能：这个程序显然是胡说八道，除非你是一个打字检查员。问题是，如果Null Xs检验为True，则只有某些计算有意义，而如果它为False，则其他计算有意义。然而，就类型系统而言，Then分支的类型是Else分支的类型，而整个条件分支的类型是Then分支的类型。从静态上讲，这项测试无关紧要。这很奇怪，因为如果测试真的无关紧要，我们就不会这么做。当然，Tail[]不会出错--输入良好的程序不会出错--所以我们最好换个词来描述它们的运行方式。
抽象和应用、元组和投影：它们为程序提供了‘软件工程’的上层建筑，我们熟悉的类型系统确保了这些操作的兼容使用。然而，大多数程序迟早会检查数据并做出选择--在这一点上，我们熟悉的类型系统将陷入沉默。他们只是不能谈论具体的数据。一直以来，我们都认为我们的程序是强类型的，而它只是我们的软件工程。为了做得更好，我们需要一种静态语言，能够在使某些计算合法化而不是其他计算合法化时表达特定值的意义。我们不应该放弃编程。
Find the type error in the following Haskell expression:
if null xs then tail xs else xs
You can’t, of course: this program is obviously nonsense unless you’re a typechecker. The trouble is that only certain computations make sense if the null xs test is True, whilst others make sense if it is False. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire conditional. Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn’t do it. Of course, tail [] doesn’t go wrong—well-typed programs don’t go wrong—so we’d better pick a different word for the way they do go.
Abstraction and application, tupling and projection: these provide the ‘software engineering’ superstructure for programs, and our familiar type systems ensure that these operations are used compatibly. However, sooner or later, most programs inspect data and make a choice—at that point our familiar type systems fall silent. They simply can’t talk about specific data. All this time, we thought our programming was strongly typed, when it was just our software engineering. In order to do better, we need a static language capable of expressing the significance of particular values in legitimizing some computations rather than others. We should not give up on programming.