Как Forall реализован в Coq - PullRequest
Новая
       5

Как Forall реализован в Coq

0 голосов
/ 01 марта 2019

Пытаясь понять, как реализовать forall в JS или Ruby, мне было бы интересно узнать, как это на самом деле реализовано в Coq.Может быть, это поможет пролить свет.Похоже, я не могу найти определение путем поиска в Google.В основном просто где-то ищет ссылку в исходном коде.

1 Ответ

0 голосов
/ 01 марта 2019

Coq's forall является зависимым типом продукта и не может быть непосредственно закодирован в динамически типизированных языках, таких как 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) (данный номер возвращает объект типа 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

Обратите внимание, что мы не можем дать нетривиальный тип foo с type_arrow - нам нужно n дляТочно проверьте тип возвращаемого значения.

Но это далеко не так, как дает нам Coq, просто потому, что он не улавливает никаких ошибок во время компиляции.Если вы действительно хотите эти гарантии, вы должны материализовать языковые конструкции как объекты первого класса и выполнить собственную проверку типов.Одна статья, которую я мог бы порекомендовать: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html

...