Delving Simplicity Part Ⅱ: Combinator Completeness of Simplicity

The unit type in Simplicity, represented as 𝟙 or ONE, is essentially a zero-bit data type that contains a single value, symbolized by an empty tuple. This contrasts with the sum type, A + B, a tagged union allowing for conditional compositions based on whether a value belongs to the left or right-hand type within the union. Product types, denoted as A × B, facilitate parallel compositions by containing pairs of values from two types.

The language's core expressions and combinators are designed to directly implement sequential, parallel, and conditional compositions. Simplicity does not incorporate function types in its type system, positioning it as a first-order language. Among its basic operations are iden, which simply passes its input to its output, and unit, which discards its input and returns the unit type's single value. Sequential and parallel compositions in Simplicity are achieved through specific combinators, while conditional composition employs a case combinator alongside a shared environment type to allow branches access to common data.

Moreover, Simplicity introduces four additional combinators to manage product and sum types effectively, allowing for the extraction of pair values or the tagging of function results. The language's design draws inspiration from the sequent calculus, emphasizing operations over values. This distinction is crucial as Simplicity expressions denote operations, contrasting with many programming languages where expressions can represent values directly.

The article also touches upon the Simplicity Completeness theorem, ensuring that any function between two Simplicity types can be expressed within the language. This theorem has been formally verified using the Rocq proof assistant, underscoring Simplicity's robust foundation. However, practical application of this theorem leads to significantly large expressions, highlighting the challenge of generating concise Simplicity expressions for complex functions.

In summary, Simplicity's approach to programming emphasizes a rigorous type system and a rich set of combinators to execute various forms of composition. Its separation of expressions and values, alongside the formal verification of its completeness theorem, positions Simplicity as a theoretically sound yet practically challenging language for developers. Further exploration of Simplicity will delve into its interaction with transactions and the construction of data structures, promising more insights into its capabilities and applications.