A cute proof and programming language.
npm i -g kind-lang # installs Kind
git clone https://github.com/uwu-tech/kind # clones base libs
cd Kind/base # enters base libs
kind Main # checks Main.kind
kind Main --run # runs Main
Right now, you must be at kind/base
to use the language.
Main: IO(Unit)
do IO {
IO.print("Hello, world!")
}
// List sum using recursion
sum(list: List(Nat)): Nat
case list {
nil : 0
cons : list.head + sum(list.tail)
}
// List sum using a fold
sum(list: List(Nat)): Nat
List.fold!(list)!(0, Nat.add)
// List sum using a loop
sum(list: List(Nat)): Nat
let sum = 0
for x in list:
sum = x + sum
sum
// A struct
type User {
new(name: String, birth: Date, avatar: Image)
}
// A simple pair
type Pair <A: Type> <B: Type> {
new(fst: A, snd: B)
}
// A dependent pair
type Sigma <A: Type> <B: A -> Type> {
new(fst: A, snd: B(fst))
}
// A list
type List <A: Type> {
nil
cons(head: A, tail: List(A))
}
// A list with a statically known size
type Vector <A: Type> ~ (size: Nat) {
nil ~ (size = 0)
cons(size: Nat, head: Nat, tail: Vector(A,size)) ~ (size = 1 + size)
}
// The propositional equality
type Equal <A: Type> <a: A> ~ (b: A) {
refl ~ (b = a)
}
// Proof that `a == a + 0`
Nat.add.zero(a: Nat): a == Nat.add(a, 0)
case a {
zero: refl
succ: apply(Nat.succ, Nat.add.zero(a.pred))
}!
// Proof that `1 + (a + b) == a + (1 + b)`
Nat.add.succ(a: Nat, b: Nat): Nat.succ(a + b) == (a + Nat.succ(b))
case a {
zero: refl
succ: apply(Nat.succ, Nat.add.succ(a.pred, b))
}!
// Proof that addition is commutative
Nat.add.comm(a: Nat, b: Nat): (a + b) == (b + a)
case a {
zero:
Nat.add.zero(b)
succ:
let p0 = Nat.add.succ(b, a.pred)
let p1 = Nat.add.comm(b, a.pred)
p0 :: rewrite X in Nat.succ(X) == _ with p1
}!
-
Syntax reference: SYNTAX.md.
-
Theorem proving tutorial: THEOREMS.md.
-
Base library: base.
-
Discord server (TODO)