当Cedric talks about dependent types,他所说的好处是在编译时检查列表长度：
Having a list with one element would be a type error,so the second line in the snippet above should not compile.
当Ana Bove and Peter Dybjer talk about dependent types,他们说的好处是编译时检查列表长度：
Dependent types are types that depend on elements of other types. An example is
the type An of vectors of length n with components of type A. Another example
is the type Amn of m n-matrices. We say that the type An depends on the
number n,or that An is a family of types indexed by the number n.
更大的一点是,我们对程序的正确性有额外的保证,因为在编译时可以获得更多的信息和检查.
现在我的经验是,人们(从Haskell的背景)冷笑在Lisp,因为它是一种“动态语言”.他们来自哪里是因为它与丰富的Haskell类型系统的比较而看起来不健全. (我没有反对他们 – 我认为这很有趣).
关键是他们声称Haskell(或Agda等)在编译时有其他的信息,不能像Lisp这样的动态语言使用. (我将使用Lisp作为“语言家族”,并假定Clojure是一个Lisp).
现在我可以在Clojure中执行以下操作,以便在编译时检查数组的长度：
(def my-vec-of-length-2 [0 1])
(defmacro compile-time-vec-length-check [x n]
(let [x @(resolve x)]
(assert (= n (count x)))))
(compile-time-vec-length-check my-vec-of-length-2 3)
现在这将失败,因为我期待一个长度为3的向量,但底层的向量是长度2.我在编译时得到这个信息.
user$lein uberjar Compiling compile-time-vec-check.core Exception in thread "main" java.lang.AssertionError: Assert Failed: (= n (count x))
现在我似乎以“动态语言”获得了依赖键入的好处.
我的问题是可以通过Lisp中的宏来实现依赖键入的好处吗？
只需检查一个我们在编译时精确知道的大小的向量并不难,并且不需要依赖类型.我们可以使用具有多态类型的正常类型语言以相当直接的方式来做到这一点.
依赖类型的重要洞察是它们可以依赖于运行时值.在你的例子中,所有的数字(2和3)都必须在编译时被知道,以使得断言正常工作.让我们想象一个函数zero_vec,它需要一个数字,并给出一个满为0的长度的向量.在一个依赖类型的伪代码中,它看起来像：
zero_vec : (n : ℕ) → Vec n
注意参数的值n如何出现在结果类型中！特别地,zero_vec 10将具有类型Vec 10,而zero_vec 42将具有类型zero_vec 42.更重要的是,尽管如此,您可以将在运行时不知道的值传递给zero_vec,并仍然键入您的代码.想象一下这样的东西：
n : ℕ ← readLine zero_vec n : Vec n
您仍然可以在编译时检查大小.例如,以下内容应该有效：
checkLength (zero_vec n) n
或者你甚至应该能够有一个像“3或更大的向量”类型,并且能够检查zero_vec n;这应该给你一个错误,因为它不能证明你读的是≥3.
关键是,类型检查本质上是一个非常通用的抽象解释形式,您必须能够传播和检查您将不会知道的值,直到运行时.
你不能用你的宏观方法来做到这一点.
但是,我认为您可以使用宏复制依赖类型.唯一的问题是,您本质上必须使用您的宏系统实现一个完整的依赖类型检查器！这是一个承诺,但可能不像你想的那么困难¹.
事实上,我的理解是,Qi和Shen是两种语言,实现为Common Lisp宏,类型系统与依赖类型一样强大.由于种种原因,我从来没有使用过(可能永远不会),所以我不确定它们是如何工作的.
¹查看“Simply Easy”一个很好的教程.
