search

stedolan / mlsub

Prototype type inference engine
193 stars 19 forks source link

type union position / subtyping lattice traversal #2

Open wizzard0 opened 7 years ago

wizzard0 commented 7 years ago

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?

stedolan commented 7 years ago

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?