是否有一种语言，其中的类型可以考虑字段的内容？

问题描述

| 我有一个疯狂的想法，想知道是否存在这样的事情： 通常，在强类型语言中，类型主要涉及内存布局或抽象\ class的成员身份。因此，

class Foo {int a;}

和

class Bar {int a; int b;}

是不同的，

class Baz {int a; int b;}

也是如此（尽管它具有相同的布局，但是是不同的类型）。到目前为止，一切都很好。 我想知道是否有一种语言可以让人们指定关于类型的更细粒度的约束。例如，我想拥有：

class Person {
    //...
    int height;
}

class RollercoasterSafe: Person (where .height>140) {}

void ride(RollercoasterSafe p) { //... }

并且编译器将确保不可能在

ride

中包含

p.height < 140

。这只是一个愚蠢的示例，但是我敢肯定，在某些用例中，这确实有帮助。有这样的事吗？     

解决方法

        这取决于谓词是静态还是动态检查。在这两种情况下，答案都是肯定的，但最终的系统看起来有所不同。 在静态方面：PL研究人员提出了一种优化类型的概念，该类型由基本类型和谓词组成：http://en.wikipedia.org/wiki/Program_refinement。我相信精简类型的思想是在编译时检查谓词，这意味着您必须将谓词的语言限制为易于处理的语言。 也可以使用依赖类型来表达约束，这些依赖类型是由运行时值参数化的类型（与多态类型相反，后者是由其他类型参数化的）。 您还可以使用其他类似的技巧来使用功能强大的类型系统（例如Haskell's），但是IIUC必须将

height

从ѭ7change更改为类型检查程序可能会想到的结构。 在动态方面：SQL具有称为域的内容，如ѭ8中所示：http://developer.postgresql.org/pgdocs/postgres/sql-createdomain.html（有关简单示例，请参见页面底部），该域又由以下部分组成：基本类型和约束。每当创建该域的值时，都会动态检查该域的约束。通常，可以通过创建新的抽象数据类型并在创建抽象类型的新值时执行检查来解决该问题。如果您的语言允许您定义新类型之间的自动强制，则可以使用它们本质上实现类似SQL的域；如果没有，您将只使用普通的旧抽象数据类型。 然后是合同，这些合同本身不被认为是类型，但可以以某些相同的方式使用，例如约束参数/函数/方法的结果。简单协定包含谓词（例如\“接受高度> 140 \的Person对象”），但是合同也可以是更高阶的（例如\“接受其makeSmallTalk（）方法从不返回null \”的Person对象）。无法立即检查高阶合同，因此它们通常涉及创建某种代理。合同检查不会创建新的值类型或标记现有值，因此每次执行合同时都会重复进行动态检查。因此，程序员经常沿模块边界放置合同以最大程度地减少冗余检查。     ,        具有这种功能的语言的一个示例是Spec＃。从项目站点上可用的教程文档中：   考虑图1中的ISqrt方法，该方法计算   给定的整数x。仅当x为非负数时才可以实现该方法，因此

int ISqrt(int x) 
  requires 0 <= x; 
  ensures result*result <= x && x < (result+1)*(result+1); 
{ 
  int r = 0; 
  while ((r+1)*(r+1) <= x) 
    invariant r*r <= x; 
  { 
    r++; 
  } 
  return r; 
} 

在您的情况下，您可能会做类似的事情（请注意，我没有尝试过，我只是在阅读文档）：

void ride(Person p)
  requires p.height > 140;
{
  //...
}

可能有一种方法可以将

requires

子句汇总为您建议的类型声明，例如

RollercoasterSafe

。     ,        您的想法听起来有点像C ++ 0x的概念，尽管并不完全相同。但是，概念已从C ++ 0x标准中删除。     ,        我不知道支持这种事情的任何语言，但我认为它确实没有必要。 我非常相信，仅在属性的设置器中应用验证可能会给您所有必要的限制。 在

RollercoasterSafe

类示例中，当height属性的值设置为小于140时，您可能会引发异常。它是运行时检查，但是多态性使编译时检查无法进行。