Хорошая информация о системах типов на основе контрактов / ограничений? - PullRequest
Новая
       36

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

0 голосов
/ 13 ноября 2009

Проблема:

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

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

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

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

Пример:

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

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

"nothing"
0
1
...
100

Надеюсь, я мог бы прояснить себя.

Ответы [ 3 ]

2 голосов
/ 27 ноября 2009

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

1 голос
/ 28 ноября 2009

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

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

(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)))

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

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 выдавать код, более адаптированный и эффективный для типов операндов, приведенные выше примеры являются более кратким способом написания проверок типов во время выполнения.

1 голос
/ 28 ноября 2009

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

...