Kind2/SYNTAX.md

All syntaxes

This document lists all the high-level syntaxes available on the Kind language. Every syntax listed below is expanded (desugared) to either a primitive FormCore term, or to one of the functions available on the base library. Also, check this answer on Hacker News for some thoughts and reasonings about our syntax choices.

Top-level definition

name(arg0: type0, arg1: type1): return_type
  return_body

...

Kind programs and proofs are composed of a number of top-level definitions containing a name, followed by a number of arguments, followed by a :, followed by a return_type, followed by a return_body. For example:

my_name: String
  "Victor"

Creates a top-level definition called my_name, of type String and value "Victor". And:

get_first(fst: String, snd: String): String
  fst

Creates a top-level function called get_first, which receives two arguments, fst and snd of type String, and returns a String, which is the first argument.

The name of the top level definition also specifies the file where the definition is. For example Physics.Verlet.step must be either in base/Physics.kind or base/Physics/Verlet.kind or base/Physics/Verlet/step.kind.

Top-level definitions and datatype declarations (described below) are the only syntaxes that aren't expressions, which mean they can't appear anywhere in the program and, instead, must appear at the "global scope" of a file.

Lambda

(x) body

A lambda represents an inline function. It is written using a parenthesis, followed by a name, followed by a closing parenthesis, followed by the function body. There is no arrow (=>) in Kind's lambdas.

Multi-argument lambdas can be written by separating multiple names by commas. They are expanded to multiple lambdas. For example:

(x,y,z) body

The code above is the same as:

(x) (y) (z) body

There are no true multi-argument lambdas in Kind, this syntax is a mere convenience.

Lambdas can also be written using <x> body instead of (x) body. You can also omit the name and write just () body. As with applications, the difference is merely stylistic.

Application

func(argm)

A function application is written using the conventional mathematical syntax, f(x). There can be no spaces between the function and the parenthesis, thus, f (x) is not allowed. If you want to apply a bigger expression to an argument, you can wrap () around it. For example: ((x) body)(argm) would apply the (x) body function to argm.

A function application can also be written using <> instead of (). There is no difference other than style, but it is usually a good practice to use <> for type arguments.

An application to a hole can also be written as fn!, which expands to fn(_).

Like multi-argument lambdas, multi-argument applications can be written using comma-separated arguments. For example:

fn(x,y,z)

The code above is expanded to:

fn(x)(y)(z)

Let

let x = value
body

Let expressions define local values. They allow an expression to be reused multiple times, and computed only once at runtime. For example:

let x = heavy(1000000)
x + x

Will only evaluate heavy(1000000) once. Since let is just an expression, you can chain it any way you like. A ; can be used for clarity to separate the value and the body, and () can be used to wrap an inline let expression, but neither are mandatory.

let a = 1
let b = (let x = 2; x)
let c = 3
a + b + c

A let expression introduces a new variable in the context. That variable will appear in error messages and is not considered equal to the expression it assigns (for theorem proving and type-aliasing purposes).

The let can be omitted, so you could write just:

a = 1
b = 2
c = 3
a + b + c

Def

def x = value
body

Def expressions also define local values. The only difference is that these expressions will be expanded at compile-time. In other words, the program below:

def x = f(42)
x + x

Is identical to:

f(42) + f(42)

And f(42) will be computed twice at runtime. One advantage of def is that it doesn't introduce a new variable to the context, so the type checker will consider it equal to the expression it binds.

Forall (self-dependent function type)

self(name: type) -> body

Forall, or Pi, or self-dependent function, is the type of a function.

Nat.add(n: Nat, m: Nat): Nat

Nat.add is a function which takes two Nats and returns its sum.

Bool.double_negation(b: Bool): Equal(Bool, Bool.not(Bool.not(b)), b)

Bool.double_negation is a proof that for all Bool, its double negation is equal to itself.

Since Kind functions are self-dependently typed, you can optionally give a name to the input variable, and to the value of the function itself. For example,

(n: Nat) -> Vector(Bool, n)

Is the type of a function that receives a n: Nat and returns a Vector of n Bools.

If you're not using self-dependent types, you can omit the names, parenthesis and colon, and write just:

Nat -> Nat

Which is a function that receives a Nat and returns a Nat.

Datatype

type Name (A: Par0, B: Par1 ...) ~ (i: Idx0, j: Idx1 ...) {
  ctor0(field0: Fld0, field1: Fld1 ...) ~ (i = id0, j = idx1 ...)
  ctor1(field0: Fld0, field1: Fld1 ...) ~ (i = id0, j = idx1 ...)
  ...
}

Declares an inductive algebraic datatype. A simple datatype starts with the type keyword, followed by its name, followed by any number of parameters ("static polymorphic types"). Inside {} follows any number of constructors, each one is followed by its fields.

As an example, the following type, in Haskell:

data List a = Nil | Cons a (List a)

Can be written in Kind as:

type List (A: Type) {
  nil
  cons(head: A, tail: List(A))
}

We can have more complex types as the following type, in Agda:

data Vector <A : Set> : (size : Nat) -> Set where
  nil  : Vector A zero
  cons : (n : Nat) -> (head : A) -> (tail : Vector A n) -> Vector A (succ n)

That can be written in Kind as:

type Vector <A: Type> ~ (size: Nat) {
  nil                                      ~ (size = zero)
  cons(n: Nat, head: A, tail: Vector(A,n)) ~ (size = succ(n))
}

Where ~ (it's optional) stands for any number of indices ("dynamic polymorphic types"). In the constructor, its fields are also optionally followed by ~ and its concrete indices.

For more examples, check the common types (Maybe, Either, Nat, Vector, List, Equal, etc.) on https://github.com/uwu-tech/Kind/tree/master/base.

Case (pattern matching)

case val0 as name0; val1 as name1 ... valN as nameN
with expr0: type0; expr1: type1 {
  case0: result0
  case1: result1
  ...
  caseN: resultN
} : motive

Kind's case is the most important syntax of the language, as it allows one to branch, extract values from datatypes, and prove theorems. In its most basic form, it allows you to branch based on a datatype's constructor:

let x = true
case x {
  true: "x is true"
  false: "x is false"
}

When a matched constructor has fields, you can access it on the respective branch as name.field. For example, when matching a List, we gain access to its head and tail as list.head and list.tail:

sum(list: List<Nat>): Nat
  case list {
    nil: 0
    cons: list.head + sum(list.tail)
  }

When the matched expression isn't a name, you can provide one with as:

case [1,2,3] as list {
  nil: 0
  cons: list.head
}

You can use default to omit missing cases:

case list {
  cons: list.head
} default 0

You may pattern-match multiple values:

let x = true
let y = false
case x y {
  true  true  : "both are true"
  true  false : "one is true"
  false true  : "one is true"
  false false : "none is true
}

You may also provide a return type, called motive. Since Kind has dependent types, the motive has access to the value of the matched variable, allowing you to return a different type on each branch. For example:

let x = true
case x {
  true: "im a string"
  false: 42
}: if x then String else Nat

Here, Kind evaluated if x then String else Nat with each possible value of x (in this case, true or false) to determine the return type of each branch. Notice that the true case and the false case return different types. This is very useful for theorem proving. For example:

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: ?a
    false: ?b
  }

To prove this theorem, Kind demands you to provide a proof of not(not(b))==b on both cases. This isn't possible. But if you write a motive:

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: ?a
    false: ?b
  }: Bool.not(Bool.not(b)) == b

Then Kind demands a proof of not(not(true))==true on the ?a branch, and a proof of not(not(false))==false on the ?b branch. Since these equalities reduce to true==true and false==false, you can complete the proof with just refl.

When the motive is just a copy of the inferred type, you can write ! instead:

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: refl
    false: refl
  }!

Sometimes, though, we have variables on the context that refer to other variables, and we want to specialize their types just like we did with the goal. For example, on the proof below:

some_theorem(x: Bool, y: Bool, e: x == y): String
  case x {
    true: ?a
    false: ?b
  }!

Both branches have a e: x == y on the context. But the value of x on each case is known, so, we can "pass e down" using with:

some_theorem(x: Bool, y: Bool, e: x == y): String
  case x with e {
    true: ?a
    false: ?b
  }!

This will send e: true == y to the first branch, and e: false == y to the second branch. The code above works by creating an extra lambda, it is equivalent to:

some_theorem(x: Bool, y: Bool, e: x == y): String
  (case x {
    true: (e) ?a
    false: (e) ?b
  }: (e: x == y) -> String)(e)

The with notation can be used not only to specialize the type of a variable on the context, but it has the benefit of turning a program linear, since you replace two uses of a variable by only one.

You can also annotate the type of the variables moved with a with, allowing you to perform finer type adjustments. For example, in the program below:

foo(n: Nat, vec: Vector<Nat,Nat.succ(n)>, e: n == 5): String
  case vec {
    nil: ?a
    ext: ?b
  }!

We have e: n == 5 on both branches. But we also know that n is one less than the size of the vector. So we may write:

foo(n: Nat, vec: Vector<Nat, 1 + n>, e: n == 5): String
  case vec with e: (vec.size - 1) == 5 {
    nil: ?a
    ext: ?b
  }!

And we'll have e passed to both branches, replacing n by vec.size - 1 on both branches.

For more information on theorem proving, check the THEOREMS.md file on this repository.

Open

open value as v
body

The open syntax is a shortcut for pattern-matching a datatype with only one constructor. For example, if we have a datatype like:

type Vector3D {
  vector(x: Nat, y: Nat, z: Nat)
}

Then, the program below:

dot(a: Vector3D, b: Vector3D): Nat
  open a
  open b
  (a.x * b.x) + (a.y * b.y) + (a.z * b.z)

Is equivalent to:

dot(a: Vector3D, b: Vector3D): Nat
  case a {
    vector: case b {
      vector: (a.x * b.x) + (a.y * b.y) + (a.z * b.z)
    }
  }

The as name part is only necessary when the matched expression isn't a variable.

Switch

Allows you to shorten sequences of if-then-else based on a A -> Bool function:

switch String.eql(str) {
  "A": "a"
  "B": "b"
  "C": "c"
} default "?"

Is equivalent to:

if String.eql(str, "A") then
  "a"
else if String.eql(str, "B") then
  "b"
else if String.eql(str, "C") then
  "c"
else
  "?"

Annotation

x :: A

An inline type annotation. Has no effect, but can be useful to help the type-checker when it can't infer a type. For example:

let fn = ((x) x + x) :: Nat -> Nat
fn(4)

The code above uses an inline annotation to annotate the type of the (x) x + x function named fn.

Goal

?name

A goal can be written as ? followed by a name. For example, ?help is a goal named help. Goals are extremely useful when developing algorithms and proofs, as they allow you to keep a part of your program incomplete while you work on the rest. They also allow you to inspect the context and expected type on that part. For example, if you write:

add(a: Nat, b: Nat): Nat
  case a {
    zero: ?hole0
    succ: ?hole1
  }

Kind will display:

Goal ?hole0:
With type: Nat
With ctxt:
- a: Nat
- b: Nat

Goal ?hole1:
With type: Nat
With ctxt:
- a: Nat
- b: Nat
- a.pred: Nat

Notice how it shows the type it expects on each hole (Nat), as well as the context available there. Note also, in particular, how a.pred is available on the succ case: that's because pred is a field of Nat.succ.

Hole

_

A hole is written as a single underscore. It stands for "complete this for me". Holes are extremely useful to let Kind fill the "obvious" parts of your program for you. Without holes, Kind would be extremely more verbose. For example, the list of lists [[1,2],[3,4]], in its full form, would be:

List.cons<List(Nat)>(List.cons<Nat>(1, List.cons<Nat>(2, List.nil<Nat>)),
List.cons<List(Nat)>(List.cons<Nat>(3, List.cons<Nat>(4, List.nil<Nat>)),
List.nil<List(Nat)>))

With holes, you can write just:

List.cons<_>(List.cons<_>(1, List.cons<_>(2, List.nil<_>)),
List.cons<_>(List.cons<_>(3, List.cons<_>(4, List.nil<_>)),
List.nil<_>))

Moreover, single holes can be shortened as !. So it can also be written as:

List.cons!(List.cons!(1, List.cons!(2, List.nil!)),
List.cons!(List.cons!(3, List.cons!(4, List.nil!)),
List.nil!))

Of course, in this particular example, we can also use &, which stands for List.cons!, and [], which stands for List.nil!, and write:

(1 & 2 & []) & (3 & 4 & [])

And, obviously, we can just use the list notation directly:

[[1, 2], [3, 4]]

But all the list syntaxes, and many others, use holes under the hoods.

Kind's holes work by unifying immediate values only. That is, whenever you'd have an error such as:

Expected: Bool
Detected: _

Kind will replace _ by Bool and try again. That is all it does, which means it does no complex unification. Turns out this covers all cases required to keep Kind's syntax clean and free from bloated type annotations, even things like equality rewrites and vectors, while also keeping the type-checker fast. But if you want more advanced hole-filling features as seen in Agda or Idris, Kind won't do that and you need explicit types.

Logging

log("foo", "bar")
body

The syntax above expands to:

Debug.log<_>("foo" | "bar", () body)

Kind's log feature works like Haskell's Debug.trace. It allows you to print a string at runtime. It is very useful for debugging and inspecting the execution of an algorithm. Note that the order that Debug.logs happen can change depending on the evaluation strategy used by the target language, so it isn't deterministic.

Pair extractor

let {x,y} = pair
body

The syntax above can be used to extract two elements of a single-constructor type with two fields (like Pair). It desugars to:

pair<() _>((x,y) body)

If, then, else

if bool then t else f

The syntax above is equivalent to a ternary operator. It evaluates the bool x and returns t if it is true, f otherwise. It expands to:

bool<() _>(t, f)

Do notation

name {
  statements
}

Do blocks, or the do-notation, is extremely useful to "flatten" cascades of callbacks. In Kind, a do block requires the name of a monad and a series of statements. Inside it, you may use var x = monad to bind the result of a monadic computation to the name x. You may also write monad directly to execute a monadic computation and drop the result. You can also use local lets, as you'd expect. It will then be converted to a series of applications of Monad.bind and Monad.pure. For example,

ask_user_age: IO(Nat)
  IO {
    var name = IO.get_line("What is your name?")
    IO.print("Welcome, " | name)
    var year = IO.get_line("When you were born?")
    let age = 2020 - Nat.read(year)
    return Nat.read(age)
  }

Is converted to:

Monad.bind<_>(IO.monad)<_,_>(IO.get_line("What is your name?"), (name)
Monad.bind<_>(IO.monad)<_,_>(IO.print(String.concat("Hello, ", name), ()
Monad.bind<_>(IO.monad)<_,_>(IO.get_line("When you were born?"), (year)
let age = 2020 - Nat.read(year)
Monad.pure<_>(IO.monad)<_>(Nat.read(year))))))

Numeric literals

type	full syntax
Nat	42
Int	+42 or -42
U8	42#8
U16	42#16
U32	42#32
U64	42#64
U128	42#128
U256	42#256
I8	+42#8 or -42#256
I16	+42#16 or -42#16
I32	+42#32 or -42#32
I64	+42#64 or -42#64
I128	+42#128 or -42#128
I256	+42#256 or -42#256
F64	42.0 or +42.0 or -42.0

• Numbers literals allow you to create different types of numbers tersely.

• Bit-widths, signs and decimals may be omitted if sufficient type information is present.

• Parenthesis may be needed in certain locations (ex: (+42) instead of +42).

• You can also use a hexadecimal (0x123...) wherever a decimal is expected.

Char literal

'a'

A character literal is written with '. Characters aren't primitive in Kind. Instead, they're represented as 16-bit words, using the Word(16) type. As such, the character literal expands to:

Word.from_bits<16>(Bits.o(Bits.i(Bits.o(...Bits.e))))

For efficiency reasons, Kind's type-checker keeps characters represented as ints in memory and only unrolls if necessary. Moreover, all characters are compiled to Uint16 or equivalent when available in the target language.

String literal

"Hello"

A string literal is written with ". Strings aren't primitives in Kind either. Instead, they are represented as:

type String {
  nil,
  cons(head: Char, tail: String),
}

Note that Strings aren't the same as List(Char). They're a new datatype in order to make efficient compilation simpler. Kind's type-checker expands string literals to strings when needed. For example, "Hello" is expanded to:

String.cons('h', "ello")

If the first character is required for type-checking purposes (such as when doing dependent macros, or implementing printf()). Strings are compiled to native strings when available.

String concatenation

xs | ys

The code above expands to:

String.concat(xs, ys)

It concatenates two strings as one.

New pair

{1, "foo"}

Pair literals can be used as a shortcut to write pairs. They are expanded to:

Pair.new<_,_>(1, "foo")

New sigma

1 ~ refl

Sigma.new literals can be used to write sigmas, or dependent pairs. They are expanded to:

Sigma.new<_,_>(1, refl)

With Sigma.new as defined on the base library.

Sigma type

[x: A] B(x)

Sigma literals can be used to write sigma types or dependent pairs. They are expanded to:

Sigma(A, (x) B(x))

With Sigma as defined in the base library. In the same way that forall (aka Pi, aka the dependent function type) can be read as "forall", Sigmas can be read as "there exists". So, for example, the program below:

there_is_an_even_nat: [x: Nat] (x % 2) == 0
  0 ~ refl

Can be read as there exists a x:Nat such that x mod 2 is equal to zero. Sigmas can also be used to create subset types:

EvenNat: Type
  [x: Nat] (x % 2) == 0

Equal type

a == b

The syntax above expands to:

Equal(_, a, b)

It is the type of propositional equality proofs. It is not a boolean equality operator.

refl is the constructor of Equal and provides an evidence of syntactically equal expressions.

Not equal type

a != b

The syntax above expands to:

Not(Equal(_, a, b))

It is the type of propositional inequality proofs. It is not a boolean inequality operator.

Maybe.some

some(42)

The syntax above expands to:

Maybe.some<_>(42)

Maybe.none

none

The syntax above expands to:

Maybe.none<_>

Maybe.default

maybe_value <> default_value

The syntax above expands to:

Maybe.default!(maybe, default_value)

It is useful to extract a value from a Maybe by providing a default. For example, some(7) <> 0 returns 7, and none <> 0 returns 0.

Without

without value: value
body

The without syntax allows us to extract the value of a Maybe, returning something in the case it is none. For example:

let list = [1, 2, 3, 4]
let head = List.head!(list)
without head: "List is empty."
"List has a head: " | Nat.show(head)

This snippet unwraps the value of head (a Maybe), allowing you to use it without manually extracting it with case. It is equivalent to:

let list = [1, 2, 3, 4]
let head = List.head!(list)
case head {
  none: "List is empty."
  some: "List has a head: " | Nat.show(head.value)
}

This is useful to flatten your code, reducing the required identation.

Record literal

{1, 2}

When a datatype has only one constructor, it can be seen as a record. The syntax above can be used to create an element of that type. It expands to:

Foo.ctor_name(1, 2)

Depending on where it is used, may require a type annotation: {1, 2} :: Foo.

Record getter

foo@x

The syntax above expands to:

case foo { new: foo.x }

It can be used to get a field of a single-constructor datatype.

Record setter

foo@x <- 100

The syntax above expands to:

case foo { new: Foo.new(100, foo.y) }

It can be used to set a field of a single-constructor datatype.

List literal

[1, 2, 3]

The syntax above expands to:

List.cons<_>(1, List.cons<_>(2, List.cons<_>(3, List.nil<_>)))

List consing

1 & list

The syntax above expands to:

List.cons<_>(1, list)

It adds an element to the beginning of a list.

List concatenation

xs ++ ys

The syntax above expands to:

List.concat<_>(xs, ys)

It concatenates two lists as one.

List getter

list[4]

The syntax above expands to:

List.get!(4, list)

This returns the element at index 4 as a Maybe.

List setter

list[4] <- 100

The syntax above expands to:

List.set!(4, 100, list)

This sets the element at index 4 to 100.

Map literal

{"foo": 1, "bar": 2, "tic": 3, "toc": 4}

The syntax above expands to:

Map.from_list!([
  {"foo", 1},
  {"bar", 2},
  {"tic", 3},
  {"toc", 4},
])

You can also replace string key by variables, for example:

let key = "foo"
let val = 1
let map = {key: val, "bar": 2}

This will create the {"foo": 1, "bar": 2} map.

Map getter

map{"foo"}

The syntax above expands to:

Map.get!("foo", map)

This returns the element at key "foo" as a Maybe.

Map setter

map{"foo"} <- 100

The syntax above expands to:

Map.set!("foo", 100, map)

This sets the element at key "foo" to 100.

Equal.apply

apply(f, e)

The syntax above expands to:

Equal.apply<_,_,_,f>(e)

Equal.rewrite

value :: rewrite x in type with e

The syntax above expands to:

Equal.rewrite<_,_,_, (x) type>(e, value)

Using Equal.rewrite as defined on Equal.fm. It allows rewritting the type of an expression based on an equality proof. For example, suppose you have the following values in your context:

eq: 10 == 5 + 5
xs: Vector(Nat, 10)

Then you can use rewrite to "cast" the type of xs:

let ys = xs :: rewrite x in Vector(Nat, x) with e

And then you'll have:

eq: 10 == 5 + 5
xs: Vector(Nat, 10)
ys: Vector(Nat, 5 + 5)

In your context. Notice that ys is just xs, except with the type changed to replace 10 by 5 + 5. You can always rewrite inside types if you have a proof that the substituted expressions are equal.

For loops with lists

for x in list with name:
  value
body

The for-in syntax can be used to update a state continuously, for each element of a list. Since Kind is a pure language, the result must be associated with a variable that serves as a target for the loop state. For example:

let sum = 0
for n in [1, 2, 3] with sum:
  sum + n
sum

The code above will add all the elements in the [1,2,3] list, resulting in 6.

Loops aren't primitives. The code above is expanded to:

let sum = 0
let sum = List.for(_, [1,2,3], _, 0, (n, sum) Nat.add(sum, n))
sum

It uses the function List.for from the base libraries.

For loops with ranges

for x from i0 to i1 with name:
  value
body

Like for-in, but operates on numeric ranges instead of lists. If unspecified, the index will be a Nat, but you can annotate it to have other types of indices:

for x : U32 from i0 to i1 with name:
  value
body

Ranged loops are expanded to use the Nat.for function.

While loops

While loops can be used to repeat an operation based on a condition:

let sum = 0
while sum <? 10 with sum:
  log("sum: " | Nat.show(sum))
  sum + 1
sum

You can also use get instead of let to store a pair on the state, which is useful to keep track of indices.

let idx = 0
let str = ""
while idx <? 10 with {idx, str}:
  log("idx=" | Nat.show(idx) | " str=" | str)
  {idx + 1, str | Nat.show(idx)}
str

While is expanded to use the Function.while function.

Binary Operators

syntax	desugar
2 + 3	Nat.add(2, 3)
2 - 3	Nat.sub(2, 3)
2 * 3	Nat.mul(2, 3)
2 / 3	Nat.div(2, 3)
2 <? 3	Nat.ltn(2, 3)
2 <=? 3	Nat.lte(2, 3)
2 =? 3	Nat.eql(2, 3)
2 >=? 3	Nat.gte(2, 3)
2 >? 3	Nat.gtn(2, 3)
(+2) + (-3)	Int.add((+2), (-3))
2#32 + 3	U32.add(2#32, 3#32)
2.0 + 3.0	F64.add(2.0, 3.0)
true && false	Bool.and(Bool.true, Bool.false)
true || false	Bool.or(Bool.true, Bool.false)

Note that operators in Kind have no precedence and are always right associative.
That means, for example, `a * b + c - d` is parsed as `(((a * b) + c) - d)`.