Despite the value of higher order logic, it has been recognized that there are some useful concepts beyond the power of higher order logic to state. An example is the practical device of monads. Monads are particularly useful in modeling, for example, realistic computations involving state or exceptions, as a shallow embedding in a logic which itself is strictly functional, without state or exceptions. The paper presents examples of using the HOL-Omega system to model monads and prove theorems about their general properties, as well as concepts from category theory such as functors and natural transformations.

The current implementation of the HOL-Omega system differs from that described in the 2009 paper in one major respect. Previously, ranks were attributes of types, as also were kinds. In the current version, ranks are attributes of kinds, and a type's rank is the rank of its kind. The grammar of kinds and types is now as follows:

Kinds: k ::= ty : r | κ : r | k₁ ⇒ k₂

Types: σ ::= α : k |  τ : k | σ_arg σ_opr | λα.σ | ∀α.σ | ∃α.σ

The parser will accept type annotations of terms (``t : σ``), kind annotations of types (``σ : k``), and rank annotations of kinds (``k : r``).  Rank annotations of types (``σ :≤ r``) are also still accepted.

When deciding if a function term can be properly applied to its argument, the type of the argument must be ≤ the type expected by the function, where some difference in ranks is acceptable. As an important innovation, the comparison of types for inequality (≤) depends on whether or not they are classified as humble types. Humble types are types that do not change how they interact with other types as they are promoted to higher rank. In other words, their semantics do not change if their rank is increased. Humble types are defined and described further in an upcoming paper being submitted to ITP 2013.

This change has had no effect on the examples in the 2009 paper or in the example source files in the distribution.