如果不知道如何解释,在计算机里能看到的也就是一些0和1.一项数据(datum)就是一个0和1的有穷序列.一个值类型(valuetype)是一个(抽象或具体)类别和一集数据之间的一个对应关系.对应于某特定实体的数据称为该实体的一个表示(representation);而这一实体称为相应数据的解释(interpretation).我们把一项数据和它的解释称为一个值(value).值的例子如采用大尾格式的32位二进制补码表示的整数;或者用连续的两个32位二进制序列表示的有理数,这两个二进制序列分别被解释为用整数表示的分子和分母,而这两个整数又用大尾格式的32位二进制补码表示.一项数据相对于一个值类型是良形式的(well-formed),当且仅当这一数据表示了该类型里的一个抽象实体.例如,每个32位的二进制序列解释为模二补码的整数时都是良形式的;而IEEE754浮点的一个NaN(NotaNumber,不是数)解释为实数就不是良形式的.一个值类型是真部分的(properlypartial),如果它的值只能表示对应抽象类别里的所有抽象实体的一个真子集;否则它就是全的(total).举例说,类型int 1.2 值是真部分的,而类型bool 是全的.一个值类型是唯一表示的(uniquelyrepresented),当且仅当每个抽象实体至多有一个对应的值.例如,如果表示真值的类型使用了一个字节,其中的0解释为假,而其他情况都解释为真,那么这个类型就不是唯一表示的.如果一个类型把整数表示为一个符号位和一个无符号量,它就不能为0提供唯一表示.用模二补码表示整数的类型是唯一表示的.一个值类型是有歧义的(ambiguous),当且仅在当该类型里存在具有多种解释的值.有歧义的否定是无歧义(unambiguous).例如,将长于一个世纪的纪年表示为两个十进制数的类型就是有歧义的.一个值类型里的两个值相等(equality),当且仅当它们表示的是同一个抽象实体.说两个值是表示相等的(representationalequality),当且仅当它们的数据是两个相同的0/1序列.引理1.1如果一个值类型具有唯一表示,相等就蕴涵着表示相等.引理1.2如果一个值类型无歧义,表示相等就蕴涵着相等.如果一个值类型是唯一表示的,通过检查其0/1序列是否相同的方式就可以实现相等判断.否则就必须以一种与该类型的解释协调的方式来实现相等判断.如果对于一个值类型经常需要生成新值而较少检查相等,那就可以考虑选用非唯一性的表示,因为这样做有可能使新值的生成更快,而使相等判断较慢.这类的例子如,用一对整数表示的两个有理数相等,条件是它们可以约简到同一个最简分数.再如用非排序序列表示的两个集合相等,条件是经过排序并消除重复元素后,它们的对应元素相等.有些时候,实现真正的行为上的(behavioral)相等判断的代价过大甚至根本就不可能.例如,将可计算函数编码为一个类型时的情况就是这样.在这种情况下,我们只能接受弱得多的表示相等的概念,简单判断两个值的0/1序列是否相等.计算机把抽象实体上的函数实现(implement)为值上的函数(function).虽然这些值驻留在内存,但一个完好实现的值上的函数并不依赖于特定的内存地址,它实现的是一个从值到值的映射(mapping).在一个值类型上定义的一个函数是规范的(regular),当且仅当它遵从相等性:给它的某个参数换一个相等的值,它一定还得出相等的结果.大多数的数简单地表示为一对整数,而该函数简单返回表示分子的那个整数.例如21 =
42,
但numerator(1 2)=numerator(2 4).
规范函数使我们可以做等式推理(equationalreasoning), 允许我们做等值替换. 非规范的函数依赖于其参数的具体表示,而不仅仅是参数的解释.在设计一个值类型的表示时,有两项相关的工作必须处理:实现相等判断,确定哪些函数应该是规范的.
