Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose, dependently typed programming language focusing on performance and usability. It features a blazingly fast type-checker that runs on the HVM via NbE. It can also compile programs to HVM and Kindelia, and can be used to prove and verify mathematical theorems.
Kind2 functions can be defined using an equational notation that is highly inspired by Haskell, Idris and Agda:
c
List.map <a: Type> <b: Type> (x: (List a)) (f: (x: a) b) : (List b)
List.map a b (Nil t) f = (Nil b)
List.map a b (Cons t x xs) f = (Cons b (f x) (List.map xs f))
But they can also be defined in a conventional notation that is highly inspired by Rust and TypeScript:
c
// Note: syntax on development
// Prints the double of many numbers
Main : (IO (Result () String)) {
ask limit = (IO.prompt "Enter limit:");
for x in (List.range limit) {
(IO.print "{} * 2 = {}" x (Nat.double x));
}
return (Ok ());
}
Mathematical proofs are present as well:
c
// For every number `a` and `b`, `a + b == b + a`
Nat.commutes (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
Nat.commutes Zero b = (Nat.comm.a b)
Nat.commutes (Succ a) b =
let e0 = (Equal.apply @x(Succ x) (Nat.commutes a b))
let e1 = (Equal.mirror (Nat.commutes.b b a))
(Equal.chain e0 e1)
For more examples, check /example.
cargo install --path .
kind2 check example.kind2
kind2 eval example.kind2
kind2 to-hvm example.kind2
kind2 to-kdl example.kind2
TODO
TODO