Discussion

From a pre-existing order on type A, we can build two different orders on the type option A depending on whether we interpret the new element None as ⊥ or ⊤. For our purposes both are useful. Indeed consider modules for example. We say that M1 ≤ M2 if all of the definitions in M1 are present in M2. This means that when we inerpret None as the absence of a definition, we should think of it as a ⊥ element: any definition is bigger than no definition. But for a given symbol defined in M1, in addition to providing the same definition, a larger module M2 is also allowed to associate the special value magic with that symbol. This means that the symbol is "overdefined": magic is the result of linking two conflicting modules, for instance i ↦ τ ⊕ i ↦ τ = i ↦ magic. Since we want ⊕ to be monotonic, and an upper bound of its arguments, it is natural to interpret magic as a top element. Of course, attempting to construct an actual program from a module containing magic will fail. But this failure fits right in as ⊤, since it results from a module that is in some sense too large. We like to use the option monad to express the program construction process, and if in this context we interpret None as a ⊤ element, then we do not need any special side-conditions when stating the monotonicity of program construction.

Simple order

Option predicates

Monad operations

FIXME: We probably want to make one of those have and explicitely higher priority, but it's not clear yet which one would be best. Contexts where transport is used will be particularly telling.