hm/test.hm

58 lines
1.4 KiB
Plaintext

-- one could define the naturals as follows
type Nat
| zero : Nat
| succ : Nat → Nat
-- which will bring a recursor for the type into scope
-- rec[Nat] : A → (A → A) → Nat → A
-- defining addition as
add : Nat → Nat → Nat
:= rec[Nat] (λx. x) (λf n. succ (f n))
-- since | rec[Nat] : A → (A → A) → Nat → A
-- which generalizes to | rec[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 → A) → (A → A → A) → (A → A → A) → Expr → A
eval : Expr → Nat
:= rec[Expr] (λx. x) add mul
-- here's some other functions
isEven : Nat → Bool
:= rec[Nat] true not
type bot
absurd : bot -> A := rec[bot]