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 based on optimal normalization-by-evaluation. It can also compile programs to HVM and Kindelia, and can be used to prove and verify mathematical theorems.
Pure functions can be defined using an equational notation that resembles Haskell:
idris
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))
Mathematical theorems can be proved via inductive reasoning, as in Idris and Agda:
idris
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)
Normal programs can be written in a monadic syntax that is inspired by Rust and TypeScript:
idris
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 ())
}
For more examples, check the Wikind.
Install Rust first, then enter:
cargo install kind2
Enter kind2 on the terminal to make sure it worked.
Command | Usage | Note
---------- | ------------------------- | --------------------------------------------------------------
Check | kind2 check file.kind2 | Checks all definitions.
Eval | kind2 eval file.kind2 | Runs using the type-checker's evaluator.
Run | kind2 run file.kind2 | Runs using HVM's evaluator, on Rust-mode.
To-HVM | kind2 to-hvm file.kind2 | Generates a .hvm file. Can then be compiled to C.
To-KDL | kind2 to-kdl file.kind2 | Generates a .kdl file. Can then be deployed to Kindelia.
In preliminary benchmarks, Kind2's type-checker has outperformed Agda, Idris by 90x to 900x, which is an expressive difference. That said, we only tested a few small programs, so there isn't enough data to draw a conclusion yet. We're working on a more extensive benchmark suite.