2 ms·
If you program in a statically-typed language with interfaces like Java or C#, you have already encountered lattices though you may not have realized it. In tho
by munificent 6y ago
If you program in a statically-typed language with interfaces like Java or C#, you have already encountered lattices though you may not have realized it. In those languages, the subtype relation between pairs of types forms a semi-lattice.
That means that for any pair of types, there is a least upper bound type that is a supertype of both of them. (When discussing this, we usually allow a type to be considered its own supertype. So by "X is a supertype of Y" we mean something more like "every instance of Y is also an X". So String is its own supertype because every String is also a String.) For example, the least upper bound of Object and List is Object. The least upper bound of ArrayList and Stack is List, etc.
This is important because there are places where you need to find a type that contains all values of two other types. For example, say you are type checking:
foo(condition ? a : b);
Is this a valid call? To determine that, you need to see if the type of the argument matches the declared parameter type on foo. But what is the type of a conditional operator? The value could have type a or type b. You need a type that subsumes both of those. The answer most languages use is to calculate the least upper bound of the types of the two branches. That works only because there is a least upper bound for every pair of types, and we know that because we know types form a semi-lattice.
Are types a full lattice? For that, you also need a greatest lower bound, or a "meet". That means for any pair of types there needs to be a type that is a sub-type of both of them. In some languages that doesn't exist. But languages that have a "bottom" type give you this property. The bottom type, by definition, is a subtype of all types. So whenever you need the greatest lower bound, if there isn't any other obvious candidate (like if one of the types is directly a subtype of the other), you can just throw your hands up and use bottom.