Контрактные типы

Контрактные типы (также контракты или гибридные типы) - ослабленная версия статических типов. В отличие от последних, контракты не гарантируют выполнение типового инварианта на протяжении всей работы программы. Нарушениями инварианта занимается алгебра вины (англ. blame calculus): система правил, по которым ошибка изолируются в определенной части программы.

Контрактные типы занимают промежуточное положение между динамической и статической типизацией. Введение их связано с избыточной сложностью языков со строгой нетривиальной типизацией (Haskell, Coq, Agda). За использование контрактов выступает известный компьютерный теоретик Бенджамин Пирс.

Языки

• Sage
• Thorn