Generalization #3
Computing over types
•
sum :: Nat ~> Nat ~> Nat
•
{sum Z x} = x
•
{sum (S x) y} = S {sum x y}
•
•
append :: List a n ->
•
List a m ->
•
List a {sum n m}
•
append Nil ys = ys
•
append (Cons x xs) ys = Cons x (append xs ys)