Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Lait

Lait is a simple programming language embedded in the Lean proof assistant, intended to be used for teaching programming languages courses. You can find the repository for Lait here. It has an ML-like syntax and type system; if you don’t know what that is, that’s OK; we will explain it as we go along.

Getting Started

To get started with Lait, ensure that you have Visual Studio Code installed with the Lean extension. You can also follow Lean’s own installation instructions here.

Once you have Lean installed, download the Lait starter repository, and open LaitStarter/Basic.lean. This will prompt VSCode to install the correct Lean version. To get Lait running for the first time, you then might need to do the following things:

  • Tell VSCode to “trust this folder”, if it is running in restricted mode.
  • Restart the Lean language server by clicking on the “∀” icon on the top right.
  • If the sidebar on the right (the Lean infoview) tells you to restart the file, click on the “∀” icon and select “Restart File”. This is the action you might do the most, so it is worth remembering the keyboard shortcut: Cmd+Shift+X or Ctrl+Shift+X on Mac and Windows, respectively.

To see if Lait is working correctly, replace the file’s contents with the following:

import Lait
#lait

#eval 2 + 24

Every Lait file must start with import Lait and #lait as the first two lines. After that, you can write Lait code. The #eval command should have a blue squiggle under it; highlighting it will show 4 as the result. In this book, the results of #eval will be shown indented underneath the command.

Updating Lait

Every once in a while, we will push an update to Lait. If this happens, you will need to update Lait as well. To do this, run lake update in the terminal in the same directory as your Lait project.

Overview of Lait

Lait, being a functional language similar to ML, has three kinds of syntax:

  • Commands, such as #eval and def, for creating top-level definitions and evaluating expressions;
  • Expressions, such as 2 + 2, which are computations to be evaluated; and
  • Values, such as 4, which are what expressions evaluate to. (Every value is also an expression.)

Additionally, every expression and value has a type. We will introduce Lait through bite-sized lessons.

#eval, #check, Int, Comments, and Arithmetic Expressions

We begin by using Lait to evaluate and check calculator expressions. First, let’s see how to use #eval to evaluate an expression:

#eval 1 + 2 -- Evalutes to 33
#eval 1 * 2 -- Evaluates to 22
#eval 1 - 2 -- Evalautes to -1-1
#eval 1 - (2 - 2) -- Evalautes to 01

By hovering over the above expressions (e.g., 1 * 2), we can see that they all have type Int, which stands for integers. Values of type Int are given by numeric constants; i.e., 3, or -4. The name of every type in Lait begins with a capital letter.

Comments

Single-line comments in Lait, inherited from Lean, start with --. Multi-line comments begin with /- and end with -/.

Command: #check

We can also simply type check expressions without running them by using #check:

#check 2 + 3Int

Boolean Operators

The Bool type is defined by the values true and false.

Logical Operators

We use the infix operators &&, ||, and the prefix operator ! (not) to build expressions of type Bool:

#eval true || falsetrue
#eval false && truefalse
#eval not falsetrue
#eval not (true && not false)false

Comparison Operators

We can also create expressions of type Bool by using equality, ==:

#eval (1 == 2)false
#eval (false == false)true
#eval ("hello" == "hello")true

Given two expressions e1 and e2 of the same type, we can form e1 = e2, which has type Bool. (Note that equality doesn’t work for all types; e.g., function types, which we will see later.) We also have the shorthand e1 != e2 for not (e1 == e2):

#eval (1 != 2)true
#eval (false != false)false
#eval ("hello" != "hello")false

The ordinary comparison operators on Int are <, >, <=, and >=:

#eval (1 < 2)true
#eval (3 >= 3)true
#eval (4 <= 2)false
#eval (7 > (-2))true

If/then/else

To use a Bool, the primary way is to use it in an if/then/else expression:

#eval (if false then 1 else 2)2

Given a boolean expression e, and two other expressions e1/e2 of the same type T, if e then e1 else e2 has type T.

Strings

Values of type String are given using double quotes. Strings support one basic operation: concatenation, given by ++, which puts the two strings together.

#eval "hello" -- "hello""hello"
#eval "hello" ++ "world" -- "helloworld""helloworld"

We can convert an Int to a String using the toString function:

#eval toString 42 -- "42""42"

Product Types

We can put types together to form product types, with syntax S * T, where S and T are types. A value of type S * T is a pair of a value of type S and a value of type T.

We create values of product types using tuples:

#eval (3, "hello") -- (3, "hello")(3, "hello")

Given a product type, we can project out the first or second component as follows:

#eval fst (2, 3) -- 22
#eval snd (2, 3) -- 33

Creating Simple Definitions

Lait has two constructs to create definitions, depending on if you are at the top level writing a command, or inside an expression.

At the top level, we use def, which can be written with or without a type annotation after the name of the definition:

def foo = 32
def foo_plus_one : Int = foo + 1
#eval foo_plus_one - 132

Inside expressions, we use let .. = .. in .., which similarly can have optional type annotations.

#eval  let x : Int = 3 in  let y = x * 2 in y * 318
#eval let res = (let b : Bool = false in if b then 1 else 2) in res * 24

Functions

Being a functional language, Lait treats functions as ordinary data, just like the types Int or String. For any types S and T, the type of a function from S to T is written S -> T.

Anonymous Functions

To create a function in Lait, one way is to define an anonymous function using the syntax fun x => e. We can also write type annotations for the argument through the syntax fun (x : T) => e, where T is the type of the argument. We can call a function in Lait by putting the function and argument side by side.

#check fun x => x + 1 (Int -> Int)
#eval fun x => x + 1 <function>
#eval (fun x => x + 1) 4243

def myFunc : Int -> Int = fun x => x + 1

Named Functions

Another way to define functions in Lait is by using named functions, which we create by using def with arguments.

def myFunc' x = x + 1
def myFunc'' (x : Int) = x + 1

Multi-Argument Functions

In contrast to anonymous functions, named functions can take in multiple arguments.

def addThese (x : Int) y (z : Int) : Int = x + y + z

#check addThese(Int -> (Int -> (Int -> Int)))
#check addThese 1(Int -> (Int -> Int))
#check addThese 1 2(Int -> Int)
#check addThese 1 2 3Int

As seen above, multi-argument functions have a nested function type; for example, addThese will have type Int -> (Int -> (Int -> Int)). We can partially apply an argument to addThese to obtain a new function with one less argument.

Recursion

Functions with names can be used recursively:

def factorial (n : Int) : Int = 
  if n <= 0 then 1 else 
  n * factorial (n - 1)

#eval factorial 5120

Polymorphism

Often, we will be able to write a function that can apply to multiple types. For example, consider the identity function fun x => x: we can supply an Int to receive an Int, and similarly for a String. We can see this in action in Lait below:

def id x = x
#check id∀ a. (a -> a)

The “type” of id is ∀ a. a -> a, which means that we can supply a value of any type a, and receive a value of type a. (We write “type” in quotes because forall-types can only be associated to top-level definitions, and not arguments of functions.) Let’s see what happens when we supply various arguments to id:

#eval id 42 -- 4242
#eval id "hello" -- "hello""hello"

A more complicated example of polymorphism is given by a higher-order function that applies a given function twice:

def applyTwice f x = f (f x)
#check applyTwice∀ a. ((a -> a) -> (a -> a))

Polymorphism and Type Annotations

We can use type annotations with polymorphic functions. While all types in Lait begin with a capital letter, we have that type variables — that is, variables that represent types — begin with a lowercase letter.

def applyThrice (f : a -> a) (x : a) : a = f (f (f x))
#check applyThrice∀ a. ((a -> a) -> (a -> a))

Above, the variable a stands in for an arbitrary type. Note that while applyThrice has the type ∀ a. (a -> a) -> a -> a, we assign f the type a -> a in the arguments of applyThrice; the “forall” symbol ∀ cannot appear in type annotations.

Examples: Equality and toString

Two important polymorphic definitions in Lait are equality and toString, which we have already seen. Let’s now look at them more closely:

def eq x y = x == y
def tostr x = toString x
#check eq∀ a. (a -> (a -> Bool))
#check tostr∀ a. (a -> String)

As we see above, eq has type ∀ a. a -> a -> Bool, while tostr has type ∀ a. a -> String. While this usually works as expected, an important exception is what happens when a is a function type, such as Int -> Int:

#eval (fun (x : Int) => x) == (fun (y : Int) => y)
#eval toString (fun (x : Int) => x)"<function>"

Complex Data, Part I: Lists and Option

So far, we have only seen basic data types, such as Int and Bool, function types, and product types, such as Int * Int. We will now move on more complex data types.

Lists

For any type t, List<t> is the type of lists of values of type t.

Creating Lists

To create a list, we have the value Nil, which has type List<t> for any type t, and the function Cons, which has type ∀ a. (a -> (List<a> -> List<a>)); that is, it takes in a value of type a and a list of type List<a> and returns a list of type List<a>.

#eval Cons 1 (Cons 2 (Cons 3 Nil)) -- Cons(1, Cons(2, Cons(3, Nil()))) Cons(1, Cons(2, Cons(3, Nil())))

(Note above that the empty list, when evaluated, is written as Nil(), not Nil. This is because Nil is a constructor for a data type, which we will discuss in more detail later.)

Using Lists

To use a list, we pattern match on it.

def sumList (xs : List<Int>) : Int  = 
  match xs with
  | Nil => 0
  | Cons h t => h + sumList t
  end

#eval sumList [1, 2, 3] -- 66

Every patern match must begin with match e with, where e is an expression; and must end with end. For lists, pattern matching must analyze two cases: the Nil case, and the Cons case. If we forget one of the two cases, Lait will throw an error:

def badSumList (xs : List<Int>) : Int  = 
  match xs with
  | Cons h t => h + badSumList t
  end

Abbreviations for Lists

Since lists are so common, we also have abbreviations. First, Nil and Cons are synonymous with [] and ::. This can be used both for creating lists and pattern matching on lists.

#eval 1 :: 2 :: 3 :: [] -- Cons(1, Cons(2, Cons(3, Nil())))Cons(1, Cons(2, Cons(3, Nil())))

def sumList xs = 
  match xs with
  | [] => 0
  | h :: t => h + sumList t
  end

In addition, when making a particular list, we can use the syntax [e1, e2, ..., en], where e1, e2, …, en are expressions of type t:

#eval [1, 2, 3] -- Cons(1, Cons(2, Cons(3, Nil())))Cons(1, Cons(2, Cons(3, Nil())))

Here, [1, 2, 3] is exactly equivalent to 1 :: 2 :: 3 :: [], which is in turn exactly equivalent to Cons(1, Cons(2, Cons(3, Nil()))).

Common List Operations

Lait has a number of list operations built in to its standard library.

List.append : ∀ a. (List<a> -> List<a> -> List<a>) takes two lists and returns a new list that joins them together:

#eval List.append [1, 2, 3] [4, 5, 6] -- Cons(1, Cons(2, Cons(3, Cons(4, Cons(5, Cons(6, Nil()))))))Cons(1, Cons(2, Cons(3, Cons(4, Cons(5, Cons(6, Nil()))))))

Note that the name of the above function is List.append, including the .. Identifiers in Lait can include periods in the middle of them. We use this as a simple form of namespacing: instead of having append, length, and so on — which might apply to binary trees as well as lists — we write them as List.append, and List.length.

List.length : ∀ a. (List<a> -> Int) takes a list and returns its length:

#eval List.length [1, 2, 3] -- 33

List.member : ∀ a. (List<a> -> a -> Bool) takes a list and a value and returns true if the value is in the list, and false otherwise:

#eval List.member [1, 2, 3] 2 -- truetrue
#eval List.member [1, 2, 3] 4 -- falsefalse

Note that List.member only works for lists of types that can be compared for equality (e.g., Int), and will throw an error if the list contains functions.

List.filter : ∀ a. (List<a> -> (a -> Bool) -> List<a>) takes a list and a predicate and returns a new list that contains only the elements of the original list that satisfy the predicate:

#eval List.filter [1, 2, 3] (fun x => x >= 2) -- Cons(2, Cons(3, Nil()))Cons(2, Cons(3, Nil()))

List.find : ∀ a. (List<a> -> (a -> Bool) -> Option<a>) takes a list and a predicate and returns the first element of the list that satisfies the predicate, or None if no element satisfies the predicate:

#eval List.find [1, 2, 3] (fun x => x >= 2) -- Some(2)Some(2)
#eval List.find [1, 2, 3] (fun x => x > 3) -- NoneNone()

(Option types are discussed below.)

Options

Lists are one example of an algebraic data type, which is a data type that is built up using constructors (for lists, Nil and Cons), and examined using pattern matching. Another common one built in to Lait are option types. Given a type t, a value of type Option<t> is either None or Some(x), where x is a value of type t. Hence, an option type is used when a value may or may not be present.

#check None -- ∀ a. Option<a>∀ a. Option<a>
#check Some 1 -- Option<Int>Option<Int>

To use an option type, we pattern match on it, similar to lists. Below is a worked example:

def List.getFirst (xs : List<a>) : Option<a> =
  match xs with 
  | [] => None
  | x :: _ => Some x
  end

def List.isFirstPositive (xs : List<Int>) : Bool =
  match List.getFirst xs with 
  | None => false -- List is empty, so head is not positive
  | Some x => x > 0 -- Otherwise, return whether that first element is positive
  end

First, we create a function List.getFirst that gets the first element of a list, or None if the list is empty. Then, we create a function List.isFirstPositive that uses List.getFirst to get the first element if it exists; if it does, we return whether it is greater than zero.

Writing Unit Tests

Printing and the Unit type

Expressions in Lait can do more than compute values; they can also do things via side effectful operations, such as printing. To print things in Lait, we use the function print : String -> Unit. Here, Unit is a type in Lait that has exactly one value — written () — which is used to represent the absence of a particular return value. Let’s see it in action:

#eval print "hello"
"hello"

---

()

When we sequence computations together using let, the side effects happen in order:

#eval let _ = print "hello" in print "world"
"world"

---

"hello"

---

()

(We use underscores in let to indicate that we don’t care about the value of the expression, since we know it will return ().) (TODO: double check how the hover should appear.)

Note that defs that contain side effects (such as print) are evaluated as soon as they are defined:

def myPrint = print "hello"…

If we want to delay myPrint to only happen when we want it to, we want to make it a function. For this purpose, we can pass it a value of type Unit:

def myPrint' (u : Unit) = print "hello"
#eval myPrint' ()
"hello"

---

()

Since we never care about the value of u, we have special syntax for arguments of type Unit:

def myPrint'' () = print "hello"

#eval myPrint'' ()
"hello"

---

()

#eval myPrint'' ()
"hello"

---

()

Complex Data, Part II: User-Defined Types

Let’s now return to complex data types. Aside from List and Option, Lait also allows you to define your own. First, let’s consider a type for a binary tree of numbers:

type Tree = | Leaf (value : Int) | Node (left : Tree) (right : Tree)

def sum_tree (t : Tree) : Int =
  match t with
  | Leaf x => x
  | Node l r => sum_tree l + sum_tree r
  end

#eval sum_tree (Node (Leaf 10) (Node (Leaf 20) (Leaf 30)))60

Here, we are using the type keyword, which requires a number of constructors. Each constructor takes any number of arguments.

If we want to define a tree that can hold values of any type, we can do that by using a type parameter:

type ParamTree<a> = | PLeaf (value : a) | PNode (left : Tree a) (right : Tree a)

Constructor names in Lait must be unique; thus, we used the names PLeaf and PNode, since Leaf and Node were taken by Tree. Above, just like polymorphic functions, we use a type parameter a to indicate the type of the tree’s values.

Complex Data, Part III: Records

While one can use pairs to hold many values (e.g., by holding a value of type Int * (Int * Int) and so on), doing so is not very ergonomic. To handle this use case, Lait supports records, which are tuples of at least one element where each element is named.

type MyFiveInts = {
  x : Int,
  y : Int,
  z : Int,
  w : Int,
  a : Int
}

type MyFiveThings<a> = {
  x : a,
  y : a,
  z : a,
  w : a,
  a : a
}

Type Aliases

We can create type aliases with the following syntax:

type Foo = Int * Int

def getFirst (f : Foo) = fst f

Type aliases can be parameterized as well:

type Pair<a, b> = a * b
def Pair.fst (p : Pair<a, b>) : a = fst p

Mutable References

The final major feature of Lait is mutation, expressed similar to ref in OCaml, or a box in Racket. For any type T, Ref<T> is the type of a mutable reference to a T; that is, a “box” that holds a T, and can be updated. Let’s see a worked example below:


def mkBox () : Ref<Int> = alloc 0

def incr (x : Ref<Int>) : Unit = 
  let v = !x in 
  x := v + 1

def myInt = mkBox ()

#eval !myInt0
#eval incr myInt()
#eval incr myInt()
#eval !myInt2
#eval incr myInt()
#eval !myInt3

We now detail the language features related to mutation.

  • To create a reference, one uses the syntax alloc e. If e is a value of type T, then alloc e is a value of type Ref<T>.
  • To read the current value of a reference, one uses the syntax !x, where x is a Ref<T>. This returns a value of type T.
  • To update the value of a reference, one uses the syntax x := e, where x is a Ref<T> and e is a value of type T. This updates the reference to hold the new value, and returns () : Unit.
  • All commands in Lait are evaluated top to bottom. Hence, the first #eval returns 0, since we haven’t incremented the value yet.

As a more sophisticated example, let’s increment a list using mutation:

def List.iter (f : a -> Unit) (xs : List<a>) : Unit = 
  match xs with 
  | [] => ()
  | x :: xs' => let _ = f x in List.iter f xs'
  end

def List.sum (xs : List<Int>) : Int = 
  let sum = alloc 0 in
  let _ = List.iter (fun x => sum := !sum + x) xs in 
  !sum

#eval List.sum [1, 2, 3, 4, 5]15