2022-07-14 05:19:47 +03:00
Kind2
=====
2022-09-02 19:40:09 +03:00
**Kind2** is a **functional programming language** and **proof assistant** .
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
It is a complete rewrite of [Kind1 ](https://github.com/kindelia/kind-legacy ), based on
[HVM ](https://github.com/kindelia/hvm ), a **lazy** , **non-garbage-collected** and **massively parallel** virtual
machine. In [our benchmarks ](https://github.com/kindelia/functional-benchmarks ), its type-checker outperforms every
alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
unleashes the [inherent parallelism of the Lambda
Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
the next century.
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
**Welcome to the inevitable parallel, functional future of computers!**
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
Examples
--------
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
Pure functions are defined via equations, as in [Haskell ](https://www.haskell.org/ ):
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
```javascript
// Applies a function to every element of a list
map < a > < b > (list: List a) (f: a -> b) : List b
map a b Nil f = Nil
2022-10-04 10:45:09 +03:00
map a b (Cons head tail) f = Cons (f head) (map tail f)
2022-07-19 04:47:18 +03:00
```
2022-12-01 17:33:54 +03:00
Side-effective programs are written via monads, resembling [Rust ](https://www.rust-lang.org/ ) and [TypeScript ](https://www.typescriptlang.org/ ):
2022-07-14 05:19:47 +03:00
2022-09-02 19:40:09 +03:00
```javascript
2022-09-21 13:15:33 +03:00
// Prints the double of every number up to a limit
2022-09-02 19:40:09 +03:00
Main : IO (Result () String) {
ask limit = IO.prompt "Enter limit:"
2022-07-23 20:56:54 +03:00
for x in (List.range limit) {
2022-09-02 19:40:09 +03:00
IO.print "{} * 2 = {}" x (Nat.double x)
2022-07-23 20:56:54 +03:00
}
2022-09-02 19:40:09 +03:00
return Ok ()
2022-07-23 20:56:54 +03:00
}
2022-07-14 05:19:47 +03:00
```
2022-09-02 19:40:09 +03:00
Theorems can be proved inductivelly, as in [Agda ](https://wiki.portal.chalmers.se/agda/pmwiki.php ) and [Idris ](https://www.idris-lang.org/ ):
```javascript
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
black_friday_theorem Nat.zero = Equal.refl
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
```
2022-07-23 20:56:54 +03:00
For more examples, check the [Wikind ](https://github.com/kindelia/wikind ).
2022-07-14 05:19:47 +03:00
2022-09-02 19:40:09 +03:00
Usage
-----
2022-07-14 05:57:15 +03:00
2022-09-02 19:40:09 +03:00
First, install [Rust ](https://www.rust-lang.org/tools/install ) first, then enter:
2022-07-19 04:47:18 +03:00
```
2022-07-23 20:56:54 +03:00
cargo install kind2
2022-07-19 04:47:18 +03:00
```
2022-12-01 17:33:54 +03:00
### Warning:
New versions probably are not in `cargo` , so you can install the current version of kind2 by following these instructions:
1. Install Rust Nightly Toolchain
2. Clone the repository
3. `cargo install --path crates/kind-cli --force`
2022-09-02 19:40:09 +03:00
Then, use any of the commands below:
2022-07-14 05:57:15 +03:00
2022-07-23 20:56:54 +03:00
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 ](https://github.com/kindelia/hvm ) file. Can then be compiled to C.
2022-09-02 19:40:09 +03:00
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl ](https://github.com/kindelia/kindelia ) file. Can then be deployed to [Kindelia ](https://github.com/kindelia/kindelia ).
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
Executables can be generated via HVM:
2022-07-19 04:47:18 +03:00
2022-09-02 19:40:09 +03:00
```
kind2 to-hvm file.kind2
hvm compile file.hvm
clang -O2 file.c -o file
./file
```