hm/test.hm

-- currently all parameterised types are commented out until kinds are being implemented

-- no pattern matching, instead a recursor is given based on your inductive definition
-- for example: the following

{-
type List A
  | nil : List A
  |	cons  : A → List A → List A
-}

-- will bring the following into scope
-- rec[List] : B → (A → B → B) → List A → B

-- map could then be written as
 
{-
map : (A → B) → List A → List B
 := rec[List] nil (λx xs. cons (f x) xs)
-}

-- one could then define the naturals as follows

type Nat
  |	zero : Nat
  |	succ : Nat → Nat

-- defining addition as

add : Nat → Nat → Nat
 := rec[Nat] (λx. x) (λf n. succ (f n))

-- since                | rec[Nat] : B → (Nat → B → B) → Nat → B
-- which generalizes to | rec[Nat] : (Nat → Nat) → (Nat → (Nat → Nat) → (Nat → Nat)) → Nat → Nat → Nat
--                                   ^ adding 0    ^ recursively adding one more     ^ resulting addition type

-- id is used to not add anything, the second function takes the last addition function and adds a layer
-- of succ onto it, this way it generates a function for adding the right amount.

-- multiplication is defined similairly

mul : Nat → Nat → Nat
 := rec[Nat] (λx. zero) (λf n. add n (f n))

-- here's an example of a simpler type

type Bool
  |	true : Bool
  | false : Bool

not : Bool → Bool
 := rec[Bool] false true

-- now, let's look at a bit more interesting example

type Expr
  | ENat : Nat →  Expr
  | EAdd : Expr → Expr → Expr
  | EMul : Expr → Expr → Expr

-- this generates the following recursor
-- rec[Expr] : (Nat → B) → (B → B → B) → (B → B → B) → Expr → B

eval : Expr → Nat
 := rec[Expr] (λx. x) add mul