Хорошая информация о системах типов, основанных на контрактах / ограничениях?

Question

Проблема:

Я ищу хорошее введение о системы типов, которые основаны на контракты/ограничения
(извините, я не помню, какой термин подходит для системы типов).

Мне нужна эта информация, чтобы иметь возможность реализовать систему экспериментального типа такого рода.

Насколько я знаю, такая система типов используется в XSD (Определение Xml-схемы).

Вместо определения типа данных задаются ограничения на набор возможных значений.

Пример:

Я определяю некоторый метод с параметром, который является либо "nothing", или соответствует целому диапазону [0..100].

Такой метод принимал бы следующие значения:

"nothing"
0
1
...
100

Я надеюсь, что смог бы прояснить ситуацию.

Answer 1

Common Lisp предлагает такое тестирование типов по адресу время выполнения.Он имеет сложную систему типов, но она используется не так, как вы могли бы привыкнуть в статически типизированном языке.Макрос check-type принимает спецификация типа, которая может быть встроенной спецификацией или определяемой макрокомандой deftype.Ограничения, выражаемые с помощью typespecs, являются ограничениями функции-предиката, написанной на языке хоста, то есть все, что вы можете проверить во время выполнения, может быть критерием того, что представляет собой ваш новый тип.

Рассмотрим этот пример:

(defun is-nothing (val)
  (when (stringp val)
    (string= val "nothing")))

(deftype strange-range ()
  "A number between 0 and 100 inclusive, or the string \"nothing\"."
  '(or (integer 0 100)
       (satisfies is-nothing)))

Это определяет тип, называемый "strange-range".Теперь протестируйте с ним несколько значений:

CL-USER> (let ((n 0))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 100))
           (check-type n strange-range))
NIL
CL-USER> (let ((n "nothing"))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 101))
           (check-type n strange-range))

Последний запускает отладчик со следующим сообщением:

The value of N should be of type STRANGE-RANGE.
The value is: 101
   [Condition of type SIMPLE-TYPE-ERROR]

Этот случай провоцирует тот же результат:

CL-USER> (let ((n "something"))
           (check-type n strange-range))

Ограничения, которые можно наложить таким образом, выразительны, но они не служат той же цели, что сложные системы типов в таких языках, как Haskell или Scala.В то время как определения типов могут побудить компилятор Common Lisp выдавать код, более адаптированный к типам операндов и эффективный для них, приведенные выше примеры представляют собой более краткий способ написания проверок типов во время выполнения.

Answer 2

Вы можете ознакомиться с такими языками, как Хаскелл, или даже Agda.Также, Олег обладает множеством отличных ресурсов.

Answer 3

Это не моя область знаний, так что, возможно, это не по теме, но у Microsoft Research есть проект Кодовые контракты, которые "предоставляют независимый от языка способ выражения предположений о кодировании в программах .NET.Контракты принимают форму предварительных условий, постусловий и объектных инвариантов".