mlsub
mlsub copied to clipboard
type union position / subtyping lattice traversal
Is there a description on why mlsub chooses {x: T1|T2, y: T3|T4} over {x:T1,y:T3}|{x:T2,y:T4} when computing a type union of {x:T1,y:T3} and {x:T2,y:T4}?
I understand that both typings are technically correct but want to know whether it is possible to steer the computation so it would produce the second option (union of records instead of record of unions)
Edit: more general question is, how does one encode a different options of traversing the subtyping lattice when there's multiple paths between types?
It tries to minimise the size of the underlying automaton, which happens to be smaller for {x: T1|T2, y: T3|T4}
than for {x:T1,y:T3}|{x:T2,y:T4}
. What it produces is a textual representation of a minimal deterministic automaton, which isn't always the best possible representation. It would probably be worth finding some better heuristics for converting automata to text, although I'm not convinced that union-of-records is an improvement over record-of-unions.
I don't understand your second question. What do you mean by multiple paths between types?