hm/test

60 lines
1.6 KiB
Plaintext
Raw Normal View History

2022-01-20 21:05:25 +01:00
-- 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) (λn f. 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) (λn f. 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
| num : Nat
| add : Expr Expr
| mul : 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