CODEWITHSUNDEEP
coq
Lance Pollard
Lance Pollard

Reputation: 79468

How forall is implemented in Coq

In trying to understand how to implement forall in JS or Ruby, I would be interested to know how it's actually implemented in Coq. Maybe that will help shed some light. I don't seem to find the definition by searching around on Google. Mainly just looking for a link in the source code somewhere.

Upvotes: 0

Views: 121

Answers (1)

user2512323
user2512323

Reputation:

Coq's forall is a dependent product type and cannot be directly encoded in a dynamically typed languages like Javascript because they simply lack the concept of static type.

It serves the purpose of giving a static type to some nonsensical from the point of view of some languages, functions. Consider we have an infinite collection of types T1, T2...

Then this function cannot be assigned a (nontrivial) type by conventional methods:

function foo(n) {
  return eval("new T" + n + "()");
}

However, we can give it dependent (forall) type, using a helper function

function H(n) {
  return eval("T" + n);
}

The type of foo then will be forall n:Number, H(n) (given Number, returns an object of type H(n), ie Tn).

Unfortunately, there is no way for us to convey this information to the JS interpreter to statically enforce this contract. However, we can check it at runtime!

Lets start by making a small type checking framework.

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);
  };
}

Now we can implement a non-dependent function type

function type_arrow(arg, ret) {
    return function(f) {
        f = type_function(f);
        return function(x) {
            return ret(f(arg(x)));
        };
    };
}

Here arg must be a type checker for the argument, and ret must be a type checker for the return value. For example:

// 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

Now to the fun part:

function type_forall(arg, ret) {
    return function(f) {
        f = type_function(f);
        return function(x) {
            var y = f(arg(x));
            return ret(x)(y);
        };
    };
}

Notice how ret is now a curried function of two arguments. Given my first example, we can now give a type to 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

Note that we cannot give a non-trivial type to foo with type_arrow - we need n to properly typecheck the return value.

But this is nowhere near the power Coq gives us, simply because it does not catch any errors at compile time. If you really want these guarantees, you must materialize language constructs as first class objects and perform your own type checking. One article I could recommend is http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html

Upvotes: 3

Related Questions