关于基于契约/约束的类型系统的好信息？

Question

问题：

我正在寻找有关类型系统的良好介绍， 基于合同/约束
（抱歉，我不记得哪个术语适合类型系统）。

我需要这些信息才能实现此类实验类型系统。

据我所知，这种类型系统用于XSD（Xml Schema Definition）。

我们不是定义数据类型，而是定义一组可能值的约束。

示例：

我定义了一些带有参数的方法，该参数要么是“nothing”，要么与整数范围[0..100]匹配。

这样的方法将接受以下值：

"nothing"
0
1
...
100

我希望，我可以清楚地表达自己。

Answer 1

您可以查看 Haskell 等语言，甚至 Agda。此外，Oleg 有很多很棒的资源。

Answer 2

Common Lisp 在运行时提供此类类型测试。它有一个复杂的类型系统，但它的使用方式与您在静态类型语言中可能习惯的方式不同。宏 check-type 接受typespec，可以是内置的-in 规范或由宏定义的 deftype< /a>.使用类型规范表达的约束是用宿主语言编写的谓词函数的约束，也就是说，您可以在运行时检查的任何内容都可以作为构成新类型的标准。

考虑这个例子：

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

这不是我的专业领域，因此可能偏离主题，但 Microsoft Research 有一个项目代码契约，“提供了一种与语言无关的方式来表达 .NET 程序中的编码假设。契约采用前置条件、后置条件和对象不变量的形式”。