Coq 中的 forall 是如何实现的答案

【问题标题】：How forall is implemented in CoqCoq 中的 forall 是如何实现的
【发布时间】：2019-03-01 06:52:53
【问题描述】：

在试图了解如何在 JS 或 Ruby 中 implement forall 时，我很想知道它是如何在 Coq 中实际实现的。也许这将有助于阐明一些问题。我似乎没有通过在谷歌上搜索找到定义。主要只是在某处寻找源代码中的链接。

【问题讨论】：

澄清一下：您是否在 Ruby/JS 中实现了一种编程语言，并且想知道如何为该语言实现 forall；还是您在问如何在 JS/Ruby 本身中表达forall-like 构造？
或者/或者，我只是在玩弄如何用 ruby 中的 DSL 来定义它，但我不在乎它是如何定义的，只要它是程序/oo 语言。

标签： coq

【解决方案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

【讨论】：