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 term, or to one of the functions available on the base library.

A Kind program consists of a collection of top-level function definitions, usually with a function called Main which acts as the entry point of the program. Here's an example of a program that reads a number n from user input and outputs the nth fibonacci number.

Main {
  do IO {
    ask inp = IO.prompt "Which fibonacci number to calculate? "
    let res = Parser.run Parser.u60_decimal inp
    match Either res {
      left  =>
        let n     = res.val
        let fib_n = Fib n
        IO.output ((U60.show fib_n) "")
      right =>
        IO.output "Input text is not a number"
    }
  }
}

Fib (n: U60) : U60 {
  Fib.go n 0 1
}

Fib.go (n: U60) (f1: U60) (f2: U60) : U60
Fib.go 0 f1 f2 = f1
Fib.go n f1 f2 = Fib.go (- n 1) f2 (+ f1 f2)

Not all programs are necessarily made to be run. Proofs for example may only exist to be type-checked, which already validates the thing they're proving.

For many more real code examples, check the Kindex repository.

Top-level definition

Name (arg0: Type0) (arg1: Type1) : ReturnType
Name (Type0.ctr subarg0 subarg1) arg1      = rule0_body
Name arg0                        Type1.ctr = rule1_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 ReturnType, followed by a sequence of rewrite rules. For example:

MyName: String
MyName = "Victor"

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

GetFirst (fst: String) (snd: String): String
GetFirst fst snd = fst

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

Every rule must pattern match on each argument and they may match on a specific type constructor or match everything on a variable. For example, given the type:

Bool : Type
Bool.true : Bool
Bool.false : Bool

We could write the following function:

Bool.and (a: Bool) (b: Bool) : Bool
Bool.and Bool.true Bool.true = Bool.true
Bool.and x         y         = Bool.false

This defines a top-level function Bool.and with arguments a and b, and two rules. The first rule is selected only when a is Bool.true and b is Bool.true, and returns Bool.true. All other cases match with the second rule, where the variable x is bound to the value of the first argument and the variable y is bound to the value of the second argument. Both variables are unused and the second rule always return Bool.false.

A function with no rules behaves like a type constructor and is considered to be always correct by the type checker. In the example above, we defined one way to create a value of type Type called Bool and two ways of creating values of type Bool called Bool.false and Bool.true.

The name of the top-level definition also specifies the file where the definition is. For example Physics.Verlet.step must be either in Physics/Verlet/step.kind2 or Physics/Verlet/step/_.kind2. All top-level definitions must start with a capital letter, while all variables must start with a lowercase letter.

An argument may be defined to be erased, meaning it will be removed on runtime, being used only for type checking, by adding a - in front of the argument. For example:

MyFun -(a: Type) (b: a) : ReturnType

This defines a function with an argument a that gets erased during runtime, and an argument b of type a. All arguments of type Type should be erased. Also, because Kind has dependent types, we can write an argument that depends on the value of another, like is the case with b in the example above.

An argument may also be defined to be implicit, meaning it's value will be inferred and we don't need to pass it explicitly when calling a function. An argument that is both erased and implicit is defined by writing it between <>. For example:

List.tail <a: Type> (xs: List a) : List a

Here a is an implicit and erased argument. When calling a function with an implicit argument, we can pass it explicitly like List.tail Bool bool_list or we can ommit it and let its value be implied from the context like List.tail bool_list.

We can write an argument that is implicit but not erased with +<arg: ArgType>, but the use cases for this construction are very uncommon.

When writing the patterns of a function's rule, we can ommit arguments that are erased. For example, we can define a rule for the List.tail function above in two equivalent ways:

List.tail <a: Type> (xs: List a) : List a
List.tail a (List.nil  t)      = List.nil
List.tail a (List.cons t x xs) = xs

or

List.tail <a: Type> (xs: List a) : List a
List.tail  List.nil        = List.nil
List.tail (List.cons x xs) = xs

When type-checking, the ommited variables will be filled with an actual variable, but it won't be available for use inside the rule's body. Also, as the example above shows, we can ommit erased variables both in a root position of the pattern as well as inside of a constructor.

When pattern matching in a rule, if we don't use one of the bound variables, we can write it simply as _ and avoid having to give it a name. Internally, this variable is given a name that is not accessible inside of the rule body. In the List.tail example, the x variable is not used in the second rule, so we could write it as List.tail (List.cons _ xs) = xs to make explicit that we don't care about this value.

It is also possible to ommit any of the type annotations in a function definition. Any variables that don't have a explicit type have their types infered during type checking. Combining everything together, we could write the List.tail example as:

List.tail <a> (xs: List a) : List a
List.tail List.nil = List.nil
List.tail (List.cons _ xs) = xs

This is how this function is defined in the Kindex repository, which contains a wide collection of Kind definitions.

For functions that have only one rule that doesn't do any pattern matching at all on the arguments, there is a concise syntax to define them:

Hello (name: String) : IO U60 {
  IO.output (String.concat "Hello, " name)
}

This is equivalent to the following:

Hello (name: String) : IO U60
Hello name = IO.output (String.concat "Hello, " name)

Top-level function definition is the only syntax that isn't an expression, which means 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 as a variable name, followed by =>, followed by a term. Currently, there are no multi-argument lambdas in Kind, they must be written like a => b => c => body.

Usually, the type of a lambda argument is infered, but we may optionally anotate its type to help the type-checker. For example:

The type inference of the lambda x => x will likely fail since there isn't enough information here to know what exactly x is. We can write this expression as (x: SomeType) => x to avoid needing to infer this type.

Application

(func argm)

A function application is written in lisp style, (f x). 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.

In Kind2, lambdas are essentially different to functions, for some important optimizations reasons. There is no automatic currying of functions and we must always call a function with either all its explicit arguments or with all explicit and all implicit arguments. A 3-argument function f3, for example, is called with (f3 a0 a1 a2). If we want to curry the last argument of this function, it must be done explicitly with (a2 => (f3 a0 a1 a2)).

For lambdas, although they are not multi-argument, we can call multiple lambdas in a row like we would a multi argument function. For example:

Consider a variable holding a lambda let lmb = a0 => a1 => a2 => a3 => (f4 a0 a1 a2 a3). We could call it with (((lmb x) y) z), but for conciseness, we can ommit the parens and call it simply with (lmb x y z). Note that, unlike was the case for functions, we don't need to resolve every single lambda at once.

When writing a sequence of nested function applications, the first layer of parenthesis can be ommited (except for binary operators on native numbers). For example, the following function definitions are equivalent:

List.flatten <a> (xs: (List (List a))) : (List a)
List.flatten (List.nil)              = (List.nil)
List.flatten (List.cons head tail)   = (List.concat head (List.flatten tail))

List.flatten <a> (xs: List (List a)) : List a
List.flatten List.nil              = List.nil
List.flatten (List.cons head tail) = List.concat head (List.flatten tail)

One thing to be careful of, is with function types. List a -> List a is interpreted as (List (a -> (List a))) which may cause errors when not being careful, so it's best to use parenthesis in this case, like so (List a) -> (List a).

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).

Since a let is a normal expression like all others, it may be used anywhere an expression is expected. This can be useful for example, for defining very complex return types for proofs. For example, the following type can be made more readable by adding some let expressions:

TODO: Find an example. I know we have one somewhere either on Kindex or on Kind1's base.

TODO: Write a warning about dups

Forall (dependent function type)

(name: type) -> body

Forall, or Pi, or dependent function type, 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. It has type (n: Nat) -> (m: Nat) -> Nat.

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. It has type (b: Bool) -> (Equal Bool (Bool.not (Bool.not b)) b).

Since Kind functions are dependently typed, you can give a name to the input variable, and use it in the body of the dependent type. 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 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. This is converted into (_: Nat) -> Nat, which is a way of not giving a name to a variable.

While the arrow -> is actually optional when defining a named forall (ie: (x: a) -> (f x) is equivalent to (x: a) (f x)), it is usually recommended for clarity.

Annotation

x :: A

An inline type annotation. Has no runtime 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.

If, then, else

if b { t } else { f }

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

Type Derivation

TODO: Explain the syntax for the kind2 derive command

Match (pattern matching)

match ExprType name = expression {
  ctr0 => body0
  ctr1 => body1
  ...
  ctrN => bodyN
}: motive

The match syntax is a convenient way of branching on each constructor of a type, and accessing their inner values without having to write an auxiliary function. By using the motive, it can also be very helpful with proving theorems. A simple example is:

let x = Bool.true
match Bool 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:

List.sum (list: List Nat) : Nat {
  match List list {
    nil  => Nat.zero
    cons => Nat.add list.head (List.sum list.tail)
  }
}

This syntax can be useful in many cases, but here this function would be better expressed as:

List.sum (list: List Nat) : Nat
List.sum  List.nil             = Nat.zero
List.sum (List.cons head tail) = Nat.add head (List.sum tail)

Instead of using a let expression like in the Bool case above, we can give the matched expression a name inside the match expression itself:

match List xs = [1 2 3] {
  nil  => Nat.zero
  cons => xs.head
}

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:

match Bool x = Bool.true {
  true  => "i'm a string"
  false => 42
}: if x { String } else { U60 }

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:

DoubleNegation (b: Bool) : Equal Bool (Bool.not (Bool.not b)) b {
  match Bool 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:

DoubleNegation (b: Bool) : Equal Bool (Bool.not (Bool.not b)) b {
  match Bool b {
    true  => ?a
    false => ?b
  }: Equal Bool (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.

TODO: Write a document explaining theorem-proving concepts using Kind

Inspection

?name

We can ask the type-checker for what it infers that the type of an expression should be by using the inspection syntax, which is written as ? and optionally followed by a name to help you find it. 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
Add  Nat.zero         b = ?i0
Add (Nat.succ a.pred) b = ?i1

Kind will display:

Inspection.
- Goal: Nat
Context:
- b : Nat
On 'your_file.kind2':
  2 | Add  Nat.zero         b = ?i0

Inspection.
- Goal: Nat
Context:
- a.pred : Nat
- b      : Nat
On 'your_file.kind2':
  3 | Add (Nat.succ a.pred) b = ?i1

Notice how it shows the type it expects on each inspect (Nat), as well as the context available there. Note also, how the context in the Nat.succ case also has the variable a.pred, that was bound in the rule with the value from inside the Nat.succ constructor.

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 U60) (List.cons U60 1 (List.cons U60 2 (List.nil U60)))
(List.cons (List U60) (List.cons U60 3 (List.cons U60 4 (List.nil U60)))
(List.nil (List U60)))

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 _))

Of course, since these arguments that we filled with holes are all implicit, we could simply not write them, like in:

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

But underneath the hood, what an implicit argument actually does is automatically put holes in these places.

Of course, in this particular example, we can just use the list notation directly:

[[1 2] [3 4]]

But in this list syntax, as well as in many others, the holes would also be put there automatically.

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

(HVM.log logged result)

The logging feature of the runtime implementation is exposed as a Kind function. It allows you to print a string at runtime without using the IO type. It is very useful for debugging and inspecting the execution of an algorithm. However, because it causes a hidden side-effect, ignoring the type system, it should be used carefully and not be present on finished programs. Note that the printing happens when this function is reduced during runtime, which may not happen at the trivially expected time, may change if Kind is being run on multithreaded mode and may also happen when executing the type-checker since it's implemented as a special Kind program.

Do notation

do MonadicType {
  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 ask x = monad to bind the result of a monadic computation to the name x. You may also write ask 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 U60
  do IO {
    ask name = IO.prompt "What is your name?"
    ask IO.output (String.concat "Welcome, " name)
    ask year = IO.prompt "When you were born?"
    let age = 2020 - (Maybe.default (U60.read_decimal year) 0)
    return Maybe.default (U60.read_decimal age) 0
  }

Is converted to:

IO.bind ((IO.prompt "What is your name?") (name =>
IO.bind ((IO.output (String.concat "Welcome, " name)) (_ =>
IO.bind ((IO.prompt "When you were born?") (year =>
let age = 2020 - (Maybe.default (U60.read_decimal year) 0)
IO.pure (Maybe.default (U60.read_decimal age) 0)
))))))

To be able to use the do syntax with a type, it must implement a function called bind which does the monadic bind operation and a function called pure, which should simply return the value encapsulated by the monad. Note that this syntax doesn't actually require your operation to be a monad, but you should not implement these functions in case your operation is not monadic. In the future we may change this to actually require a proof of the monad properties.

Numbers and operators

Currently, Kind has one primitive number type, U60, the unsigned integers of length 60. When writing numbers in an expression like 583 and 34957, they are interpreted as U60. These numbers are compiled into very efficient machine code and should be used whenever you need performant number operations.

There are also some primitive number operators that work on U60s, that are used like any other function, except the () are always needed. They are:

Operation	Syntax
Addition	(+ a b)
Subtraction	(- a b)
Multiplication	(* a b)
Division	(/ a b)
Remainder	(% a b)
Shift left	(<< a b)
Shift right	(>> a b)
Bitwise and	(& a b)
Bitwise or	(
Bitwise xor	(^ a b)
Greater than	(> a b)
Greater equal	(>= a b)
Less than	(< a b)
Less equal	(<= a b)
Equal	(== a b)
Not equal	(!= a b)

Note that all of these are of type U60 -> U60 -> U60, that is, they all return a number. For example, (== 2 2) returns 1 and (<= 30 4) returns 0. If you need functions that return a boolean, check the Kindex repository for things like U60.equal (a: U60) (b: U60) : Bool.

TODO: Write about U120 compilation for kindelia

Char literal

'a'

A character literal is an ascii character surrounded with ''. Characters are currently implemented as U60 numbers, which makes them fast, but wastes a lot of space since only 8 bits are used at most.

String literal

"Hello"

A string literal is a sequence of ascii characters surrounded with "". Strings aren't primitives in Kind either. Instead, they are currently implemented as:

String : Type
String.nil : String
String.cons (head: Char) (tail: String) : String

String literals are expanded into a sequence of String.cons. For example, "Hello" is desugared to String.cons 'H' (String.cons 'e' (String.cons 'l' (String.cons 'l' (String.cons 'o' String.nil)))).

Sigma type

[name: type] -> body

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

Sigma type (name => body)

With Sigma in Kindex defined as Sigma (a: Type) (b: a -> Type) : Type . 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:

ThereIsEvenNat : [x: Nat] (Equal (Nat.mod x Nat.two) Nat.zero)
  $Nat.zero Equal.refl

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

EvenNat: Type
  [x: Nat] (Equal (Nat.mod x Nat.two) Nat.zero)

New sigma

$val_a val_b

Sigma.new literals can be used to create values for sigma types, or dependent pairs. They are expanded to:

(Sigma.new _ _ val_a val_b)

With Sigma.new defined as Sigma.new <a: Type> <b: a -> Type> (fst: a) (snd: b fst) : Sigma a b in Kindex.

List literal

[1, 2, 3]

The syntax above expands to:

(List.cons 1 (List.cons 2 (List.cons 3 List.nil)))

The , is optional.