lambda_cube.lean

lambda_cube.lean

-- PTS-style First-order dependent types
-- usage examples

--------------------------------------------------------------------------------
-- λ→
def plus_1_of_nat : Π _ : ℕ, ℕ := λ x : ℕ, x + 1

#check plus_1_of_nat
#reduce Π _ : ℕ, ℕ

#check ℕ -- parameter type sort, Type
#check ℕ -- return type sort, Type

def plus_1_of_nat' : Π _ : (ℕ:Type), (ℕ:Type) := λ x : ℕ, x + 1

-- Type to Type
-- value into value, terms that can bind terms

--------------------------------------------------------------------------------
-- λ2 (system F)
def identity : Π X : Type, Π _ : X, X := λ X : Type, λ x : X, x

#check identity
#reduce Π X : Type, Π _ : X, X

#check Type -- parameter type sort, Type 1
#check Π x : ℕ , ℕ  -- example return type sort, Type

def identity' : Π X : (Type : Type 1), ((Π _ : X, X) : Type) := λ X , λ x : X, x

-- Kind to Type
-- type into value, terms that can bind types, corresponding to polymorphism.

--------------------------------------------------------------------------------
-- λω
def IdentityFunctionType : Π _ : Type, Type := λ X : Type, X → X

#check IdentityFunctionType
#reduce Π _ : Type, Type

#check Type -- parameter type sort, Type 1
#check Type -- return type sort, Type 1

def IdentityFunctionType' : Π _ : (Type: Type 1), (Type: Type 1) := λ X , X → X

def HttpResponse : Π _ : Type → Type, Type := λ Future : Type → Type, Future ℕ

#check Type → Type -- parameter type sort, Type 1
#check Type -- return type sort, Type 1
def HttpResponse' : Π _ : ((Type → Type): Type 1), (Type: Type 1) := λ Future , Future ℕ

-- Kind to Kind
-- types that can bind types, corresponding to (binding) type operators

--------------------------------------------------------------------------------
-- λP (LF)
constant data : Type

constant Vector : ℕ → Type
constant nil : Vector 0
constant cons : Π n : ℕ, data → Vector n → Vector (n + 1)
constant first : Π n : ℕ, Vector (n + 1) → data
constant last : Π n : ℕ, Vector (n + 1) → data

#check ℕ -- parameter type sort, Type
#check Type -- return type sort, Type 1

constant Vector' : (ℕ: Type) → (Type : Type 1)

-- Type to Kind
-- value to type, types that can bind terms, corresponding to dependent types.