You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### 50 lines 1.2 KiB Plaintext Raw Permalink Blame History

 ```#!/usr/bin/env -S ivo -c ``` ```// Create a list by iterating `f` `n` times: ``` ```let iterate = \f x. ``` ``` { Z -> [] ``` ``` ; S n -> (x :: iterate f (f x) n) ``` ``` }; ``` ``` ``` ```// Use the iterate function to count to 10: ``` ```let countToTen : [Nat] = ``` ``` let countTo = iterate S 1 ``` ``` in countTo 10; ``` ``` ``` ```// Append two lists together: ``` ```let append = \xs ys. ``` ``` { [] -> ys ``` ``` ; (x :: xs) -> (x :: append xs ys) ``` ``` } xs; ``` ``` ``` ```// Reverse a list: ``` ```let reverse = ``` ``` { [] -> [] ``` ``` ; (x :: xs) -> append (reverse xs) [x] ``` ``` }; ``` ``` ``` ```// Now we can reverse `"reverse"`: ``` ```let reverseReverse : [Char] = reverse "reverse"; ``` ``` ``` ```// Calculating `3 + 2` with the help of Church-encoded numerals: ``` ```let threePlusTwo : Nat = ``` ``` let Sf = \n f x. f (n f x) ``` ``` ; plus = \x. x Sf ``` ``` in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z; ``` ``` ``` ```let undefined = undefined; ``` ``` ``` ```// This expression would loop forever, but `callcc` saves the day! ``` ```let callccSaves : Nat = S (callcc \k. undefined (k Z)); ``` ``` ``` ```// And if it wasn't clear, this is what the `Char` constructor does: ``` ```let charB : Char = { Char c -> Char (S c) } 'a; ``` ```// (it outputs `'b`) ``` ``` ``` ```// pack all of the examples into tuples so the main function can print them ``` ```let main = ``` ``` ( countToTen ``` ``` , ( reverseReverse ``` ``` , ( callccSaves ``` ``` , charB ``` ``` ))) ```