haw*_*eye 9 macros haskell clojure compile-time dependent-type
这是一个诚实的问题,而不是一个巨魔.我请你耐心等待.
当Cedric谈到依赖类型时,他声明的好处是在编译时检查List长度:
拥有一个包含一个元素的列表将是一个类型错误,因此上面代码段中的第二行不应该编译.
当Ana Bove和Peter Dybjer谈论依赖类型时,他们声明的好处是在编译时检查列表长度:
依赖类型是依赖于其他类型元素的类型.一个例子是长度为n且具有类型A的分量的向量的类型An.另一个例子是m个n矩阵的Amn类型.我们说类型An取决于数字n,或者An是由数字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))
现在,我似乎在"动态语言"中获得了Dependent Typing的好处.
我的问题是,是否有可能在Lisp中实现使用宏的依赖键入的好处？
Tik*_*vis 15
是的,但不是你提出的方式.
只是检查其大小,我们确切地知道在编译时并不困难,并没有一个向量没有需要依赖类型.我们可以在具有多态类型的普通类型语言中以相当简单的方式执行此操作.
依赖类型的重要见解是它们可以依赖于运行时值.在您的示例中,必须在编译时知道所有数字(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它; 这应该会给你一个错误,因为它不能证明n你读的是≥3.
关键在于,类型检查基本上成为一种非常通用的抽象解释形式,您必须能够传播并检查在运行时才能知道的值.
你的宏观方法无法做到这一点.
但是,我认为您可以使用宏复制依赖类型.唯一的问题是你基本上必须使用你的宏系统实现一个完整的依赖类型检查器!这是一项承诺,但可能并不像你想象的那么困难¹.
事实上,我的理解是Qi和Shen是两种语言,实现为Common Lisp宏,类型系统与依赖类型一样强大.出于各种原因,我从未使用它们(也许永远不会),所以我不确定它们是如何工作的.
¹查看"简单易用"以获得精彩的教程.