3 ms·

A bit off-topic, but could someone ELI5 what a lattice is in this context?

• chombier 4y ago
  I think this refers to a system of types in which for any two types there is also an union type and an intersection type in the lattice.
• mjd 4y ago
  If you have two types, there should be a single type that "joins" them, in the sense that you can understand both of the original types as somehow being special cases of the join type. A join is not necessarily a union, since the representations of the three types might be completely different, and also because the third type might contain many values that don't correspond to anything in the two original types. (It might be much bigger than the union.) Mathematical lattices must also have "meets", which are like joins except down instead of up. I'm not sure that meets are as important as joins in this context.
• layer8 4y ago
  It refers to https://en.m.wikipedia.org/wiki/Lattice_(order) https://en.m.wikipedia.org/wiki/Lattice_(order), with the elements of the lattice being the arithmetic types and the order relation being the subtyping relation here. Given any two types in the lattice, the lattice property then guarantees that there exists a unique common (least) supertype (aka upper bound, supremum) of the two types. Which means you can apply the binary operation (e.g. addition) as defined for that common supertype.