I'm playing with type unification, I got the algorithm from here, https://eli.thegreenplace.net/2018/unification/
My problem is: I want to use this as type inference step, I tweaked the code from the above page and added Lark parser to parse and unify X -> Y == W -> Z expressions, meaning something like unify(_(X, Y), _(Y, W)). Also I use poly is for meaning poly types, or type variables, mono is for meaning mono types like int, str, bool in my case.
I expected a -> b == int -> int to be reject. I can understand why is not rejected because unify(f(A, B), f(1, 1)) is perfect fine. But I want it to fail. I don't know if this should be done in a later step, at type checking type, that would happen after type inference time, but to my application this seem just wrong.
Is the unification algorithm that I used the right one for type inference?
If not, how to fix this unification unify(a -> b, int -> int) problem so it's rejected? (any papers on subject would be nice)
Or I'm just mixing the balls and this should be done latter on type checking?
Here is my code, to execute you need Lark pip install lark-parser, I'm using python 3.8 for testing
from typing import (
Dict,
Any,
NamedTuple,
Optional,
Callable,
TypedDict,
Generic,
TypeVar,
Iterable,
Sequence,
Tuple,
Union,
)
from lark import Lark, Transformer as LarkTransformer
Subst = Dict[str, "TTerm"]
class TTerm:
"Type term"
def unify_eq(self, other) -> bool:
pass
class TArrow(TTerm):
def __init__(self, t1, t2):
self.t1 = t1
self.t2 = t2
def unify_eq(self, other) -> bool:
return (
other.__class__ is TArrow
and self.t1.unify_eq(other.t1)
and self.t2.unify_eq(other.t2)
)
def __repr__(self):
return f"({self.t1} -> {self.t2})"
class TPoly(TTerm):
def __init__(self, name):
self.name = name
def unify_eq(self, other):
return other.__class__ is TPoly and self.name == other.name
def __eq__(self, other):
return other.__class__ is self.__class__ and self.name == other.name
def __repr__(self):
return self.name
class TMono(TTerm):
def __init__(self, val):
self.val = val
def unify_eq(self, other):
return self.__class__ is other.__class__ and self.val == other.val
def __eq__(self, other):
return other.__class__ is self.__class__ and self.val == other.val
def __repr__(self):
return self.val
class TUnification:
def __init__(self, t1: TTerm, t2: TTerm):
self.t1 = t1
self.t2 = t2
def unify(self):
return unify(self.t1, self.t2, {})
def __repr__(self):
return f"unify({self.t1}, {self.t2})"
def unify(x: TTerm, y: TTerm, subst: Optional[Subst]) -> Optional[Subst]:
print(f"unify({x}, {y}, {subst})")
if subst is None:
return None
elif x.unify_eq(y):
return subst
elif isinstance(x, TPoly):
return unify_var(x, y, subst)
elif isinstance(y, TPoly):
return unify_var(y, x, subst)
elif isinstance(x, TArrow) and isinstance(y, TArrow):
subst = unify(x.t1, y.t1, subst)
subst = unify(x.t2, y.t2, subst)
return subst
else:
return None
def unify_var(v: TPoly, x: TTerm, subst: Subst) -> Optional[Subst]:
print(f"unify_var({v}, {x}, {subst})")
if v.name in subst:
return unify(subst[v.name], x, subst)
elif isinstance(x, TPoly) and x.name in subst:
return unify(v, subst[x.name], subst)
elif occurs_check(v, x, subst):
return None
else:
return {**subst, v.name: x}
def occurs_check(v: TPoly, term: TTerm, subst: Subst) -> bool:
if v == term:
return True
elif isinstance(term, TPoly) and term.name in subst:
return occurs_check(v, subst[term.name], subst)
elif isinstance(term, TArrow):
return occurs_check(v, term.t1, subst) or occurs_check(v, term.t2, subst)
else:
return False
grammar = r"""
unification : term "==" term
?term : tarrow | POLY -> poly | MONO -> mono
?tarrow : term "->" term | "(" term ")"
POLY : /[a-z]/
MONO : /(int|str|bool)/
%import common.WS
%import common.SH_COMMENT
%import common.INT
%ignore WS
%ignore SH_COMMENT
"""
parser = Lark(grammar, start="unification", parser="lalr")
class Transformer(LarkTransformer):
def unification(self, tree):
return TUnification(tree[0], tree[1])
def poly(self, tree):
return TPoly(tree[0].value)
def mono(self, tree):
return TMono(tree[0].value)
def tarrow(self, tree):
return TArrow(tree[0], tree[1])
def parse(input_):
return Transformer().transform(parser.parse(input_))
print(parse("a -> b == int -> int").unify())
Output
unify((a -> b), (int -> int), {})
unify(a, int, {})
unify_var(a, int, {})
unify(b, int, {'a': int})
unify_var(b, int, {'a': int})
{'a': int, 'b': int}
