Algebraic effects
Effects visible in the type, composable handlers. No async/await infecting the whole call stack.
A functional language with algebraic effects and isolated fibers. No garbage collector, no borrow checker.
Designed to be written with — and by — agents.
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(())
}
}
}Effects visible in the type, composable handlers. No async/await infecting the whole call stack.
Four operators, four intents: |> applies, | maps, || flat-maps, |? filters. Each form tells you what it does before you read the function.
Perceus reference counting + isolated fibers. Memory is per-fiber; no global pauses.
Real<m/s> for measures, currencies that never mix, arenas via region { }. Information in the type, zero runtime cost.
requires, ensures, Int where >= 0. What SPARK does, without an SMT solver.
Holes (?), --holes-json, structured diagnostics. Designed for humans and agents to write together.
Seven programs that show the shape of the language. All run with kai run.
# 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")
}# 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
}# 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(())
}
}
}# 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}")
}# 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}")
}# 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}")
}# 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
}