Есть ли язык, на котором типы могут учитывать содержимое полей?

Question

У меня была эта сумасшедшая идея, и мне было интересно, существует ли такая вещь:

Обычно в строго типизированном языке типы в основном связаны с разметкой памяти или членством в абстрактном «классе».Так что 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) { //... }

, а компилятор сделает невозможным наличие p.height < 140 в ride.Это просто глупый пример, но я уверен, что есть случаи, когда это действительно может помочь.Есть ли такая вещь?

Answer 1

Это зависит от того, будет ли предикат проверяться статически или динамически. В любом случае ответ - да, но получающиеся системы выглядят по-разному.

На статическом конце: исследователи PL предложили понятие типа уточнения , который состоит из базового типа вместе с предикатом: http://en.wikipedia.org/wiki/Program_refinement. Я считаю, что идея типов уточнения что предикаты проверяются во время компиляции, а это значит, что вы должны ограничить язык предикатов чем-то поддающимся обработке.

Также возможно выразить ограничения, используя зависимые типы , которые являются типами, параметризованными значениями времени выполнения (в отличие от полиморфных типов, которые параметризованы другими типами).

Существуют и другие приемы, которые вы можете использовать с такими мощными системами типов, как Haskell, но IIUC вам придется изменить height с int на нечто, о структуре которого может рассуждать средство проверки типов.

На динамическом конце: в SQL есть нечто, называемое domains , как в CREATE DOMAIN: http://developer.postgresql.org/pgdocs/postgres/sql-createdomain.html (простой пример приведен в нижней части страницы), которое снова состоит из базовый тип и ограничение. Ограничение домена проверяется динамически всякий раз, когда создается значение этого домена. В общем случае вы можете решить эту проблему, создав новый абстрактный тип данных и выполняя проверку всякий раз, когда вы создаете новое значение абстрактного типа. Если ваш язык позволяет вам определять автоматическое приведение от и к вашему новому типу, то вы можете использовать их для реализации SQL-подобных доменов; если нет, то вместо этого вы просто используете простые старые абстрактные типы данных.

Кроме того, существуют контракты, которые не рассматриваются как типы сами по себе, но могут использоваться некоторыми из тех же способов, таких как ограничение аргументов и результатов функций / методов. Простые контракты включают в себя предикаты (например, «принимает объект Person с высотой> 140»), но контракты также могут быть более высокого порядка (например, «принимает объект Person, метод makeSmallTalk () которого никогда не возвращает ноль»). Контракты более высокого порядка не могут быть проверены немедленно, поэтому они обычно включают создание какого-либо прокси. Проверка контракта не создает новый тип значения или не помечает существующие значения, поэтому динамическая проверка будет повторяться при каждом выполнении контракта. Следовательно, программисты часто размещают контракты вдоль границ модулей, чтобы минимизировать избыточные проверки.

Answer 2

Примером языка с такими возможностями является Spec # .Из учебной документации, доступной на сайте проекта:

Рассмотрим метод ISqrt на рис. 1, который вычисляет целочисленный квадратный корень из заданного целого числа 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, которое вы предложили.

Answer 3

Ваша идея звучит несколько как концепции C ++ 0x, но не идентичны. Однако понятия были удалены из стандарта C ++ 0x.

Answer 4

Я не знаю ни одного языка, который бы поддерживал подобные вещи, но я не считаю это действительно необходимым.

Я довольно уверен, что простое применение проверки в установщиках свойств может дать вам все необходимые ограничения.

В вашем примере класса RollercoasterSafe вы можете вызвать исключение, если для свойства высоты установлено значение меньше 140. Это проверка во время выполнения, но полиморфизм может сделать невозможной проверку во время компиляции.