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

Question

问题：

我正在寻找关于 类型系统, 这些基于 契约/约束
（抱歉，我不记得哪个术语适合类型系统）.

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

据我所知，这种类型系统用于 XSD （Xml 架构定义）。

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

例子：

我定义了一些带参数的方法，它是 "nothing", ，或匹配积分范围 [0..100].

这种方法将接受以下值：

"nothing"
0
1
...
100

我希望，我能把自己说清楚。

Answer 1

Common Lisp 提供了这样的类型测试： 运行. 。它有一个复杂的类型系统，但它的使用方式与您在静态类型语言中可能习惯的方式不同。宏观 check-type 接受一个 类型规范, ，可以是内置规范或由宏定义的规范 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)))

这定义了一个名为“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

您可以看看像哈斯克尔，甚至的阿格达。此外，奥列格有很多重要的资源。

Answer 3

这是不是我的专业领域，所以它可能是题外话，但微软研究院有一个项目的的代码契约 下，其中‘提供一种语言无关的方式来表达在.NET程序编码的假设。这些合同采取先决条件，后置条件和对象不变量的形式’