29d8338f4a
1. Previously, the following term wouldn't type-check:
match x = term {
true: ct
false: cf
}
When `term` isn't a variable.
The reason is that the `match` syntax was desugared to:
(~term _ ct cf)
Which, in general, results in the following check:
true : ∀(P: Bool -> *) ∀(t: P true) ∀(f: P false) (P term)
check _ :: Bool -> *
check ct :: (_ true)
check cf :: (_ false)
check () :: (_ term)
unify (_ term) == (P term)
This should generate the solution:
_ = λx(P x)
But, when `term` isn't a variable (it could be a function call, or a ref, for
example), this fails to satisfy the pattern unification criteria. To fix that,
we just use a `let` to always create a variable before unifying, so that the
`match` syntax is desugared to:
let x = term
(~x _ ct cf)
Which solves the issue.
2. Previously, the following term wouldn't type-check:
equal (a: Nat) (b: Nat) : Bool =
match a with (b: Nat) {
succ: match b {
succ: (equal a.pred b.pred)
zero: false
}
zero: match b {
succ: false
zero: true
}
}
After inspecting the type-checker output, I noticed the reason is due to how the
outer hole interacts with the inner hole. Specifically, after some computations
we eventually get to the following unification problem:
unify _2 == (_3 b)
Here, there are two ways to solve this:
_2 = (_3 b)
or
_3 = λx (_2)
Initially, it seems like both solutions are equivalent. Yet, by choosing the
first, we, later on, face the following problem:
- (_3 (succ x))
- Bool
Which violates the pattern unification requisites (for the same reason: `succ`
is a constructor, rather than a variable). A way to solve this problem would be
to simply invert the order, and use `_3 = λx (_2)` instead (done in the last
commit). That way, we'd have `(_3 (succ x))` reduce to just `_2`, which would
solve `_2 = Bool` and type-check fine. This is a quickfix though. I wonder if
there is a more principled approach that would let us avoid `(succ x)` to be
there at all.
Debug log: https://gist.github.com/VictorTaelin/6dd1a7167d5b7c8d5626c0f5b88c75a0
|
||
|---|---|---|
| book | ||
| docs | ||
| formal | ||
| src | ||
| .gitignore | ||
| Cargo.lock | ||
| Cargo.toml | ||
| README.md | ||
Kind2: a parallel proof & programming language
Kind2 is a general-purpose programming language made from scratch to harness HVM's massive parallelism and computational advantages (no garbage collection, optimal β-reduction). Its type system is a minimal core based on the Calculus of Constructions, making it inherently secure. In short, Kind2 aims to be:
-
As friendly as Python
-
As efficient as Rust
-
As high-level as Haskell
-
As parallel as CUDA
-
As formal as Lean
And it seeks to accomplish that goal by relying on the solid foundations of Interaction Combinators.
Usage
-
Clone this repository and install it:
git clone https://github.com/HigherOrderCO/Kind2 cargo install --path . -
Type-check a Kind2 definition:
kind2 check name_here -
Test it with the interpreter:
kind2 run name -
Compile and run in parallel, powered by HVM!
kind2 compile name ./name
Syntax
Kind2's syntax aims to be as friendly as Python's, while still exposing the
high-level functional idioms that result in fast, parallel HVM binaries.
Function application ((f x y z ...)) follows a Lisp-like style and
pattern-matching (match x { ctr: .. }) feels like Haskell; but control-flow is
more Python-like. In short, it can be seen as "Haskell inside, Python
outside": a friendly syntax on top of a powerful functional core.
Functions:
// The Fibonacci function
fib (n: U60) : U60 =
switch n {
0: 0
1: 1
_: (+ (fib (- n 1)) (fib (- n 2)))
}
Datatypes (ADTs):
// Polymorphic Lists
data List T
| cons (head: T) (tail: (List T))
| nil
// Applies a function to all elements of a list
map <A> <B> (xs: (List A)) (f: A -> B) : (List B) =
fold xs {
++: (f xs.head) ++ xs.tail
[]: []
}
Theorems and Proofs:
use Nat/{succ,zero,half,double}
// Proof that `∀n. n*2/2 = n`
bft (n: Nat) : (half (double n)) == n =
match n {
succ: (Equal/apply succ (bft n.pred))
zero: {=}
}
More Examples:
There are countless examples on the Book/ directory. Check it!