Skip to content
Browse files

Merge branch 'typechecker3'

  • Loading branch information...
2 parents 7308527 + 0a3118b commit 4f7ca36d20bc05ae985349c60019195a11016eb6 Mattis Jeppsson committed May 21, 2010
Showing with 1,827 additions and 1 deletion.
  1. +2 −1 haskell.js
  2. +950 −0 haskell.typechecker.js
  3. +29 −0 typecheckertests.html
  4. +846 −0 typecheckertests.js
View
3 haskell.js
@@ -3,5 +3,6 @@ var haskell = {
interpreter: {},
ast: {},
primitives: {},
- utilities: {}
+ utilities: {},
+ typechecker: {}
};
View
950 haskell.typechecker.js
@@ -0,0 +1,950 @@
+
+(function (typechecker, ast) {
+ var inject = function(arr, f, acc) {
+ for(var ii in arr) {
+ acc = f(arr[ii], acc);
+ }
+ return acc;
+ };
+
+ var injectRight = function(arr, f, acc) {
+ for(var ii = arr.length-1; ii >= 0; ii--) {
+ acc = f(arr[ii], acc);
+ }
+ return acc;
+ };
+
+ var any = function(arr, f) {
+ return inject(
+ arr,
+ function(p, acc) {
+ return f(p) || acc;
+ },
+ false);
+ };
+
+ var elem = function(arr, p) {
+ return any(
+ arr,
+ function(pp) {
+ return p.compare(pp);
+ });
+ };
+
+ typechecker.any = any;
+
+ var all = function(arr, f) {
+ return inject(
+ arr,
+ function(p, acc) {
+ return f(p) && acc;
+ },
+ true);
+ };
+
+ typechecker.all = all;
+
+ var uniqueBy = function(arr, comp) {
+ var ys = [];
+ var member = function(x) {
+ for(var ii in ys) {
+ if(comp(x, ys[ii])) {
+ return true;
+ }
+ }
+ return false;
+ };
+ for(var ii in arr) {
+ if(!member(arr[ii])) {
+ ys.push(arr[ii]);
+ }
+ }
+ return ys;
+ };
+
+ var flatten = function(arr) {
+ return inject(
+ arr,
+ function(a, acc) {
+ return acc.concat(a);
+ },
+ []);
+ };
+
+ typechecker.flatten = flatten;
+
+ var unionBy = function(arr, otherArray, comp) {
+ return uniqueBy(arr.concat(otherArray), comp);
+ };
+
+ var intersectBy = function(arr, otherArray, comp) {
+ return inject(
+ arr,
+ function(a, acc) {
+ if(any(
+ otherArray,
+ function(b) {
+ return comp(a, b);
+ })) {
+ return acc.concat([a]);
+ }
+ return acc;
+ },
+ []
+ );
+ };
+
+ var filter = function(arr, f) {
+ return inject(
+ arr,
+ function(a, acc) {
+ if(f(a)) {
+ return acc.concat([a]);
+ }
+ return acc;
+ },
+ []
+ );
+ };
+
+ var diff = function(arr, diffArr){
+ return inject(
+ arr,
+ function(a, acc) {
+ if(!elem(diffArr, a)) {
+ return acc.concat([a]);
+ }
+ return acc;
+ },
+ []);
+ };
+
+ typechecker.filter = filter;
+ typechecker.unionBy = unionBy;
+ typechecker.intersectBy = intersectBy;
+
+ ast.Expression.prototype.infer = function(env) {
+ return this.desugar().infer(env);
+ };
+
+ ast.Constant.prototype.infer = function(env) {
+ return this.value.infer(env);
+ };
+
+
+
+ ast.Num.prototype.infer = function(env) {
+ var v = typechecker.newTVar(new typechecker.Star(), env);
+ return {
+ preds: [new typechecker.Pred("Num", v)],
+ type: v
+ };
+ };
+
+ ast.Wildcard.prototype.infer = function(env) {
+ var v = typechecker.newTVar(new typechecker.Star(), env);
+ return {
+ preds: [],
+ assumps: [],
+ type: v
+ };
+ };
+
+ ast.VariableBinding.prototype.infer = function(env) {
+ var v = typechecker.newTVar(new typechecker.Star(), env);
+ return {
+ preds: [],
+ assumps: [
+ new typechecker.Assump(
+ this.identifier,
+ typechecker.toScheme(v))
+ ],
+ type: v
+ };
+ };
+
+ ast.VariableLookup.prototype.infer = function(env) {
+ var a = env.lookup(this.identifier);
+ var inst = a.freshInst(env);
+ return {
+ preds: inst.preds(),
+ type: inst.t()
+ };
+ };
+
+ ast.Application.prototype.infer = function(env) {
+ var fInf = this.func.infer(env);
+ var argInf = this.arg.infer(env);
+ var t = env.newTVar(new typechecker.Star());
+ env.unify(typechecker.fn(argInf, t), fInf);
+ return {
+ preds: fInf.preds().concat(argInf.preds()),
+ type: t
+ };
+ };
+
+ ast.ConstantPattern.prototype.infer = function(env) {
+ var t = this.value.infer(env);
+ return t;
+ };
+
+ ast.PatternContructor.prototype.infer = function(env) {
+ /*
+ var sc = env.lookup(this.identifier);
+ var ps = [];
+ var ts = [];
+ var as = [];
+ this.patterns.map(
+ function(pat) {
+ var patInf = pat.infer(env);
+ ps = ps.concat(patInf.preds);
+ ts.push(patinf.type);
+ as = as.concat(patinf.assumps);
+ }
+ );
+ var inst = sc.freshInst(sc);
+ var infert = injectRight(
+ ts,
+ function(t, acc) {
+ typechecker.fn(t)
+ });
+ env.unify(inst.t(), ) */
+ };
+
+ ast.Combined.prototype.infer = function(env) {
+ var t = this.pattern.infer(env);
+ return {
+ preds: t.preds,
+ assumps: [
+ new typechecker.Assump(
+ this.identifier,
+ typechecker.toScheme(t.type))
+ ],
+ type: t.type
+ };
+ };
+
+ /*
+ * data Kind = Star | Kfun Kind Kind
+ * deriving Eq
+ *
+ */
+ typechecker.Star = function() {
+ this.toString = function() { return "*"; };
+ this.toStringNested = this.toString;
+ this.equals = function(otherKind) { return otherKind.isStar(); };
+ this.isStar = function() { return true; };
+ };
+ typechecker.Kfun = function(kind1, kind2) {
+ this.kind1 = function() { return kind1; };
+ this.kind2 = function() { return kind2; };
+ this.toString = function() {
+ return this.kind1().toStringNested() +
+ "->" +
+ this.kind2().toStringNested();
+ };
+ this.toStringNested = function() {
+ return "(" + this.toString() + ")";
+ };
+ this.isStar = function() { return false; };
+ this.equals = function(otherKind) {
+ return !otherKind.isStar() &&
+ this.kind1().equals(otherKind.kind1()) &&
+ this.kind2().equals(otherKind.kind2());
+ };
+ };
+
+ /*
+ * data Type = TVar Tyvar | TCon Tycon | TAp Type Type | TGen Int
+ * deriving Eq
+ *
+ */
+ typechecker.TVar = function(id, kind) {
+ this.type = function() { return "TVar"; };
+ this.toString = function () {
+ return this.id() + " (" + this.kind() + ")";
+ };
+ this.id = function () { return id; };
+ this.kind = function() { return kind; };
+ this.apply = function(subst) {
+ if (subst.lookup(this) != undefined) {
+ return subst.lookup(this);
+ }
+ return (new typechecker.TVar(this.id(), this.kind()));
+ };
+ this.tv = function() {
+ return [new typechecker.TVar(this.id(), this.kind())]; };
+ this.equals = function (otherTVar) {
+ return this.id() == otherTVar.id();
+ };
+ this.compare = function(otherType) {
+ return otherType.type() == "TVar" &&
+ this.id() == otherType.id() &&
+ this.kind().equals(otherType.kind());
+ };
+ this.substWith = function(replaceWith) {
+ return new typechecker.Subst().add(
+ this,
+ replaceWith);
+ };
+ this.mgu = function(otherType) {
+ if(this.compare(otherType)) {
+ return typechecker.nullSubst();
+ }
+ if(elem(otherType.tv(), this)) {
+ throw "occurs check fails";
+ }
+ if(!this.kind().equals(otherType.kind())) {
+ throw "kinds do not match";
+ }
+ return this.substWith(otherType);
+ };
+ this.match = function(otherType) {
+ if(!otherType.kind().equals(this.kind())) {
+ throw "types do not match";
+ }
+ return this.substWith(otherType);
+ };
+ this.inst = function(ts) { return this; };
+ this.hnf = function() { return true; };
+ };
+
+ typechecker.newTVar = function(kind, env) {
+ return new typechecker.TVar(env.nextName(), kind);
+ };
+
+ typechecker.TCon = function(id, kind) {
+ this.type = function() { return "TCon"; };
+ this.id = function() { return id; };
+ this.kind = function() { return kind; };
+ this.apply = function(subst) { return this; };
+ this.tv = function() { return []; };
+ this.equals = function(otherTCon) {
+ return this.id() == otherTCon.id() &&
+ this.kind().equals(otherTCon.kind());
+ };
+ this.compare = function(otherType) {
+ return otherType.type() == "TCon" &&
+ this.id() == otherType.id() &&
+ this.kind().equals(otherType.kind());
+ };
+ this.mgu = function(otherType) {
+ if(otherType.type() == "TVar") {
+ return otherType.mgu(this);
+ }
+ if(this.compare(otherType)) {
+ return typechecker.nullSubst();
+ }
+ throw "types do not unify";
+ };
+ this.match = function(otherType) {
+ if(otherType.compare(this)) {
+ return typechecker.nullSubst();
+ }
+ throw "types do not match";
+ };
+ this.inst = function(ts) { return this; };
+ this.hnf = function() { return false; };
+ };
+
+ typechecker.TAp = function(t1, t2) {
+ this.t1 = function() { return t1; };
+ this.t2 = function() { return t2; };
+ this.type = function() { return "TAp"; };
+ this.kind = function() { return this.t1().kind().kind2(); };
+ this.apply = function(subst) {
+ return new typechecker.TAp(t1.apply(subst),t2.apply(subst));
+ };
+ this.tv = function() {
+ if(t1.type() == "TVar" &&
+ t2.type() == "TVar" &&
+ t1.compare(t2)) {
+ return [t1];
+ }
+ return unionBy(
+ t1.tv(),
+ t2.tv(),
+ function(a, b) {
+ return a.compare(b);
+ });
+ };
+ this.mgu = function(otherType) {
+ if(otherType.type() == "TAp") {
+ var s1 = this.t1().mgu(otherType.t1());
+ var s2 = this.t2().apply(s1).mgu(otherType.t2().apply(s1));
+ return s1.compose(s2);
+ }
+ throw "types do not unify";
+ };
+ this.match = function(otherType) {
+ if(otherType.type() == "TAp") {
+ var s1 = this.t1().match(otherType.t1());
+ var s2 = this.t2().match(otherType.t2());
+ return s1.merge(s1, s2);
+ }
+ throw "types do not match";
+ };
+ this.compare = function(otherType) {
+ return otherType.type() == "TAp" &&
+ this.t1().compare(otherType.t1()) &&
+ this.t2().compare(otherType.t2());
+ };
+ this.inst = function(ts) {
+ return new typechecker.TAp(
+ this.t1().inst(ts),
+ this.t2().inst(ts));
+ };
+ this.hnf = function() {
+ return this.t1().hnf();
+ };
+ };
+ typechecker.TGen = function(id) {
+ this.id = function() { return id; };
+ this.apply = function(subst) { return this; };
+ this.tv = function() { return []; };
+ this.inst = function(ts) { return ts[this.id()]; };
+ };
+
+ typechecker.tArrow = function() {
+ return new typechecker.TCon(
+ "(->)",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())));
+ };
+ typechecker.fn = function(a,b) {
+ return new typechecker.TAp(
+ new typechecker.TAp(
+ typechecker.tArrow(),
+ a),
+ b);
+ };
+
+ typechecker.Subst = function() {
+ var mappings = {};
+ this.add = function(from, to) {
+ mappings[from.id()] = {
+ from: from,
+ to: to
+ };
+ return this;
+ };
+ this.inject = function(f, acc) {
+ for(var id in mappings) {
+ acc = f(mappings[id].from, mappings[id].to, acc);
+ }
+ return acc;
+ };
+ this.lookup = function(v) {
+ return (mappings[v.id()] != undefined &&
+ mappings[v.id()].from.compare(v)) ?
+ mappings[v.id()].to :
+ undefined;
+ };
+ this.exists = function(v) {
+ return this.lookup(v) != undefined;
+ };
+ this.compose = function(otherSubst) {
+ var curSubst = this;
+ var newSubst = this.inject(
+ function(from, to, acc) {
+ return acc.add(from, to);
+ },
+ new typechecker.Subst());
+ otherSubst.inject(
+ function(from, to, acc) {
+ return acc.add(from, to.apply(curSubst));
+ },
+ newSubst);
+ return newSubst;
+ };
+ this.merge = function(otherSubst) {
+ var newSubst = this.inject(
+ function(from, to, acc) {
+ return acc.add(from, to);
+ },
+ new typechecker.Subst());
+ otherSubst.inject(
+ function(from, to, acc) {
+ if(acc.exists(from) && !acc.lookup(from).compare(to)) {
+ throw "merge fails";
+ }
+ return acc.add(from, to);
+ },
+ newSubst);
+ return newSubst;
+ };
+ this.compare = function(otherSubst) {
+ var curSubst = this;
+ return this.inject(
+ function(from, to, acc) {
+ return acc &&
+ otherSubst.lookup(from) != undefined &&
+ to.compare(otherSubst.lookup(from));
+ },
+ true) &&
+ otherSubst.inject(
+ function(from, to, acc) {
+ return acc &&
+ curSubst.lookup(from) != undefined &&
+ to.compare(curSubst.lookup(from));
+ },
+ true);
+ };
+ };
+ typechecker.nullSubst = function() { return new typechecker.Subst({}); };
+
+ typechecker.Qual = function(preds, t) {
+ this.preds = function() { return preds; };
+ this.t = function() { return t; };
+ this.apply = function(subst) {
+ return new typechecker.Qual(
+ preds.map(
+ function(pred) { return pred.apply(subst); }),
+ t.apply(subst));
+ };
+ this.tv = function() {
+ return this.preds().map(
+ function(pred) { return pred.tv(); }
+ ).concat(this.t().tv());
+ };
+ this.compare = function(otherQual) {
+ var otherPreds = otherQual.preds();
+ for(var p in preds) {
+ if(!preds[p].compare(otherPreds[p])) {
+ return false;
+ }
+ }
+ if(!t.compare(otherQual.t())) {
+ return false;
+ }
+ return true;
+ };
+ this.inst = function(ts) {
+ return new typechecker.Qual(
+ this.preds().map(
+ function(pred) { return pred.inst(ts); }),
+ this.t().inst(ts));
+ };
+ this.quantify = function(vs) {
+ var vss = this.tv().filter(
+ function(v) {
+ return elem(vs, v);
+ });
+ var ks = vss.map(
+ function(vv) {
+ return vv.kind();
+ });
+ var i = 0;
+ var s = inject(
+ vss,
+ function(vv, acc) {
+ acc.add(vv, new typechecker.TGen(i));
+ i++;
+ return acc;
+ });
+ return new typechecker.Scheme(
+ ks,
+ this.apply(s));
+ };
+ this.stringify = function() {
+ return this.t().stringify();
+ };
+ };
+
+ typechecker.Pred = function(id, type) {
+ this.id = function() { return id; };
+ this.type = function() { return type; };
+ this.apply = function(subst) { return this.type().apply(subst); };
+ this.mguPred = function(otherPred) {
+ if(this.id() == otherPred.id()) {
+ return this.type().mgu(otherPred.type());
+ }
+ throw "classes differ";
+ };
+ this.matchPred = function(otherPred) {
+ if(this.id() == otherPred.id()) {
+ return this.type().match(otherPred.type());
+ }
+ throw "classes differ";
+ };
+ this.overlap = function(otherPred) {
+ try {
+ this.mguPred(otherPred);
+ } catch (x) {
+ return false;
+ }
+ return true;
+ };
+ this.tv = function() { return this.type().tv(); };
+ this.compare = function(otherPred) {
+ return this.id() == otherPred.id() &&
+ this.type().compare(otherPred.type());
+ };
+ this.inst = function(ts) {
+ return new typechecker.Pred(this.id(), this.type().inst(ts));
+ };
+ this.inHnf = function() {
+ return this.type().hnf();
+ };
+ };
+
+ typechecker.Scheme = function(kinds, qual) {
+ this.kinds = function() { return kinds; };
+ this.qual = function() { return this.qual; };
+ this.apply = function(subst) {
+ return new typechecker.Scheme(
+ this.kinds(),
+ this.qual().apply(subst));
+ };
+ this.tv = function() { return this.qual().tv(); };
+ this.freshInst = function(env) {
+ var ts = this.kinds().map(
+ function(kind) {
+ return typechecker.newTVar(kind, env);
+ });
+ return qual.inst(ts);
+ };
+ this.stringify = function() {
+ return this.qual().stringify();
+ };
+ };
+
+ typechecker.toScheme = function(type) {
+ return new typechecker.Scheme(
+ [],
+ new typechecker.Qual(
+ [],
+ type));
+ };
+
+ typechecker.Assump = function(id, scheme) {
+ this.id = function() { return id; };
+ this.scheme = function() { return scheme; };
+ };
+
+ typechecker.Assumps = function(parent) {
+ parent = parent == undefined ? {
+ lookup: function() {
+ throw "no such identifier";
+ }
+ } : parent;
+ var as = {};
+ this.add = function(a) {
+ as[a.id()] = a.scheme();
+ return this;
+ };
+ this.lookup = function(id) {
+ if(as[id] != undefined) {
+ return as[id];
+ }
+ return parent.lookup(id);
+ };
+ this.createChild = function() {
+ return new typechecker.Assumps(this);
+ };
+ };
+
+
+ typechecker.NameGen = function() {
+ var curr = 0;
+ this.nextName = function() {
+ var ret = curr;
+ curr++;
+ return "a" + ret;
+ };
+ };
+
+ typechecker.Klass = function(supers, instances) {
+ this.supers = function() { return supers; };
+ this.instances = function() { return instances; };
+ };
+
+ typechecker.KlassEnvironment = function() {
+ var env = {};
+ this.lookup = function(id) {
+ if(this.defined(id)) {
+ return env[id];
+ }
+ throw "class not found";
+ };
+ this.modify = function(id, klass) {
+ env[id] = klass;
+ return this;
+ };
+ this.defined = function(id) {
+ return env[id] != undefined;
+ };
+ this.addClass = function(id, supers) {
+ var cur = this;
+ if(this.defined(id)) {
+ throw "class already defined";
+ }
+ supers.map(
+ function(s) {
+ if(!cur.defined(s)) {
+ throw "superclass not defined";
+ }
+ });
+ return this.modify(
+ id,
+ new typechecker.Klass(
+ supers,
+ []));
+ };
+ this.addInst = function(ps, p) {
+ if(!this.defined(p.id())) {
+ throw "no class for instance";
+ }
+ var qs = this.lookup(p.id()).instances().map(
+ function(inst) {
+ return inst.t();
+ });
+ qs.map(
+ function(q) {
+ if(p.overlap(q)) {
+ throw "overlapping instances";
+ }
+ });
+ return this.modify(
+ p.id(),
+ new typechecker.Klass(
+ this.lookup(p.id()).supers(),
+ this.lookup(p.id()).instances().concat(
+ [new typechecker.Qual(ps, p)])));
+
+ };
+ this.bySuper = function(pred) {
+ var cur = this;
+ return [pred].concat(
+ flatten(
+ this.lookup(pred.id()).supers().map(
+ function(id) {
+ return cur.bySuper(
+ new typechecker.Pred(
+ id,
+ pred.type()));
+ }
+ )));
+ };
+ this.byInst = function(pred) {
+ var ret = undefined;
+ this.lookup(pred.id()).instances.map(
+ function(qual) {
+ if(ret != undefined) {
+ return;
+ }
+ try {
+ var u = qual.t().matchPred(pred);
+ ret = qual.preds().map(
+ function(p) {
+ return p.apply(u);
+ });
+ } catch (x) {
+ return;
+ }
+ }
+ );
+ return ret;
+ };
+
+ this.entail = function(ps, p) {
+ var cur = this;
+ var a = any(
+ ps.map(
+ function(pp) {
+ return cur.bySuper(pp);
+ }),
+ function(pps) {
+ return any(
+ pps,
+ function(pp) {
+ return p.compare(pp);
+ });
+ });
+ var qs = this.byInst(p);
+ var b = qs == undefined
+ ? false
+ : all(
+ qs,
+ function(q) {
+ return cur.entail(ps,q);
+ });
+ return a || b;
+ };
+
+ this.toHnfs = function(ps) {
+ return flatten(
+ ps.map(
+ function(p) {
+ return this.toHnf(p);
+ }));
+ };
+
+ this.toHnf = function(p) {
+ if(p.inHnf()) {
+ return [p];
+ }
+ var ps = this.byInst(p);
+ if(ps == undefined) {
+ throw "context reduction";
+ }
+ return this.toHnfs(ps);
+ };
+
+ this.simplify = function(qs) {
+ var rs = [];
+ var ps = qs;
+ while(ps.length != 0) {
+ if(this.entail(
+ rs.concat(ps.slice(1)),
+ ps.slice(0,1))) {
+ ps = ps.slice(1);
+ } else {
+ rs = ps.slice(0,1).concat(rs);
+ ps = ps.slice(1);
+ }
+ }
+ return rs;
+ };
+
+ this.reduce = function(ps) {
+ return this.simplify(this.toHnfs(ps));
+ };
+
+ this.scEntail = function(ps, p) {
+ var cur = this;
+ return any(
+ ps.map(
+ function(pp) {
+ return cur.bySuper(pp);
+ }),
+ function(pps) {
+ return elem(pps, p);
+ });
+ };
+ };
+
+ typechecker.ambiguities = function(ce, vars, preds) {
+ return diff(preds.tv(), vars).map(
+ function(v) {
+ return {
+ type: v,
+ preds: filter(
+ ps,
+ function (vv) {
+ return elem(preds, vv);
+ })
+ };
+ });
+ };
+
+ typechecker.numClasses = ["Num", "Fractional", "Integral", "Float",
+ "Real", "RealFloat", "RealFrac"];
+
+ typechecker.stdClasses = ["Eq", "Ord", "Show", "Read", "Bounded",
+ "Enum", "Ix", "Functor", "Monad",
+ "MonadPlus"].concat(typechecker.numClasses);
+
+ typechecker.candidates = function(ce, ambig) {
+ return all(
+ ambig.preds,
+ function(p) {
+ return p.type().compare(ambig.type);
+ }) && any(
+ ambig.preds,
+ function(p) {
+ return elem(
+ typechecker.numClasses,
+ p.id());
+ }) && all(
+ ambig.preds,
+ function(p) {
+ return elem(
+ typechecker.stdClasses,
+ p.id());
+ }) ? filter(
+ ce.defaults(),
+ function(t) {
+ return all(
+ ambig.preds,
+ function(p) {
+ return ce.entail(
+ [],
+ new typechecker.Pred(
+ p.id(),
+ t));
+ }
+ );
+ }) :[];
+ };
+
+ typechecker.defaultPreds = function(ce, ts, ps) {
+ var ambigs = typechecker.ambiguities(ce, ts, ps);
+ var candidates = ts.map(
+ ambigs,
+ function(t) {
+ return typechecker.candidates(ce, t);
+ });
+ if(any(
+ candidates,
+ function(c) {
+ return c.length == 0;
+ })) {
+ throw "cannot resolve ambiguity";
+ }
+ return flatten(
+ candidates.map(
+ function(ambig) {
+ return ambig.preds;
+ }
+ ));
+ };
+
+ typechecker.defaultSubst = function(ce, ts, ps) {
+ var ambigs = typechecker.ambiguities(ce, ts, ps);
+ var candidates = ts.map(
+ ambigs,
+ function(t) {
+ return typechecker.candidates(ce, t);
+ });
+ if(any(
+ candidates,
+ function(c) {
+ return c.length == 0;
+ })) {
+ throw "cannot resolve ambiguity";
+ }
+ var subst = new typechecker.Subst();
+ for(var i in ts) {
+ subst.add(ts[i], ambigs[i].type);
+ }
+ return subst;
+ };
+
+ typechecker.Environment = function(assumps, subst, namegen) {
+ this.nextName = function() {
+ return namegen.nextName();
+ };
+ this.extSubst = function(otherSubst) {
+ subst = subst.compose(otherSubst);
+ };
+ this.getSubst = function() {
+ return subst;
+ };
+ this.unify = function(t1, t2) {
+ var newSubst = t1.apply(
+ this.getSubst()).mgu(t2.apply(this.getSubst()));
+ this.extSubst(newSubst);
+ };
+ this.newTVar = function(kind) {
+ return typechecker.newTVar(kind, namegen);
+ };
+ this.lookup = function(id) {
+ return assumps.lookup(id);
+ };
+ };
+
+}) (haskell.typechecker, haskell.ast);
View
29 typecheckertests.html
@@ -0,0 +1,29 @@
+<html xmlns="http://www.w3.org/1999/xhtml">
+ <head>
+ <script src="lib/jsparse.js" type="text/javascript"></script>
+ <script src="haskell.js" type="text/javascript"></script>
+ <script src="haskell.utilities.js" type="text/javascript"></script>
+ <script src="haskell.ast.js" type="text/javascript"></script>
+ <script src="haskell.parser.js" type="text/javascript"></script>
+ <script src="haskell.primitives.js" type="text/javascript"></script>
+ <script src="haskell.interpreter.js" type="text/javascript"></script>
+ <script src="haskell.typechecker.js" type="text/javascript"></script>
+ <script src="typecheckertests.js" type="text/javascript"></script>
+
+ <script type="text/javascript">
+ /* fireunit.ok(true, "Passing test result");
+ fireunit.ok(false, "Failing test result.");
+ fireunit.compare("expected data", "expected data",
+ "Passing verification of expected and actual input.");
+ fireunit.compare("<div>expected</div>", "<div>actual</div>",
+ "Failing verification of expected and actual input.");
+
+ // Wait for asynchronous operation.
+ setTimeout(function(){
+ // Finish test
+ fireunit.testDone();
+ }, 1000); */
+ </script>
+ </head>
+ <body/>
+</html>
View
846 typecheckertests.js
@@ -0,0 +1,846 @@
+var ast = haskell.ast;
+var typechecker = haskell.typechecker;
+
+function expectException(f, e) {
+ try {
+ f();
+ } catch (x) {
+ return x == e;
+ }
+ return false;
+}
+/*
+var astt = new ast.Module(
+ [
+ new ast.Variable(
+ new ast.VariableBinding("inc"),
+ new ast.Lambda(
+ new ast.VariableBinding("x"),
+ new ast.Application(
+ new ast.Application(
+ new ast.VariableLookup("+"),
+ new ast.VariableLookup("x")),
+ new ast.Constant(new ast.Num(1))))),
+ new ast.Variable(
+ new ast.VariableBinding("inc2"),
+ new ast.Lambda(
+ new ast.VariableBinding("x"),
+ new ast.Application(
+ new ast.VariableLookup("inc"),
+ new ast.Application(
+ new ast.VariableLookup("inc"),
+ new ast.VariableLookup("x"))))),
+ new ast.Variable(
+ new ast.VariableBinding("main"),
+ new ast.Application(
+ new ast.VariableLookup("alert"),
+ new ast.Application(
+ new ast.VariableLookup("inc2"),
+ new ast.Constant(new ast.Num(2)))))
+ ]);
+
+var asttt = new ast.Application(
+ new ast.Application(
+ new ast.VariableLookup("+"),
+ new ast.VariableLookup("x")),
+ new ast.Constant(new ast.Num(1))); // ((x + :: (Num -> Num)) 1 :: Num)
+*/
+/*
+ * Kinds
+ *
+ */
+(function() {
+ fireunit.compare(
+ new typechecker.Star().toString(),
+ "*",
+ "Star is *");
+ fireunit.compare(
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()).toString(),
+ "*->*",
+ "Kfun Star Star is *->*");
+ fireunit.compare(
+ new typechecker.Kfun(
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()),
+ new typechecker.Star()).toString(),
+ "(*->*)->*",
+ "Kfun Kfun Star Star Star is (*->*)->*");
+ fireunit.compare(
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())).toString(),
+ "*->(*->*)",
+ "Kfun Star Kfun Star Star is *->(*->*)");
+ fireunit.ok(
+ new typechecker.Star().equals(new typechecker.Star()),
+ "Star is equal to Star");
+ fireunit.ok(
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()).equals(
+ new typechecker.Kfun(
+ new typechecker.Star(), new typechecker.Star())),
+ "Kfun Star Star is equal to Kfun Star Star");
+ fireunit.ok(
+ !new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()
+ ).equals(new typechecker.Star()),
+ "Kfun Star Star is not equal to Kfun Star");
+}) ();
+
+/*
+ * TVar
+ *
+ */
+(function () {
+ fireunit.ok(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).equals(new typechecker.TVar(
+ "a",
+ new typechecker.Star())),
+ "Any TVar instances with common identifiers are equal");
+ fireunit.ok(
+ !new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).equals(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())),
+ "Two TVars are not equal if their names do not match");
+}) ();
+
+/*
+ * Substitutions
+ *
+ */
+(function () {
+ fireunit.ok(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).apply(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()))
+ ).equals(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())),
+ "The simple substitution");
+ fireunit.ok(
+ new typechecker.TAp(
+ new typechecker.TVar("a", new typechecker.Star()),
+ new typechecker.TVar("b", new typechecker.Star())
+ ).apply(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()))
+ ).compare(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()))),
+ "Substitutions involving TAp");
+ fireunit.ok(
+ new typechecker.TCon(
+ "[]",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())
+ ).apply(
+ new typechecker.Subst()
+ ).compare(
+ new typechecker.TCon(
+ "[]",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()))),
+ "Type constructors are never substituted");
+}) ();
+
+/*
+ * Operations on substitutions
+ *
+ */
+
+(function () {
+ fireunit.ok(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "d",
+ new typechecker.Star())
+ ).compose(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "g",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "h",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()))
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "d",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "g",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "h",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()))),
+ "c.apply(a.compose(b)) == c.apply(b).apply(a)");
+ fireunit.ok(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).merge(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "d",
+ new typechecker.Star()))
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).add(
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "d",
+ new typechecker.Star()))),
+ "Merging to substitutions produces a merged substitution");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).merge(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "c",
+ new typechecker.Star())));
+ },
+ "merge fails"),
+ "merge can only be performed if the two substitutions agree");
+ }) ();
+
+
+/*
+ * Unification
+ *
+ */
+(function() {
+ fireunit.ok(
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star())
+ ).compare(typechecker.nullSubst()),
+ "Constructors of the same type and kind need no substitutions");
+ fireunit.ok(
+ expectException(
+ function () {
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TCon(
+ "apa",
+ new typechecker.Star())); },
+ "types do not unify"),
+ "If we cannot unify we get an exception");
+ fireunit.ok(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star())
+ ).compare(typechecker.nullSubst()),
+ "Identical type variables need not be substituted");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()))); },
+ "occurs check fails"),
+ "If one of the type variables depends on the other unification fails");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())));
+ },
+ "kinds do not match"),
+ "We cannot unify if kinds do not match");
+ fireunit.ok(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()))),
+ "If both variables are of the same kind substitute first with second");
+ fireunit.ok(
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()
+ ).mgu(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star())
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))),
+ "Same as previous but other order of application");
+ fireunit.ok(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star())
+ ).mgu(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "c",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()))
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TVar(
+ "c",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star()))
+ ).add(
+ new typechecker.TVar(
+ "b",
+ new typechecker.Star()),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()))),
+ "Unification of type applications is done by composing the underlying substitutions");
+ fireunit.ok(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).match(
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star())
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()))),
+ "A type variable can match anything of the same kind");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()
+ ).match(
+ new typechecker.TCon(
+ "[]",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())));
+ },
+ "types do not match"),
+ "If kinds are not same matching is impossible");
+ fireunit.ok(
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()
+ ).match(
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star())
+ ).compare(
+ new typechecker.Subst()),
+ "Matching type constructors need no substitution");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()
+ ).match(
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()));
+ },
+ "types do not match"),
+ "You cannot substitute one type into another");
+ fireunit.ok(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star())
+ ).match(
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "k",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star()))
+ ).compare(
+ new typechecker.Subst(
+ ).add(
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TVar(
+ "k",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())))),
+ "Type applications just operates recursively on the underlying types");
+ fireunit.ok(
+ expectException(
+ function() {
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TCon(
+ "Char",
+ new typechecker.Star())
+ ).match(
+ new typechecker.TVar(
+ "a",
+ new typechecker.Star()));
+ },
+ "types do not match"),
+ "Type applications can only match other applications");
+}) ();
+
+/*
+ * Type schemes
+ *
+ */
+(function() {
+ fireunit.ok(
+ new typechecker.Scheme(
+ [new typechecker.Star()],
+ new typechecker.Qual(
+ [
+ new typechecker.Pred(
+ "Monad",
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())))],
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TGen(0)))
+ ).freshInst(
+ new typechecker.NameGen()
+ ).compare(
+ new typechecker.Qual(
+ [
+ new typechecker.Pred(
+ "Monad",
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())))],
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "m",
+ new typechecker.Kfun(
+ new typechecker.Star(),
+ new typechecker.Star())),
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())))
+ ),
+ "TGens are substituted by their corresponding TVars");
+}) ();
+
+/*
+ * Literals
+ *
+ */
+(function() {
+ fireunit.ok(
+ new ast.Num(3
+ ).infer(new typechecker.NameGen()
+ ).preds[0].compare(
+ new typechecker.Pred("Num",
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star()))),
+ "Num literals are in the Num typeclass");
+}) ();
+
+/*
+ * Patterns
+ *
+ */
+(function() {
+ fireunit.ok(
+ new ast.Wildcard(
+ ).infer(
+ new typechecker.NameGen()
+ ).type.compare(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())),
+ "Wildcards are * type variables");
+ fireunit.ok(
+ new ast.VariableBinding(
+ "x"
+ ).infer(
+ new typechecker.NameGen()
+ ).type.compare(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())),
+ "Bind the new variable and create a type variable for it");
+ fireunit.ok(
+ new ast.Combined(
+ "x",
+ new ast.Wildcard()
+ ).infer(
+ new typechecker.NameGen()
+ ).type.compare(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())),
+ "Combined pattern");
+ fireunit.ok(
+ new ast.ConstantPattern(
+ new ast.Num(3)
+ ).infer(
+ new typechecker.NameGen()
+ ).type.compare(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())),
+ "Constant pattern");
+ fireunit.ok(
+ new ast.ConstantPattern(
+ new ast.Num(3)
+ ).infer(
+ new typechecker.NameGen()
+ ).preds[0].compare(
+ new typechecker.Pred(
+ "Num",
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star()))),
+ "Constant pattern2");
+
+}) ();
+
+/*
+ * NameGen
+ *
+ */
+(function() {
+ fireunit.compare(
+ new typechecker.NameGen().nextName(),
+ "a0",
+ "First name is a0");
+ fireunit.ok(
+ typechecker.newTVar(
+ new typechecker.Star(),
+ new typechecker.NameGen()
+ ).compare(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star()
+ )),
+ "Creating a new variable gives it a unique name and the assigned kind");
+}) ();
+
+/*
+ * Context reduction
+ *
+ */
+(function() {
+ fireunit.ok(
+ new typechecker.Pred(
+ "Num",
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star())
+ ).inHnf(),
+ "A type variable is in hnf");
+ fireunit.ok(
+ !new typechecker.Pred(
+ "Num",
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star())
+ ).inHnf(),
+ "A type constructor is not in hnf");
+ fireunit.ok(
+ new typechecker.Pred(
+ "Num",
+ new typechecker.TAp(
+ new typechecker.TVar(
+ "a0",
+ new typechecker.Star()),
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))
+ ).inHnf(),
+ "An application is in hnf if its first argument is");
+})();
+
+/*
+ * KlassEnvironment
+ *
+ */
+(function() {
+ fireunit.ok(
+ new typechecker.KlassEnvironment(
+ ).addClass(
+ "Eq",
+ []
+ ).lookup(
+ "Eq"
+ ).supers().length == 0,
+ "Here we have no supers");
+ fireunit.ok(
+ new typechecker.KlassEnvironment(
+ ).addClass(
+ "Eq",
+ []
+ ).addClass(
+ "Ord",
+ ["Eq"]
+ ).lookup(
+ "Ord"
+ ).supers()[0] == "Eq",
+ "Here we have one super");
+ fireunit.ok(
+ new typechecker.KlassEnvironment(
+ ).addClass(
+ "Eq",
+ []
+ ).defined("Eq"),
+ "Eq is defined");
+ fireunit.ok(
+ new typechecker.KlassEnvironment(
+ ).addClass(
+ "Eq",
+ []
+ ).addClass(
+ "Ord",
+ ["Eq"]
+ ).addInst(
+ [],
+ new typechecker.Pred(
+ "Ord",
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))
+ ).bySuper(
+ new typechecker.Pred(
+ "Ord",
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))
+ )[1].compare(
+ new typechecker.Pred(
+ "Eq",
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))),
+ "Superclass of Ord is Eq");
+/*
+ fireunit.ok(
+ new typechecker.KlassEnvironment(
+ ).addClass(
+ "Eq",
+ []
+ ).addInst(
+ [
+ new typechecker.Pred],
+ new typechecker.Pred(
+ "Eq",
+ new typechecker.TCon(
+ "Int",
+ new typechecker.Star()))
+ );
+ */
+
+
+})();
+
+fireunit.testDone();

0 comments on commit 4f7ca36

Please sign in to comment.
Something went wrong with that request. Please try again.