An exercise in dependent types: A well-typed interpreter
An exercise in dependent types: A well-typed interpreter
复制标题
依赖类型的练习：类型良好的解释器
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Carlsson
中科院分区：
文献类型：
--
作者：
L. Augustsson;M. Carlsson
用类型化语言编写的解释器的结果类型通常是标记联合。通过使用依赖类型，我们可以更精确地了解解释器返回的值的类型。不需要用它们的类型来标记这些值，这为更高效的解释器打开了大门。 1 一个我们忽略的恼人问题？目前。为可以产生不同类型结果的语言编写解释器需要对结果进行某种编码，如图 1 所示。编码在数据类型 Value 的标记中捕获。这种标记效率低下，因为每个返回值都必须被标记。此外，标签在使用时必须经过测试并再次提取真实值。 interp :: Expr-> Value interp (EBool b) = VBool b interp (EInt i) = VInt i interp (EAdd e1 e2) = case (interp e1, interp e2) of (VInt i1, VInt i2)-> VInt (i1+i2) _-> VError 图 1. 一种非常简单的语言及其解释器。这些标签有两个目的：第一，它们将结果转换为联合类型，以便结果是单一类型；第二，它们将结果转换为联合类型，以便结果是单一类型。其次，它们用于确保
The result type of an interpreter written in a typed language is normally a tagged union. By using depent types, we can be more precise about the type of values that the intepreter returns. There is no need for tagging these values with their type, something which opens the door to more eecient interpreters. 1 An annoying problem We are ignoring ? for now. Writing an interpreter for a language which can produce results of diierent types requires some kind of encoding of the result, as in gure 1. The encoding is captured in the tagging in the data type Value. This tagging is ineecient since each return value must be tagged. In addition, the tags must be tested and the real values extracted again when they are used. interp :: Expr-> Value interp (EBool b) = VBool b interp (EInt i) = VInt i interp (EAdd e1 e2) = case (interp e1, interp e2) of (VInt i1, VInt i2)-> VInt (i1+i2) _-> VError Fig. 1. A very simple language and its interpreter. The tags serve two purposes: rst, they turn the result into a union type so that the result is a single type; second, they are used to make sure that the