Examples

Our Calculus of Constructions implementation demonstrates the full expressiveness of dependent type theory through comprehensive examples that span basic inductive types, higher-order polymorphic functions, universe polymorphism, implicit arguments, and dependent data structures. These examples showcase how the theoretical power of the Calculus of Constructions translates into practical programming language features.

Each example successfully type checks under our implementation, demonstrating the correctness of the constraint solving algorithms, universe system, and dependent type checker. The progression from simple types through complex dependent constructions illustrates how the Calculus of Constructions enables programming patterns while maintaining logical consistency.

Basic Inductive Types and Pattern Matching

The foundation of data structures in the Calculus of Constructions rests on inductive type definitions with constructor-based pattern matching:

#![allow(unused)]
fn main() {
inductive Bool : Type with
| true : Bool
| false : Bool

inductive Nat : Type with
| zero : Nat
| succ : Nat -> Nat

def predecessor (n : Nat) : Nat :=
  match n with
  case zero => zero
  case succ(m) => m

def not_bool (b : Bool) : Bool :=
  match b with
  case true => false
  case false => true
}

These basic examples demonstrate fundamental inductive types including natural numbers and booleans with their associated elimination functions. The predecessor function illustrates how pattern matching provides safe destructuring of inductive values, while the not_bool function shows simple enumeration-style pattern matching. The type checker ensures that all pattern cases are properly handled and that result types are consistent across branches.

Higher-Order Polymorphic Functions

The Calculus of Constructions supports polymorphic programming patterns through its dependent type system:

#![allow(unused)]
fn main() {
inductive Nat : Type with
  | zero : Nat
  | succ : Nat -> Nat

inductive Bool : Type with
  | true : Bool
  | false : Bool

axiom mult : Nat -> Nat -> Nat

def compose (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (x : A) : C :=
  g (f x)

def square (x : Nat) : Nat :=
  mult x x

def doTwice (A : Type) (h : A -> A) (x : A) : A :=
  h (h x)

def doThrice (A : Type) (h : A -> A) (x : A) : A :=
  h (h (h x))
}

These examples showcase the interaction between inductive types, higher-order functions, and polymorphic composition. The compose function demonstrates parametric polymorphism over three type parameters, while doTwice and doThrice show how higher-order functions can abstract over computational patterns. The square function illustrates interaction with primitive operations, showing how user-defined types integrate with built-in arithmetic.

Universe Polymorphism and Level Abstraction

Universe polymorphism enables definitions that work across the entire universe hierarchy, providing genuine genericity over type levels:

#![allow(unused)]
fn main() {
-- Universe Polymorphism Examples
-- Demonstrates universe-polymorphic definitions in CoC

-- 1. Basic universe polymorphic identity
def id.{u} (A : Sort (u+1)) (x : A) : A := x

-- 2. Universe polymorphic constant function  
def const.{u, v} (A : Sort (u+1)) (B : Sort (v+1)) (x : A) (y : B) : A := x

-- 3. Universe polymorphic composition
def compose.{u, v, w} (A : Sort (u+1)) (B : Sort (v+1)) (C : Sort (w+1)) (g : B -> C) (f : A -> B) (x : A) : C := g (f x)

-- 4. Tests at different universe levels
-- At Type level (u = Zero)
axiom test_id_type : (A : Type) -> A -> A
def id_at_type : (A : Type) -> A -> A := id

-- At Prop level (u = -1, but we use Zero for Prop)  
axiom test_id_prop : (A : Prop) -> A -> A

-- 5. Inductive types with universe parameters
inductive List.{u} (A : Sort (u+1)) : Sort (u+1) with
  | nil : List A
  | cons : A -> List A -> List A

-- 6. Higher-order universe polymorphism
def map.{u, v} (A : Sort (u+1)) (B : Sort (v+1)) (f : A -> B) (l : List A) : List B := match l with case nil => nil B case cons(x, xs) => cons B (f x) (map A B f xs)

-- 7. Universe constraints with max
axiom pair_type.{u, v} : Sort (u+1) -> Sort (v+1) -> Sort (u+1)

-- 8. Dependent types with universe parameters
def dependent_id.{u} (A : Sort (u+1)) (P : A -> Sort (u+1)) (x : A) (px : P x) : P x := px

-- 9. Examples of universe level arithmetic
-- Type 0 = Sort 1
-- Type 1 = Sort 2  
-- Type n = Sort (n+1)
axiom level0 : Type       -- Type 0 = Sort 1
axiom level1 : Type 1     -- Type 1 = Sort 2
axiom level2 : Type 2     -- Type 2 = Sort 3

-- 10. Universe polymorphic structures
structure Pair.{u, v} (A : Sort (u+1)) (B : Sort (v+1)) : Sort (u+1) :=
  (fst : A)
  (snd : B)
}

These examples demonstrate universe-polymorphic definitions that abstract over universe levels using explicit level parameters. The id.{u} function works at any universe level, while const.{u,v} shows polymorphism over multiple universe parameters. The inductive type List.{u} demonstrates universe-polymorphic data structures that can contain elements at arbitrary universe levels.

The universe arithmetic expressions like Sort (u+1) show how the universe solver handles level arithmetic during type checking. Universe constraints ensure that polymorphic instantiations respect the universe hierarchy while enabling maximum flexibility in generic programming.

Comprehensive Implicit Arguments

Implicit arguments provide syntactic convenience while maintaining the full expressiveness of dependent types:

#![allow(unused)]
fn main() {
-- Comprehensive tests for implicit arguments with constraint solving

-- Basic datatypes
inductive Nat : Type with
  | zero : Nat
  | succ : Nat -> Nat

inductive List (A : Type) : Type with
  | nil : List A
  | cons : A -> List A -> List A

inductive Pair (A : Type) (B : Type) : Type with
  | mkPair : A -> B -> Pair A B

-- Test 1: Simple implicit argument
def id {A : Type} (x : A) : A := x

-- Test 2: Multiple implicit arguments  
def const {A : Type} {B : Type} (x : A) (y : B) : A := x

-- Test 3: Implicit with explicit type application
def apply_id : Nat -> Nat := id

-- Test 4: Multiple implicit arguments with inference
def first : Nat -> Nat -> Nat := const

-- Test 5: Nested implicit arguments
def compose {A : Type} {B : Type} {C : Type} 
           (g : B -> C) (f : A -> B) (x : A) : C :=
  g (f x)

-- Test 6: Implicit arguments in inductive type constructors
def empty_list : List Nat := nil Nat

def nat_list : List Nat := cons Nat zero (nil Nat)

-- Test 7: Implicit with dependent types
def replicate {A : Type} (n : Nat) (x : A) : List A :=
  match n with
  case zero => nil A
  case succ(m) => cons A x (replicate m x)

-- Test 8: Higher-order functions with implicits
def map {A : Type} {B : Type} (f : A -> B) (l : List A) : List B :=
  match l with
  case nil => nil B
  case cons(x, xs) => cons B (f x) (map f xs)

-- Test 9: Polymorphic pair operations
def fst {A : Type} {B : Type} (p : Pair A B) : A :=
  match p with
  case mkPair(a, b) => a

def snd {A : Type} {B : Type} (p : Pair A B) : B :=
  match p with
  case mkPair(a, b) => b

-- Test 10: Complex composition with implicits
def double_map {A : Type} {B : Type} {C : Type}
               (f : B -> C) (g : A -> B) (l : List A) : List C :=
  map f (map g l)

-- Test 11: Implicit arguments in let bindings
def test_let : Nat :=
  let f := id in
  f zero

-- Test 12: Implicit arguments with universe polymorphism
-- axiom Type_id {u : Level} : Type u -> Type u
-- def type_identity : Type -> Type := Type_id

-- Test cases that should work
def test_id_nat : Nat := id zero
def test_const_nat : Nat := const zero (succ zero)
def test_compose_nat : Nat -> Nat := compose succ succ
def test_pair : Pair Nat Nat := mkPair Nat Nat zero (succ zero)
def test_fst : Nat := fst (mkPair Nat Nat zero (succ zero))

-- Test that implicit arguments are correctly inferred
def complex_test : List Nat :=
  map succ (cons Nat zero (cons Nat (succ zero) (nil Nat)))
}

This comprehensive example demonstrates the full range of implicit argument features. Simple functions like id {A : Type} show basic type inference, while complex functions like double_map demonstrate implicit argument propagation through nested polymorphic calls. The constraint solver automatically infers type arguments based on usage context, eliminating boilerplate while maintaining type safety.

The map and replicate functions show how implicit arguments work with recursive functions and pattern matching. The constraint solver tracks type relationships across recursive calls, ensuring that implicit arguments are consistently instantiated throughout the computation.

Dependent Data Structures

Dependent types enable data structures whose types encode computational properties, providing compile-time guarantees about program behavior:

#![allow(unused)]
fn main() {
inductive Nat : Type with
  | zero : Nat
  | succ : Nat -> Nat

inductive Vec (A : Type) : Nat -> Type with  
  | nil : Vec A zero
  | cons : (n : Nat) -> A -> Vec A n -> Vec A (succ n)
}

Length-indexed vectors represent the paradigmatic example of dependent data types. The Vec A n type carries its length n at the type level, enabling operations that are guaranteed to respect vector bounds at compile time. The nil constructor produces vectors of length zero, while cons extends vectors by exactly one element.

This example demonstrates how dependent types can encode invariants that would traditionally require runtime checking. The type system ensures that vector operations respect length constraints, eliminating entire classes of array bounds errors at compile time.

Structure Types and Record Operations

Structure types provide named field access and demonstrate the Calculus of Constructions’ support for record-like data organization:

#![allow(unused)]
fn main() {
inductive Nat : Type with
| zero : Nat
| succ : Nat -> Nat

structure Point : Type := (x : Nat) (y : Nat)

axiom point_instance : Point

axiom Point_x : Point -> Nat
axiom Point_y : Point -> Nat

def get_x_coordinate : Nat := Point_x point_instance
}

The Point structure demonstrates basic record types with named fields. While full dot notation requires additional parser support, the example shows how structures integrate with the dependent type system. Structure types can participate in dependent constructions, enabling data modeling patterns.

Polymorphic Function Composition

Complex polymorphic programming demonstrates the interaction between higher-order functions, type inference, and constraint solving:

#![allow(unused)]
fn main() {
def compose (A : Type) (B : Type) (C : Type) : (B -> C) -> (A -> B) -> A -> C :=
  fun g => fun f => fun x => g (f x)

def doTwice (A : Type) : (A -> A) -> A -> A :=
  fun h => fun x => h (h x)
}

These examples show curried function definitions that demonstrate the lambda calculus foundations of the Calculus of Constructions. The compose function shows three-way type polymorphism, while doTwice demonstrates how polymorphic higher-order functions can abstract over computational patterns.

Working Examples with Type Inference

Practical examples demonstrate how the constraint solver handles complex type inference scenarios:

#![allow(unused)]
fn main() {
axiom id_type : Type -> Type -> Type

def simple_function : Type -> Type := fun A => A

inductive MyBool : Type with
  | true : MyBool
  | false : MyBool

def constFunc (A : Type) (B : Type) : A -> B -> A :=
  fun x => fun y => x
}

These working examples demonstrate the type inference engine in action. The constFunc definition shows how the constraint solver handles nested lambda abstractions with polymorphic types. The simple_function illustrates type-level computation, where functions can manipulate types as first-class values.

Advanced Dependent Programming

The most examples demonstrate the full power of dependent types in practical programming scenarios:

#![allow(unused)]
fn main() {
-- Dependent types example

def id (A : Type) (x : A) : A := x

axiom Nat : Type
def test_id_nat : Nat -> Nat := id Nat
}

These examples show how dependent types enable programs where types can depend on term values. The id function with explicit type parameters demonstrates how dependent functions can be polymorphic over both types and their computational properties.