how would you encode a program like
function f<T>(x: T) { return x; }
function g(x: number) { return { a: f(x), b: f(x.toString()) }; }
in sat?if that's easy, how about length and f in:
function append<T>(xs: list<T>, ys: list<T>) {
return match xs {
Nil() -> ys,
Cons(hd, tl) -> Cons(hd, append(tl, ys)),
};
}
function flatten<T>(xs: list<list<T>>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> append(hd, flatten(xs)),
};
}
function map<T, U>(f: (T) => U, xs: list<T>) {
return match xs {
Nil() -> Nil(),
Cons(hd, tl) -> Cons(f(hd), tl),
};
}
function sum(xs: list<number>) {
return match xs {
Nil() -> 0,
Cons(hd, tl) -> hd + length(tl),
};
}
function length<T>(xs: list<T>) { return sum(map((_) -> 1, xs)); }
function f<T>(xs: list<list<T>>) {
return length(flatten(xs)) === sum(map(length, xs));
}
hm-style inference handles polymorphism and type application without a complicated sat encoding