3.0 KiB
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)))