Terms and constraints

Terms

Ligare has one syntactic category: the term. Literals, names, functions, constraints, propositions, proofs, and data declarations are all terms:

• 1 is a term.
• "hello" is a term.
• fun x => x + 1 is a term.
• int is a term.
• x >= 0 is a term.

There is no separate type-language for describing values. A term is checked against another term, and that relationship is a constraint.

Constraints

The expression 1 : int says that the term 1 satisfies the constraint int. Refinement constraints add a predicate:

def Nat : prop := int where (x => x >= 0)

def answer : Nat := 42

The definition of Nat is a proposition-level constraint. The value 42 is runtime data, while the refinement evidence is checked and erased.

Constraints are themselves terms, so they can be constrained too. For example, int : prop classifies int as a proposition-level constraint. This is the mechanism that replaces the type/value split found in many languages.

Universes and levels

The current language has two root universes:

Universe	Role	Runtime
data	Computable values and retained program terms	Yes
prop	Propositions, constraints, and erased evidence	No

sort0, sort1, and higher forms classify terms by level; sort is not a third runtime universe. The indexed forms data n and prop n select a universe at a specific level. The compiler solves level constraints and rejects inconsistent positive cycles.

There are no separate theorem or proof universes in the current implementation. theorem is a top-level declaration command, and a proof of a proposition is simply a term checked against that proposition.