EditHint: Could be merged/recombined with PartialOrder, ConstraintLogicProgramming, BooleanLattice, DirectedAcyclicGraph (all CategoryMath I guess)

EditHint 2: An appropriate place for most stuff could be LatticeStructure.

Meet and join are two fundamental operations on types; which come from CategoryTheory. A ''meet'' of two types '''T1''' and '''T2''' is a type '''Tm''' with the following properties:

* '''Tm''' is a (not necessarily proper) subtype of both '''T1''' and '''T2'''. ('''Tm''' <= '''T1'''; '''Tm''' <= '''T2''').

* There is no type '''Tx''' such that '''Tx''' <= '''T1''', '''Tx''' <= '''T2''', and '''Tm''' < '''Tx'''. (If there is, then '''Tx''' and not '''Tm''' might be a meet of '''T1''' and '''T2'''


Note that if '''T1''' < '''T2''', then '''Tm''' = '''T1'''. Similarly, if '''T2''' < '''T1''', then '''Tm''' = '''T2''', and if '''T1''' = '''T2''', then '''Tm''' = '''T1''' = '''T2'''.

Likewise, a ''join'' is the opposite function; it has the following properties:

* '''Tj''' is a (not necessarily proper) supertype of both '''T1''' and '''T2'''. ('''Tj''' >= '''T1'''; '''Tm''' >= '''T2''').

* There is no type '''Tx''' such that '''Tx''' >= '''T1''', '''Tx''' >= '''T2''', and '''Tj''' > '''Tx'''. (If there is, then '''Tx''' and not '''Tj''' might be a join of '''T1''' and '''T2'''

Note that if '''T1''' < '''T2''', then '''Tj''' = '''T2'''. Similarly, if '''T2''' < '''T1''', then '''Tj''' = '''T1''', and if '''T1''' = '''T2''', then '''Tj''' = '''T1''' = '''T2'''.

In a type system with single inheritance, and neither '''T1''' nor '''T2''' is a subtype of the other, then their meet doesn't exist (alternatively, it could be said to be the BottomType, and no instances of that exist). In a single-inheritance system, two types may have either one join or none; in singly-rooted systems without MI, any two types will have exactly one join (which may be TopType).

In a type system with MultipleInheritance, a class which inherits from '''T1''' and '''T2''' is a meet of the two types, unless it has a supertype which is a meet of '''T1''' and '''T2'''. Likewise, multiple joins are possible in such a system. (The Java type system runs into difficulties with this; as the type of the ternary (? :) operator is - or ought to be - defined as the join of the types of the two choices. Since Java interfaces allow multiple joins to exist, the language takes the easy way out and uses Object instead, rather than selecting any particular join).

A ''meet'' can also be called an ''intersection'', and a ''join'' can be called a ''sum'' or ''union'' (preferably not ''union'', since unions in CeeLanguage are not joins).

However, a CeeLanguage union can certainly be used to represent a meet:

  union {
    struct foo *pFoo;
    struct bar *pBar;
  } foobar_u;

There have been many times I've wished for a way to have a JavaLanguage (or occasionally CeeSharpLanguage) reference have a meet-of-interfaces type.  (Actually defining this meet as a new interface doesn't work -- because JavaLanguage uses NominativeTyping instead of StructuralTyping, classes that implement all necessary interfaces would have to have the new interface explicitly added to their supertype list.)  In CeeSharpLanguage the concept sometimes falls apart because the same method may have multiple different implementations dispatched on the type of the reference.

See also ConstraintLogicProgramming, BooleanLattice, DirectedAcyclicGraph