Examples

fn main() {
  println("Hello, kaikai")
}

type Tag
  = Both
  | Fizz
  | Buzz
  | Other(Int)

# Guards let every arm carry its own condition, so the cascade of
# `if / else if` collapses into the match itself.
fn classify(n: Int) : Tag = match n {
  n if n % 15 == 0 -> Both
  n if n % 3 == 0  -> Fizz
  n if n % 5 == 0  -> Buzz
  n                -> Other(n)
}

fn label(c: Tag) : String = match c {
  Both     -> "FizzBuzz"
  Fizz     -> "Fizz"
  Buzz     -> "Buzz"
  # String interpolation: `#{expr}` renders any displayable value.
  Other(n) -> "#{n}"
}

fn main() {
  [1..15]
    | classify  # map: [Int] -> [Tag]
    | label     # map: [Tag] -> [String]
    |! println  # each: print each line
}

type Expr
  = Lit(Int)
  | Add(Expr, Expr)
  | Mul(Expr, Expr)
  | Neg(Expr)

# A function whose whole body is one expression uses `=`; no braces,
# no `return`.
fn eval(e: Expr) : Int = match e {
  Lit(n)    -> n
  Add(l, r) -> eval(l) + eval(r)
  Mul(l, r) -> eval(l) * eval(r)
  Neg(x)    -> -eval(x)
}

fn show(e: Expr) : String = match e {
  Lit(n)    -> "#{n}"
  Add(l, r) -> "#{show(l)} + #{show(r)}"
  Mul(l, r) -> "#{show(l)} * #{show(r)}"
  Neg(x)    -> "-#{show(x)}"
}

fn main() {
  let e = Add(Lit(2), Mul(Lit(3), Lit(4)))
  println("#{show(e)} = #{eval(e)}")
}

effect Log {
  log(msg: String) : Unit
}

fn greet(name: String) : Unit / Log {
  # `#{...}` interpolates into the string, with no manual concatenation.
  Log.log("hello, #{name}")
}

fn main() {
  handle {
    greet("kaikai")
    greet("world")
  } with Log {
    log(msg, resume) -> {
      println("[INFO] #{msg}")
      resume(())
    }
  }
}

import spawn
import loop

fn worker(tag: String, n: Int) : Unit / Stdout + Spawn {
  loop.repeat(n) {
    println(tag)
    spawn.yield()
  }
}

fn main() {
  # Trailing-lambda form: `spawn.spawn { ... }` instead of
  # `spawn.spawn(() => ...)`.
  let f = spawn.spawn { worker("B", 3) }
  worker("A", 3)
  spawn.await(f)
}

fn square(n: Int) : Int = n * n

fn divisors(n: Int) : [Int] = [1, n]

fn is_even(n: Int) : Bool = n % 2 == 0

fn main() {
  # `[1..4]` is a range literal: no hand-written accumulator loop.
  # `[1..10..2]` adds a step.
  let total = [1..4]                  # [1, 2, 3, 4]
    | square                          # [1, 4, 9, 16]      (map)
    || divisors                       # [1, 1, 1, 4, 1, 9, 1, 16] (flat-map)
    |? is_even                        # [4, 16]            (filter)
    |> list.sum                       # 20                 (apply)

  println("total=#{total}")
}

unit USD
unit EUR

fn to_usd(amount: Real<EUR>, rate: Real<USD/EUR>) : Real<USD>
  = amount * rate

fn main() {
  let salary    : Real<USD> = 1000.0<USD>
  let groceries : Real<USD> =  250.0<USD>
  let fee       : Real<USD> =    5.0<USD>
  let refund    : Real<EUR> =   91.0<EUR>
  let rate      : Real<USD/EUR> = 1.10<USD/EUR>

  let balance = salary - groceries - fee + to_usd(refund, rate)

  # 1000 - 250 - 5 + 100.1 = 845.1 USD
  println("balance=#{balance}")
}

unit m

# `Measure` is declared over `AbelianGroup`, which has multiplicative
# closure: metres times metres is a real quantity, so `u^2` is a unit
# you can name. `[u: Measure]` is an ordinary type parameter that
# ranges over units instead of over types.
fn area[u: Measure](w: Real<u>, h: Real<u>) : Real<u^2> = w * h

# Because units are only a kind, the machinery is open: declare your
# own. Experience points add up, but `xp^2` is meaningless, so this
# kind is declared over `Module`: an additive group with NO
# multiplicative closure. A quantity is either scalar or carries
# exactly one habitant, and `fn sq(a: Real<xp>) : Real<xp^2>` is
# rejected at the point the unit is written:
#
#   error: unit `xp^2` does not exist: `Points` habitants have no
#          products or powers
#
# Same machinery as `Measure`, different theory, different algebra.
kind Points : Module with points
points xp

fn gain(a: Real<xp>, b: Real<xp>) : Real<xp> = a + b

fn main() {
  let floor = area(3.0<m>, 4.0<m>)
  let score = gain(120.0<xp>, 45.0<xp>)

  # Habitants of different kinds never unify either: `3.0<m> +
  # 4.0<xp>` is a type error. Your kind cannot leak into anyone
  # else's.
  println("floor=#{floor}")
  println("score=#{score}")
}

fn divide(a: Int, b: Int) : Int
  requires b != 0
  ensures  result * b == a
{
  a / b
}

# Absolute value: the postcondition guarantees a non-negative result
# of the same magnitude as the argument.
fn abs(n: Int) : Int
  ensures result >= 0
  ensures result == n or result == -n
{
  if n >= 0 { n } else { -n }
}

fn main() {
  println("#{divide(10, 2)}")   # 5
  println("#{abs(-3)}")         # 3
}