Kind/SYNTAX.md

Kind2 Syntax Guide

Kind2 is a minimal proof language based on the calculus of constructions, extended with self-types. This guide has been generated by Sonnet-3.5 and will be reviewed soon.

Basic Syntax

Comments

• Single-line comments: // Comment

Simple Datatype Declarations

data Nat
| zero
| succ (pred: Nat)

Polymorphic Datatypes

data List <T>
| cons (head: T) (tail: (List T))
| nil

Dependent Types

data Equal <A: Type> (a: A) (b: A)
| refl (a: A) : (Equal A a a)

data Sigma <A: Type> <B: A -> Type>
| new (fst: A) (snd: (B fst))

Function Definitions and Calls

Functions in Kind2 use Lisp-like call syntax, requiring parentheses: The matched variable's fields are automatically added to the scope:

add (a: Nat) (b: Nat) : Nat =
  match a {
    zero: b
    succ: (succ (add a.pred b))
  }

// Function call
(add (succ zero) (succ (succ zero)))

Advanced Features

Generic Functions

List/fold <A> <B> (xs: (List A)) (c: A -> B -> B) (n: B) : B =
  match xs {
    ++: (c xs.head (List/fold xs.tail c n))
    []: n
  }

Note that ++ and [] are shortcuts for List/cons and List/nil.

Universal Quantification

Use ∀ or forall:

∀(A: Type) ∀(B: Type) ...

Lambda Functions

Use λ or lambda:

λx (x + 1)

Implicit Arguments

Use <> for erased implicit arguments:

id <T: Type> (x: T) : T = x

Metavariables

Represented by _, metavariables allow the compiler to fill parts of the program automatically:

(id _ 7)  // The compiler will infer the type argument

Named Holes

Use ?name for debugging and inspection. This will cause the context around the hole to be printed in the console:

(function_call ?hole_name)

Operators

• Arithmetic: +, -, *, /, %
• Comparison: ==, !=, <, <=, >, >=
• Logical: &&, ||, !

Type Universe

Use Type or * to denote the type of types

Module System

Use dot notation for accessing module members:

(List/map (Nat/add 1) my_list)

Self Types

Self types allow a type to access its typed value, bridging value and type levels.

Self Type Introduction

Use $ to introduce a self type:

$(self: T) X

Self Type Instantiation

Use ~ to instantiate a self type:

(~some_self_type_value)

Self-Encoded Versions of Earlier Types

List (Self-Encoded)

List (A: *) : * =
  $(self: (List A))
  ∀(P: (List A) -> *)
  ∀(cons: ∀(head: A) ∀(tail: (List A)) (P (List/cons/ A head tail)))
  ∀(nil: (P (List/nil/ A)))
  (P self)

List/cons/ <A: *> (head: A) (tail: (List A)) : (List A) =
  ~λP λcons λnil (cons head tail)

List/nil/ <A: *> : (List A) =
  ~λP λcons λnil nil

Pattern Matching as Self-Instantiation

Pattern matching desugars to self-instantiation of a λ-encoding:

// This pattern match:
match x {
  nil: foo
  cons: (bar x.head x.tail)
}

// Desugars to:
(~x foo (λhead λtail (bar head tail)))