mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
A next-gen functional language
dependent-typesformalityfunctional-programminglambda-calculusmoonadproof-languageproof-languagesstarred-kindelia-repostarred-repotheorem-provertype-theory
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 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.
Example
Kind2 functions can be defined using an equational notation that is highly inspired by Haskell, Idris and Agda:
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:
// 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:
// 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.
Usage
- Install:
cargo install --path .
- Check a Kind2 file:
kind2 check example.kind2
- Eval the Main term:
kind2 eval example.kind2
- Compile to HVM:
kind2 to-hvm example.kind2
- Compile to Kindelia:
kind2 to-kdl example.kind2
Benchmarks
Type-Checker
TODO
Runtime
TODO