Coq 中的 forall 是如何实现的
Posted
技术标签:
【中文标题】Coq 中的 forall 是如何实现的【英文标题】:How forall is implemented in Coq 【发布时间】:2019-03-01 06:52:53 【问题描述】:在试图了解如何在 JS 或 Ruby 中 implement forall
时,我很想知道它是如何在 Coq 中实际实现的。也许这将有助于阐明一些问题。我似乎没有通过在谷歌上搜索找到定义。主要只是在某处寻找源代码中的链接。
【问题讨论】:
澄清一下:您是否在 Ruby/JS 中实现了一种编程语言,并且想知道如何为该语言实现forall
;还是您在问如何在 JS/Ruby 本身中表达forall
-like 构造?
或者/或者,我只是在玩弄如何用 ruby 中的 DSL 来定义它,但我不在乎它是如何定义的,只要它是程序/oo 语言。
【参考方案1】:
Coq 的 forall
是一个 dependent product type,不能直接用像 javascript 这样的动态类型语言编码,因为它们只是缺少静态类型的概念。
从某些语言、函数的角度来看,它的目的是为一些无意义的东西提供静态类型。假设我们有无限的类型集合T1
、T2
...
那么这个函数不能通过常规方法分配一个(非平凡的)类型:
function foo(n)
return eval("new T" + n + "()");
但是,我们可以使用辅助函数为其赋予依赖 (forall
) 类型
function H(n)
return eval("T" + n);
那么foo
的类型将是forall n:Number, H(n)
(给定Number,返回一个H(n)
类型的对象,即Tn
)。
很遗憾,我们无法将此信息传达给 JS 解释器以静态执行此合同。但是,我们可以在运行时检查它!
让我们从创建一个小型类型检查框架开始。
function type_number(x)
if (typeof x == "number") return x;
throw new Error("not a number");
function type_function(x)
if (typeof x == "function") return x;
throw new Error("not a function");
function type_instance(clss)
return function (x)
if (x instanceof clss) return x;
throw new Error("not an instance of " + clss);
;
现在我们可以实现一个不依赖的函数类型了
function type_arrow(arg, ret)
return function(f)
f = type_function(f);
return function(x)
return ret(f(arg(x)));
;
;
这里arg
必须是参数的类型检查器,ret
必须是返回值的类型检查器。例如:
// declare a function from numbers to numbers
var fn1 = type_arrow(type_number, type_number)((x) => x * x);
fn1(10); // works
fn1("asdsa"); // fails
// bad declaration, but, unfortunately, JS cannot possibly catch it at "compilation" time
var fn2 = type_arrow(type_number, type_number)((x) => "Hello!");
fn2(10); // fails, return value is not a number
现在进入有趣的部分:
function type_forall(arg, ret)
return function(f)
f = type_function(f);
return function(x)
var y = f(arg(x));
return ret(x)(y);
;
;
注意ret
现在是一个包含两个参数的柯里化函数。鉴于我的第一个示例,我们现在可以给 foo
一个类型:
function T1()
function T2()
function T3()
function T4()
function T5()
// ...etc
function foo(n)
return eval("new T" + n + "()");
function H(n)
return eval("T" + n);
function type_H(n)
return type_instance(H(n));
var typed_foo = type_forall(type_number, type_H)(foo);
typed_foo(2); // successfully invokes and returns a T2 instance
请注意,我们不能用type_arrow
为foo
提供非平凡的类型 - 我们需要n
来正确地检查返回值。
但这远不及 Coq 为我们提供的强大功能,仅仅是因为它不会在编译时捕获任何错误。如果你真的想要这些保证,你必须将语言构造物化为第一类对象并执行你自己的类型检查。我可以推荐的一篇文章是http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
【讨论】:
以上是关于Coq 中的 forall 是如何实现的的主要内容,如果未能解决你的问题,请参考以下文章