0

问题：

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

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

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

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

例子：

我用一个参数定义了一些方法，它要么是"nothing"，要么与整数范围匹配[0..100]。

这种方法将接受以下值：

"nothing"
0
1
...
100

我希望，我可以说清楚自己。

4

3 回答 3

2

你可以看看像Haskell甚至Agda这样的语言。此外，奥列格有很多很棒的资源。

于 2009-11-27T20:55:02.290 回答
1

这不是我的专业领域，所以它可能跑题了，但微软研究院有一个项目Code Contracts，它“提供了一种与语言无关的方式来表达 .NET 程序中的编码假设。合同采用前置条件、后置条件的形式, 和对象不变量”。

于 2009-11-27T21:04:30.087 回答
1

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

考虑这个例子：

(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 编译器为操作数的类型量身定制更高效的代码，但上面的示例更简洁地编写运行时类型检查。

于 2009-11-27T21:46:28.163 回答