Update ADT param syntax; update many things (WIP)

README.md

@@ -1,26 +1,10 @@
 # Kind2: a parallel proof & programming language
 
-> NOTE: THIS REPOSITORY IS A WIP. OFFICIAL RELEASE COMING SOON!
-
-Kind2 is a general-purpose programming language made from scratch to harness
-[HVM](https://github.com/HigherOrderCO/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. Essentially, 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](https://www.semanticscholar.org/paper/Interaction-Combinators-Lafont/6cfe09aa6e5da6ce98077b7a048cb1badd78cc76).
-
-
+Kind2 is a minimalist proof language based on [Self
+types](https://cse.sc.edu/~pfu/document/papers/rta-tlca.pdf), a simple extension
+to the Calculus of Constructions that allows encoding inductive types without a
+complex, hardcoded datatype system. It compiles to
+[Bend](https://github.com/HigherOrderCO/Bend).
 
 ## Usage
 
@@ -52,16 +36,7 @@ And it seeks to accomplish that goal by relying on the solid foundations of [Int
     ./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:
+## Examples
 
 ```javascript
 // The Fibonacci function
@@ -104,4 +79,4 @@ bft (n: Nat) : (half (double n)) == n =
 
 ### More Examples:
 
-There are countless examples on the [`Book/`](book) directory. Check it!
+There are countless examples on the [`Book/`](book) directory.

book/Bool/and.kind2

@@ -2,6 +2,6 @@ use Bool/{true,false,and}
 
 and (a: Bool) (b: Bool) : Bool =
   match a {
-    true: b
+    true: "foo"
     false: false
   }

book/Bool/lemma/double_negation.kind2

@@ -1,7 +1,4 @@
 use Bool/{true,false,not}
 
-double_negation (x: Bool) : (not (not x)) == x =
-  match x {
-    true: {=}
-    false: {=}
-  }
+double_negation (x: Bool) : (Equal Bool (not (not x)) x) =
+  ?a

book/Bool/match.kind2

@@ -1,9 +1,9 @@
 use Bool/{true,false}
 
 match
-  (b: Bool)
   (P: ∀(x: Bool) *)
   (t: (P true))
   (f: (P false))
+  (b: Bool)
 : (P b)
 = (~b P t f)

book/Cmp/gtn.kind2

@@ -1,2 +1,2 @@
-Cmp.gtn : Cmp =
+Cmp/gtn : Cmp =
   ~λP λltn λeql λgtn gtn

book/Cmp/ltn.kind2

@@ -1,2 +1,2 @@
-Cmp.ltn : Cmp =
+Cmp/ltn : Cmp =
   ~λP λltn λeql λgtn ltn

book/Equal.kind2

@@ -1,4 +1,4 @@
-data Equal T (a: T) (b: T)
+data Equal <T> (a: T) (b: T)
 | refl (a: T) : (Equal T a a)
 
 //Equal : ∀(T: *) ∀(a: T) ∀(b: T) * =
@@ -7,7 +7,3 @@ data Equal T (a: T) (b: T)
   //∀(P: ∀(a: T) ∀(b: T) ∀(x: (Equal T a b)) *)
   //∀(refl: ∀(x: T) (P x x (Equal/refl T x)))
   //(P a b self)
-
-//Equal
-//: ∀(A: *) ∀(a: A) ∀(b: A) *
-//= λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)

book/Equal/match.kind2

@@ -4,3 +4,15 @@ match <T: *> <a: T> <b: T>
   (e: (Equal T a b))
 : (P a b e) =
   (~e P refl)
+
+can you understand this?
+
+Yes, this appears to be a dependently-typed pattern matching function, likely written in a language similar to Idris, Agda, or Coq. It's implementing the principle of indiscernibility of identicals, also known as Leibniz's law. Here's a brief explanation:
+
+1. It takes two values `a` and `b` of some type `T`.
+2. It takes a predicate `P` that depends on two values of type `T` and a proof of their equality.
+3. It takes a proof `refl` that the predicate holds for any value `x` when compared to itself.
+4. It takes a proof `e` that `a` and `b` are equal.
+5. It returns a proof that the predicate `P` holds for `a`, `b`, and the equality proof `e`.
+
+The implementation uses the equality proof `e` to rewrite the goal, effectively turning it into `P a a (Equal/refl/ T a)`, which can be solved by the `refl` argument.

book/Kind.kind2

@@ -30,4 +30,4 @@ Kind
   use some = λvalue (Kind.Term.show value Nat.zero)
   use none = "error"
   use chk = (Kind.check test Test Nat.zero)
-  (~chk P some none)
+  (~chk P some none)

book/List.kind2

@@ -1,3 +1,3 @@
-data List T
+data List <T>
 | cons (head: T) (tail: (List T))
 | nil

book/Nat/double.kind2

@@ -2,6 +2,6 @@ use Nat/{succ,zero}
 
 double (n: Nat) : Nat =
   match n {
-    succ: (succ (succ (double n.pred)))
+    succ: (succ (succ (double succ)))
     zero: #0
   }

book/Sigma.kind2

@@ -1,7 +1,11 @@
-Sigma
-: ∀(A: *) ∀(B: ∀(x: A) *) *
-= λA λB
-  $(self: (Sigma A B))
-  ∀(P: ∀(x: (Sigma A B)) *)
-  ∀(new: ∀(a: A) ∀(b: (B a)) (P (Sigma.new A B a b)))
-  (P self)
+data Sigma <A: *> <B: A -> *>
+| new (fst: A) (snd: (B fst))
+
+// λ-encoded version:
+//Sigma
+//: ∀(A: *) ∀(B: ∀(x: A) *) *
+//= λA λB
+ //$(self: (Sigma A B))
+ //∀(P: ∀(x: (Sigma A B)) *)
+ //∀(new: ∀(a: A) ∀(b: (B a)) (P (Sigma/new A B a b)))
+ //(P self)

book/Sigma/new.kind2

@@ -1,4 +1,4 @@
-Sigma.new
+Sigma/new
 : ∀(A: *) ∀(B: ∀(x: A) *) ∀(a: A) ∀(b: (B a))
   (Sigma A B)
-= λA λB λa λb ~λP λnew (new a b)
+= λA λB λa λb ~λP λnew (new a b)

book/_check_all.sh

@@ -1,4 +1,13 @@
-for file in $(ls *.kind2 | grep -v '^_'); do
+#for file in $(ls *.kind2 | grep -v '^_'); do
+  #echo "checking ${file}"
+  #kind2 check "${file%.*}"
+#done
+
+# TODO: make this script check all kind2 files recursively, not just top-dir ones
+
+#!/bin/bash
+
+find . -name "*.kind2" -not -name "_*" | while read -r file; do
   echo "checking ${file}"
   kind2 check "${file%.*}"
 done

book/main.kind2

@@ -1,5 +0,0 @@
-use Nat/{succ,zero}
-
-main : (List U60) =
-  let list = [10, 20]
-  list

src/book/parse.rs

@@ -52,8 +52,8 @@ impl<'i> KindParser<'i> {
         typ = Term::All { era: false, nam: idx_nam.clone(), inp: Box::new(idx_typ.clone()), bod: Box::new(typ) };
         val = Term::Lam { era: false, nam: idx_nam.clone(), bod: Box::new(val) };
       }
-      for par_nam in adt.pars.iter().rev() {
-        typ = Term::All { era: false, nam: par_nam.clone(), inp: Box::new(Term::Set), bod: Box::new(typ) };
+      for (par_nam, par_typ) in adt.pars.iter().rev() {
+        typ = Term::All { era: false, nam: par_nam.clone(), inp: Box::new(par_typ.clone()), bod: Box::new(typ) };
         val = Term::Lam { era: false, nam: par_nam.clone(), bod: Box::new(val) };
       }
       //println!("NAM: {}", adt.name);

src/sugar/mod.rs

@@ -17,7 +17,7 @@ pub struct Equal {
 #[derive(Debug, Clone)]
 pub struct ADT {
   pub name: String,
-  pub pars: Vec<String>, // parameters
+  pub pars: Vec<(String,Term)>, // parameters
   pub idxs: Vec<(String,Term)>, // indices
   pub ctrs: Vec<Constructor>, // constructors
 }
@@ -70,7 +70,7 @@ pub struct Match {
 //
 // The Vector type:
 //
-//   data Vector A (len: Nat)
+//   data Vector <A: *> (len: Nat)
 //   | nil : (Vector A zero)
 //   | cons (len: Nat) (head: A) (tail: (Vector A len)) : (Vector A (succ len))
 //
@@ -400,7 +400,7 @@ impl Term {
     let name: String;
     let pvar: String;
 
-    let mut pars: Vec<String> = Vec::new();
+    let mut pars: Vec<(String,Term)> = Vec::new();
     let mut idxs: Vec<(String,Term)> = Vec::new();
     let mut ctrs: Vec<Constructor> = Vec::new();
     let mut term = self;
@@ -448,7 +448,7 @@ impl Term {
         // Collects the wit's parameters (remaining Apps)
         while let Term::App { era: _, fun: wit_inp_fun, arg: wit_inp_arg } = &**wit_inp {
           if let Term::Var { nam: parameter } = &**wit_inp_arg {
-            pars.push(parameter.to_string());
+            pars.push((parameter.to_string(), Term::Met {})); // FIXME: fill type
             wit_inp = wit_inp_fun;
           } else {
             return None;
@@ -531,8 +531,8 @@ impl Term {
     let mut self_type = Term::Var { nam: adt.name.clone() };
 
     // Then appends each type parameter
-    for par in adt.pars.iter() {
-      self_type = Term::App { era: false, fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par.clone() }) };
+    for (par_name, _) in adt.pars.iter() {
+      self_type = Term::App { era: false, fun: Box::new(self_type), arg: Box::new(Term::Var { nam: par_name.clone() }) };
     }
 
     // And finally appends each index
@@ -598,7 +598,7 @@ impl Term {
 
       // For each type parameter
       // NOTE: Not necessary anymore due to auto implicit arguments
-      for par in adt.pars.iter() {
+      for (par, _) in adt.pars.iter() {
         ctr_type = Term::App {
           era: true,
           fun: Box::new(ctr_type),
@@ -694,8 +694,12 @@ impl ADT {
     let mut adt_head = vec![];
     adt_head.push(Show::text("data"));
     adt_head.push(Show::text(&self.name));
-    for par in self.pars.iter() {
-      adt_head.push(Show::text(par));
+    for (nam,typ) in self.pars.iter() {
+      adt_head.push(Show::call("", vec![
+        Show::glue("", vec![Show::text("<"), Show::text(nam), Show::text(": ")]),
+        typ.format_go(),
+        Show::text(">"),
+      ]));
     }
     for (nam,typ) in self.idxs.iter() {
       adt_head.push(Show::call("", vec![
@@ -733,7 +737,7 @@ impl ADT {
         Show::call(" ", {
           let mut ret_typ = vec![];
           ret_typ.push(Show::text(&format!("({}", &self.name)));
-          for par in &self.pars {
+          for (par,_typ) in &self.pars {
             ret_typ.push(Show::text(par));
           }
           for idx in &ctr.idxs {
@@ -764,11 +768,19 @@ impl<'i> KindParser<'i> {
     let mut uses = uses.clone();
     // Parses ADT parameters (if any)
     self.skip_trivia();
-    while self.peek_one().map_or(false, |c| c.is_ascii_alphabetic()) {
+    while self.peek_one() == Some('<') {
+      self.consume("<")?;
       let par = self.parse_name()?;
-      self.skip_trivia();
+      let par_type = if self.peek_one() == Some(':') {
+        self.consume(":")?;
+        Some(self.parse_term(fid, &uses)?)
+      } else {
+        None
+      };
+      self.consume(">")?;
       uses = shadow(&par, &uses);
-      pars.push(par);
+      pars.push((par, par_type.unwrap_or(Term::Met {})));
+      self.skip_trivia();
     }
     // Parses ADT fields
     while self.peek_one() == Some('(') {
@@ -814,7 +826,7 @@ impl<'i> KindParser<'i> {
           // Parses the type (must be fixed, equal to 'name')
           self.consume(&name)?;
           // Parses each parameter (must be fixed, equal to 'pars')
-          for par in &pars {
+          for (par,_typ) in &pars {
             self.consume(par)?;
           }
           // Parses the indices