# Kind

A next-gen functional language
Alternatives To Kind
Kind3,058
3 days ago44mitRust
A next-gen functional language
Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
Magic In Ten Mins644
2 months ago2cc-by-4.0HTML

Fp Core.rs644
3 years ago25mitRust
A library for functional programming in Rust
Plam430
An interpreter for learning and exploring pure λ-calculus
Lambda287
3 years ago1JavaScript
🔮 Estudos obscuros de programação funcional
Lambda Talk246
3 years agomitJavaScript
A Flock of Functions: Combinators, Lambda Calculus, & Church Encodings in JS
Curryhoward232
2 years ago15August 23, 20215apache-2.0Scala
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Cognate164
3 months ago4bsd-2-clauseC
A human readable quasi-concatenative programming language
Y Combinator For Non Programmers145
3 months agoTypeScript
🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science
Alternatives To Kind
Select To Compare

Alternative Project Comparisons

Kind is a pure functional programming language and proof assistant.

# Getting started

It is a complete rewrite of Kind1, based on HVM, a lazy, non-garbage-collected and massively parallel virtual machine. In our 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 to become the ultimate programming language of the next century.

Welcome to the inevitable parallel, functional future of computers!

## Examples

Pure functions are defined via equations, as in Haskell:

``````// 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
Map a b (Cons head tail) f             = Cons (f head) (Map tail f)
``````

Theorems can be proved inductively, as in Agda and Idris:

``````// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
BlackFridayTheorem (n: Nat)     : Equal Nat (Nat.half (Nat.double n)) n
BlackFridayTheorem Nat.zero     = Equal.refl
BlackFridayTheorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (BlackFridayTheorem n)
``````

For more examples, check the Wikind.

# Installation

First, install Rust first, then enter:

``````cargo install kind2
``````

Then, use any of the commands below:

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 a rust crate using HVM.
To-KDL `kind2 to-kdl file.kind2` Generates a .kdl file. Can then be deployed to Kindelia.

The rust crate can be generated via HVM:

``````kind2 to-hvm file.kind2 > file.hvm
hvm compile file.hvm
``````

Popular Functional Programming Projects
Popular Lambda Calculus Projects
Popular Software Development Categories
Related Searches

Get A Weekly Email With Trending Projects For These Categories
No Spam. Unsubscribe easily at any time.
Rust
Functional Programming
Lambda Calculus
Dependent Types
Type Theory