当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.

@H_502_6@

当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.

@H_502_6@

更大的一点是,我们对程序的正确性有额外的保证,因为在编译时可以获得更多的信息和检查.

现在我的经验是,人们(从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中的宏来实现依赖键入的好处吗？