2. Functions & recursion

Teaches: a generic let rec over your own data, no trait bound

Functions are ordinary thunks bound with let; recursive functions use let rec. This program declares its own List a and a recursive length, then calls the prelude's take/drop — both are generic over the element type with no trait bound at all: the compiler discovers each call site's concrete instantiation from its type annotation and monomorphizes it, so nothing polymorphic ever reaches the kernel.

-- ADR-0103: the bound-free `let rec` monomorphization pre-pass. `take`/`drop`
-- (Prelude.bang) are GENERIC over the element type (`Int -> List a -> List
-- a`, no trait bound) — the pre-pass discovers each call site's concrete
-- instantiation from its annotation and emits one monomorphic residue per
-- element, exactly witness w3's by-hand shape, auto-generated.
data List a = Nil | Cons(a, List a)
let rec length : List a -> Int =
  fun xs => match (xs : List a) { Nil -> 0, Cons(h, t) -> 1 + (($length) t) }
let nums = (Cons(1, Cons(2, Cons(3, Cons(4, Cons(5, Nil))))) : List Int) in
let firstThree = ($take 3) (nums : List Int) in
let lastTwo = ($drop 3) (nums : List Int) in
(($length) (firstThree : List Int)) * 100 + (($length) (lastTwo : List Int))

Expected output (bang run stdout):

Run it yourself:

curl -fsSL https://raw.githubusercontent.com/phibkro/bang/main/tools/install.sh | sh
bang run examples/list-basics/main.bang

← 1. Values are thunks; $ forces · 3. Your own data →