kind2 0.2.37

A pure functional functional language that uses the HVM.
kind2-0.2.37 is not a library.
Visit the last successful build: kind2-0.2.79

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.