#!/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
      )))