Implication Unifier
The Implication Unifier of two type expressions is a directed intersection of their statements. Implication is similar to Most General Unifier with the added constraint that information can only flow from left to right.
Implication by example
A type expression, implied with itself, will always yield itself, and its full self.
? => ? = ?
A => A = A
Aa => Aa = Aa
Aa + Bb => AA + Bb = AA + Bb
Aa -> Bb => Aa -> Bb = Aa -> Bb
(Aa,Bb) => (Aa,Bb) = (Aa,Bb)
Aa*Bb => Aa*Bb = Aa*Bb
Aa/Bb => Aa/Bb = Aa/Bb
[1] => [1] = [1]
The left-hand-side can narrow to unify. The right-hand-side cannot narrow.
Aa + Bb => Aa = Aa
Aa + Bb => Bb = Bb
Aa + Bb + Cc => Aa + Bb = Aa + Bb
Aa => Aa + Bb = {}
Bb => Aa + Bb = {}
Aa + Bb => Aa + Bb + Cc = {}
Components of compound types can narrow also.
{Aa + Bb} -> Aa => Aa -> Aa = {}
Aa -> {Aa + Bb} => Aa -> Aa = Aa -> Aa
Aa -> Aa => {Aa + Bb} -> Aa = Aa -> Aa
Aa -> Aa => Aa -> {Aa + Bb} = {}
({Aa + Bb},Aa) => (Aa,Aa) => (Aa,Aa)
(Aa,Aa) => ({Aa + Bb},Aa) => {}
{Aa+Bb)*Aa => Aa*Aa => Aa*Aa
Aa*Aa => {Aa+Bb}*Aa => {}
{Aa+Bb)/Aa => Aa/Aa => Aa*Aa
Aa/Aa => {Aa+Bb}/Aa => {}
There are several special cases.
A/() => A = A
A => A/() = A
Any failure to unify in a compound type yields the bottom type.
Aa -> Aa => Aa -> Bb = {}
(Aa,Bb) => (Aa,Cc) = {}
Aa*Bb => Aa*Cc = {}
Aa/Bb => Aa/Cc = {}
Parameter Unification yields the Most General Unifier of all substitutions. Parameters are invariant with respect to arrow types etc.
(Aa,Aa) -> Aa | (X,X) -> X = (Aa,Aa) -> Aa
(Aa,Bb) -> Cc | (X,X) -> X = {}
({Aa+Bb},{Aa+Bb}) -> {Aa+Bb+Cc} | (X,X) -> X = ({Aa+Bb},{Aa+Bb}) -> {Aa+Bb}
({Aa+Bb},{Aa+Cc}) -> {Aa+Bb+Cc} | (X,X) -> X = (Aa,Aa) -> Aa
({Aa+Bb},{Aa+Cc}) -> {Bb+Cc} | (X,X) -> X = {}