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

The constructors of option_le have type classes as types, so we need to cast them before we use them as hints.

Option predicates

Monad operations