A functional language with algebraic effects and isolated fibers. No garbage collector, no borrow checker.

Designed to be written with — and by — agents.

why this name?

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

fn greet(name: String) : Unit / Log {
  Log.log("hello, #{name}")
}

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

Why kaikai

Algebraic effects

Effects visible in the type, composable handlers. No async/await infecting the whole call stack.

Pipe family

Four operators, four intents: |> applies, | maps, || flat-maps, |? filters. Each form tells you what it does before you read the function.

No GC, no borrow checker

Perceus reference counting + isolated fibers. Memory is per-fiber; no global pauses.

Kinds: units, currencies, regions

Real<m/s> for measures, currencies that never mix, arenas via region { }. Information in the type, zero runtime cost.

Contracts & refinements

requires, ensures, Int where >= 0. What SPARK does, without an SMT solver.

Dialogue with the compiler

Holes (?), --holes-json, structured diagnostics. Designed for humans and agents to write together.

Examples

Seven programs that show the shape of the language. All run with kai run.

01_hello.kai
# Hello, world.
#
# Every kaikai program starts at `fn main()`. `println` is the
# default-handled stdout effect — no `import` needed.
#
#   $ kai run examples/quickstart/01_hello.kai
#   Hello, kaikai

fn main() {
  println("Hello, kaikai")
}
02_fizzbuzz.kai
# FizzBuzz.
#
# Sum types + pattern match, expressed as a pipeline instead of a
# hand-written recursion: `[1..15]` is a range literal, `|` maps over
# the list, and `|>` applies a function to the whole list.
#
#   $ kai run examples/quickstart/02_fizzbuzz.kai
#   1
#   2
#   Fizz
#   4
#   Buzz
#   ...
#   FizzBuzz

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]
    |> list.foreach(println)  # apply: print each line
}
04_effect.kai
# Custom effect with a handler.
#
# Algebraic effects are kaikai's differentiator: a function declares
# the effects it uses in its type, and any caller has to either also
# declare them, or install a handler that provides them.
#
# Below, `Log` is a custom effect with one op, `log(msg)`. `greet`
# uses it but doesn't say HOW logging happens. `main` decides at
# call time: prefix every log with `[INFO]` and route to stdout.
#
#   $ kai run examples/quickstart/04_effect.kai
#   [INFO] hello, kaikai
#   [INFO] hello, world

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

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

fn main() {
  handle {
    greet("kaikai")
    greet("world")
  } with Log {
    log(msg, resume) -> {
      println("[INFO] #{msg}")
      resume(())
    }
  }
}
06_pipes.kai
# Pipe family: four operators, four intents.
#
#   |>   apply       apply a function to the left-hand value
#   |    map         map over the collection
#   ||   flat-map    map and flatten the result
#   |?   filter      keep elements that satisfy the predicate
#
#   $ kai run examples/quickstart/06_pipes.kai
#   total=20

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}")
}
07_uom.kai
# Units of measure: arithmetic that doesn't mix currencies.
#
# Units live in the type. The compiler rejects adding USD to EUR;
# converting between currencies requires an explicit step.
#
# `unit` is not a bolted-on feature: it mints a habitant of the kind
# `Measure`. See the kinds example for what that buys you.
#
#   $ kai run examples/quickstart/07_uom.kai
#   balance=845.1 USD

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}")
}
09_kinds.kai
# Kinds: units of measure are not a special case.
#
# Types classify values; kinds classify types.
#
#   42     : Int       a value, and its type
#   Int    : Type      a type,  and its kind
#   m      : Measure   a unit,  and its kind
#
# So `unit m` is not special syntax bolted onto the compiler. It mints
# a habitant of the kind `Measure`, exactly the way `type` mints one
# of `Type` and `effect` mints one of `Effect`. Units of measure are
# just the kind `Measure` — nothing more.
#
# Every kind is declared over a *theory*, and the theory is what
# decides the algebra its habitants obey. That choice is the whole
# design surface, so pick it to match the domain.
#
#   $ kai run examples/quickstart/09_kinds.kai
#   floor=12 m^2
#   score=165 xp

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}")
}
08_contracts.kai
# Contracts: preconditions and postconditions in the signature.
#
# `requires` rejects callers passing invalid arguments.
# `ensures` demands the result satisfy a property.
# Inside `ensures`, the name `result` refers to the returned value.
#
#   $ kai run examples/quickstart/08_contracts.kai
#   5
#   3

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
}