type_constraints.js

"use strict";

/*
    type schemes
    TyScheme =
          TyVar
        | TyInt
        | TyBool
        | TyProd
        | TyArrow
*/
class TyScheme {
    constructor() {

    }

    toString() {
        throw new Error("unknown type scheme");
    }

    equals(tyScheme) {
        throw new Error("unknown type scheme");
    }
}

class TyVar extends TyScheme {
    constructor(name) {
        super();
        this.name = name;
    }

    toString() {
        return this.name;
    }

    equals(tyScheme) {
        return tyScheme instanceof TyVar
            && this.name === tyScheme.name;
    }
}

class TyInt extends TyScheme {
    constructor() {
        super();
    }

    toString() {
        return "Int";
    }

    equals(tyScheme) {
        return tyScheme instanceof TyInt;
    }
}

class TyBool extends TyScheme {
    constructor() {
        super();
    }

    toString() {
        return "Bool";
    }

    equals(tyScheme) {
        return tyScheme instanceof TyBool;
    }
}

class TyProd extends TyScheme {
    constructor(left, right) {
        super();
        this.left  = left;
        this.right = right;
    }

    toString() {
        return "(" + this.left.toString() + ") * (" + this.right.toString() + ")";
    }

    equals(tyScheme) {
        return tyScheme instanceof TyProd
            && this.left.equals(tyScheme.left)
            && this.right.equals(tyScheme.right);
    }
}

class TyArrow extends TyScheme {
    constructor(dom, codom) {
        super();
        this.dom   = dom;
        this.codom = codom;
    }

    toString() {
        return "(" + this.dom.toString() + ") -> (" + this.codom.toString() + ")";
    }

    equals(tyScheme) {
        return tyScheme instanceof TyArrow
            && this.dom.equals(tyScheme.dom)
            && this.codom.equals(tyScheme.codom);
    }
}

const newTyVar = () => {
    let counter = 0;
    return () => new TyVar("t" + (++counter).toString());
}();

/* type environment */
class Environment {
    constructor(dict) {
        this.dict = dict;
    }

    static empty() {
        return new Environment(Object.create(null));
    }

    lookup(x) {
        return this.dict[x];
    }

    extend(x, tyScheme) {
        let newDict = Object.create(this.dict);
        newDict[x] = tyScheme;
        return new Environment(newDict);
    }
}

/*
    terms
    Term =
          TmInt
        | TmBool
        | TmVar
        | TmAdd
        | TmEq
        | TmGt
        | TmProd
        | TmLeft
        | TmRight
        | TmAbs
        | TmApp
        | TmIf
        | TmLet
        | TmFix
*/
class Term {
    constructor() {

    }

    toString() {
        throw new Error("unknown term");
    }

    // extends constraints
    extendCstrs(env, tyScheme, cstrs) {
        throw new Error("unknown term");
    }
}

class TmInt extends Term {
    constructor(n) {
        super();
        this.n = n;
    }

    toString() {
        return this.n.toString();
    }

    extendCstrs(env, tyScheme, cstrs) {
        return cstrs.concat([[tyScheme, new TyInt()]]);
    }
}

class TmBool extends Term {
    constructor(b) {
        super();
        this.b = b;
    }

    toString() {
        return this.b.toString();
    }

    extendCstrs(env, tyScheme, cstrs) {
        return cstrs.concat([[tyScheme, new TyBool()]]);
    }
}

class TmVar extends Term {
    constructor(x) {
        super();
        this.x = x;
    }

    toString() {
        return this.x;
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyScheme1 = env.lookup(this.x);
        if (tyScheme1) {
            return cstrs.concat([[tyScheme, tyScheme1]]);
        }
        throw new Error("unbound variable: " + this.x);
    }
}

class TmAdd extends Term {
    constructor(s, t) {
        super();
        this.s = s;
        this.t = t;
    }

    toString() {
        return "(" + this.s.toString() + ") + (" + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let cstrs1 = this.s.extendCstrs(env, new TyInt(), cstrs);
        let cstrs2 = this.t.extendCstrs(env, new TyInt(), cstrs1);
        return cstrs2.concat([[tyScheme, new TyInt()]]);
    }
}

class TmEq extends Term {
    constructor(s, t) {
        super();
        this.s = s;
        this.t = t;
    }

    toString() {
        return "(" + this.s.toString() + ") = (" + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let cstrs1 = this.s.extendCstrs(env, new TyInt(), cstrs);
        let cstrs2 = this.t.extendCstrs(env, new TyInt(), cstrs1);
        return cstrs2.concat([[tyScheme, new TyBool()]]);
    }
}

class TmGt extends Term {
    constructor(s, t) {
        super();
        this.s = s;
        this.t = t;
    }

    toString() {
        return "(" + this.s.toString() + ") > (" + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let cstrs1 = this.s.extendCstrs(env, new TyInt(), cstrs);
        let cstrs2 = this.t.extendCstrs(env, new TyInt(), cstrs1);
        return cstrs2.concat([[tyScheme, new TyBool()]]);
    }
}

class TmProd extends Term {
    constructor(s, t) {
        super();
        this.s = s;
        this.t = t;
    }

    toString() {
        return "(" + this.s.toString() + ", " + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar1 = newTyVar();
        let tyVar2 = newTyVar();
        let cstrs1 = this.s.extendCstrs(env, tyVar1, cstrs);
        let cstrs2 = this.t.extendCstrs(env, tyVar2, cstrs1);
        return cstrs2.concat([[tyScheme, new TyProd(tyVar1, tyVar2)]]);
    }
}

class TmLeft extends Term {
    constructor(t) {
        super();
        this.t = t;
    }

    toString() {
        return "left(" + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar = newTyVar();
        return this.t.extendCstrs(env, new TyProd(tyScheme, tyVar), cstrs);
    }
}

class TmRight extends Term {
    constructor(t) {
        super();
        this.t = t;
    }

    toString() {
        return "right(" + this.t.toString() + ")";
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar = newTyVar();
        return this.t.extendCstrs(env, new TyProd(tyVar, tyScheme), cstrs);
    }
}

class TmAbs extends Term {
    constructor(x, t) {
        super();
        this.x = x;
        this.t = t;
    }

    toString() {
        return "\\" + this.x + ". " + this.t.toString();
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar1 = newTyVar();
        let tyVar2 = newTyVar();
        let env1 = env.extend(this.x, tyVar1);
        let cstrs1 = this.t.extendCstrs(env1, tyVar2, cstrs);
        return cstrs1.concat([[tyScheme, new TyArrow(tyVar1, tyVar2)]]);
    }
}

class TmApp extends Term {
    constructor(s, t) {
        super();
        this.s = s;
        this.t = t;
    }

    toString() {
        return "(" + this.s.toString() + ") @ (" + this.t.toString() + ")"; 
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar = newTyVar();
        let cstrs1 = this.s.extendCstrs(env, new TyArrow(tyVar, tyScheme), cstrs);
        return this.t.extendCstrs(env, tyVar, cstrs1);
    }
}

class TmIf extends Term {
    constructor(s, t, u) {
        super();
        this.s = s;
        this.t = t;
        this.u = u;
    }

    toString() {
        return "if " + this.s.toString() + " then " + this.t.toString() + " else " + this.u.toString();
    }

    extendCstrs(env, tyScheme, cstrs) {
        let cstrs1 = this.u.extendCstrs(env, new TyBool(), cstrs);
        let tyVar = newTyVar();
        let cstrs2 = this.u.extendCstrs(env, tyVar, cstrs1);
        return this.u.extendCstrs(env, tyVar, cstrs2);
    }
}

class TmLet extends Term {
     constructor(x, s, t) {
        super();
        this.x = x;
        this.s = s;
        this.t = t;
     }

     toString() {
        return "let " + this.x + " = " + this.s.toString() + " in " + this.t.toString();
     }

     extendCstrs(env, tyScheme, cstrs) {
        let tyVar = newTyVar();
        let cstrs1 = this.s.extendCstrs(env, tyVar, cstrs);
        let env1 = env.extend(this.x, tyVar);
        return this.t.extendCstrs(env1, tyScheme, cstrs1);
     }
}

class TmFix extends Term {
    constructor(x, y, t) {
        super();
        this.x = x;
        this.y = y;
        this.t = t;
    }

    toString() {
        return "fix " + this.x + ". " + this.y + ". " + this.t.toString();
    }

    extendCstrs(env, tyScheme, cstrs) {
        let tyVar1 = newTyVar();
        let tyVar2 = newTyVar();
        let env1 = env.extend(this.x, new TyArrow(tyVar1, tyVar2));
        let env2 = env1.extend(this.y, tyVar1);
        let cstrs1 = this.t.extendCstrs(env2, tyVar2, cstrs);
        return cstrs1.concat([[tyScheme, new TyArrow(tyVar1, tyVar2)]]);
    }
}

// step 1: construct constraints
function constructCstrs(env, t) {
    return t.extendCstrs(env, newTyVar(), []);
}

// example
{
    function printCstrs(cstrs) {
        console.log(cstrs.map(p => p[0].toString() + " = " + p[1].toString()).join("\n"));
    }
    {
        let env = Environment.empty();
        env = env.extend("y", newTyVar());
        let t = new TmAbs("f", new TmAbs("x",
            new TmApp(
                new TmVar("f"),
                new TmAdd(new TmVar("x"), new TmVar("y"))
            )
        ));
        let cstrs = constructCstrs(env, t);
        printCstrs(cstrs);
    }
}

// step 2: unification
// ...