undefined | Better HN

0 pointsdnautics5y ago0 comments

Totally different.

This the question that needs resolution:

    f = (x) => (...) ? Foo : g(x)

    g = (x) => (...) ? Bar : f(x)

Obviously the type of the result of f should be Foo | Bar but figuring that out is not trivial because there is a circular dependency.

0 comments

1 comments · 1 top-level

Joker_vD5y ago

You start with f having type 'a0 -> a1', and g having type 'a2 -> a3'.

Looking at the body of f you infer that a0 = a2 and a1 = Foo | a3, after the substitution f has type 'a0 -> Foo | a3' and g has type 'a0 -> a3'.

Looking at the body of g you infer that a0 = a0 (whew!) and a3 = Bar | (a3 | Foo). Now, the last one is tricky, and here is the point where you can easily get your type inference engine to diverge, but the (least) solution is given by a3 = Bar | Foo (because A = A | B iff A is a superset of B).

So, after the final substitution you have 'a0 -> Bar | Foo' for f and 'a0 -> Bar | Foo' for g, generalize 'a0' as appropriate.

j / k navigate · click thread line to collapse