bench | ||
example | ||
src | ||
.gitignore | ||
Cargo.lock | ||
Cargo.toml | ||
README.md |
Kind2
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.
Examples
Pure functions can be defined using an equational notation that resembles Haskell:
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:
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:
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.
Installation
Install Rust first, then enter:
cargo install kind2
Enter kind2
on the terminal to make sure it worked.
Usage
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. |
Benchmarks
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.