list.dtlc (992B)
1 \ Church-encoded unary natural numbers (pattern matching on built-in Nats is 2 \ not implemented) 3 UNat: Type := [M: Type, M, M -> M] -> M; 4 zero: UNat := fn M, z, s => z; 5 succ: UNat -> UNat := fn n => fn M, z, s => s (n M z s); 6 7 \ Conversion from UNat to built-in Nat type for pretty printing 8 toNat: UNat -> Nat := fn n => n Nat 0 (fn m => m + 1); 9 10 \ Polymorphic Church-encoded lists 11 List: Type -> Type := fn A => 12 [M: Type, M, [A, M] -> M] -> M; 13 nil: [A: Type] -> List A := fn A => 14 fn M, n, c => n; 15 cons: [A: Type, A, List A] -> List A := rec fn A, hd, tl => 16 fn M, n, c => c hd (tl M n c); 17 18 \ Example operations on lists 19 length: [A: Type, List A] -> UNat := fn A, l => 20 l UNat zero (fn _, n => succ n); 21 map: [A: Type, B: Type, A -> B, List A] -> List B := fn A, B, f, l => 22 l (List B) (nil B) (fn a, tl' => cons B (f a) tl'); 23 24 l0: List UNat := cons UNat zero (cons UNat zero (cons UNat zero (nil UNat))); 25 l1: List UNat := map UNat UNat succ l0; 26 (map UNat Nat toNat l0, map UNat Nat toNat l1)