haskell – 可以通过Lisp中的宏来实现依赖键入的好处吗？

当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中的宏来实现依赖键入的好处吗？