Lait

Lait is a simple programming language embedded in the Lean proof assistant, intended to be used for teaching programming languages courses. To get started using Lait, see here. If you are interested in the implementation of Lait itself, see the repository.

The Lait tutorial is meant to be read in order, from beginning to end:

• Getting Started
• Arithmetic and Basic Commands
• Boolean Operators
• Strings
• Product Types
• Creating Simple Definitions: let and def
• Functions
• Polymorphism
• Complex Data, Part I: Lists and Option
• Complex Data, Part II: User-Defined Types
• Type Aliases
• Printing and the Unit type
• Mutable References
• Errors

Additional information about functions and datatypes built in with Lait are here.

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 + 2>> 4

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 with the syntax >> ....

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.

Arithmetic and Basic Commands: #eval/check/test

import Lait
#lait

Lait is a typed functional language similar to ML. Hence, if you have used Haskell, OCaml, SML, or Plait before, the concepts here should be familiar. We begin by using Lait to evaluate and check calculator expressions. First, let’s see how to use #eval to evaluate an expression:

-- Below are some arithmetic expressions.

/-
And here
is another comment.
-/

#eval 1 + 2 >> 3
#eval 1 * 2 >> 2
#eval 1 - 2 >> -1
#eval 1 - (2 - 2) >> 1

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 + 3>> Int

Command: #test

You can write unit tests in Lait as follows:

#test (1 + 2 * 3) === 7

The syntax is #test e1 === e2, where e1 and e2 are expressions. Note the use of three equals signs. If a test passes, nothing happens; however, if a test fails, we see an error message:

#test 1 * 2 === 3

In this book (as well as when using Lait), error messages show up as red squiggles.

Boolean Operators

import Lait
#lait

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 || false>> true
#eval false && true>> false
#eval not false>> true
#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

import Lait
#lait

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 values to a String using the toString function:

#eval toString 42>> "42"
#eval toString true>> "true"

Here, toString has a polymorphic type, which means it can accept arguments of multiple types; e.g., Int, or Bool as above. We will see more about polymorphism here.

Product Types

import Lait
#lait

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

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

#eval fst (2, 3)>> 2
#eval snd (2, 3) >> 3

Creating Simple Definitions

import Lait
#lait

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 - 1>> 32

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 * 3>> 18
#eval let res := (let b : Bool := false in if b then 1 else 2) in res * 2>> 4

Identifiers

Inherent in every language is what counts as a valid identifier; that is, what kinds of things can be defined by def or let. Identifiers in Lait are inherited from Lean. In Lait, every identifier:

• Must begin with a letter or an underscore;
• and can contain letters, numbers, or the symbols ., ?, ', and _ (among others).

Functions

import Lait
#lait

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.

-- Creating anonymous functions:
#check fun x => x + 1 >> Int -> Int
#eval fun x => x + 1 >> <function>
#check fun (x : Bool) => not x>> Bool -> Bool

-- Calling an anonymous function:
#eval (fun x => x + 1) 42>> 43

-- Assigning an anonymous function to a def:
def myFunc : Int -> Int := fun x => x + 1

-- Calling it:
#eval myFunc 20>> 21

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

#eval myFunc' 12>> 13
#eval myFunc'' 12>> 13

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

-- The function itself has a nested function type.
-- We can think of this as either a function of three arguments, 
-- or equivalently a function that returns a function, which itself
-- returns another function. 
#check addThese>> Int -> Int -> Int -> Int

-- We can partially apply functions of multiple arguments.
#check addThese 1>> Int -> Int -> Int
#check addThese 1 2>> Int -> Int
#eval addThese 1 2 3>> 6

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 5>> 120

Polymorphism

import Lait
#lait

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

The type of id is a -> a. Here, a is a type variable, which can be instantiated to any other type. While types in Lait must begin with a captial letter, type variables must begin with a lowercase one. Hence, we can think of id as having type Int -> Int, if we set a = Int, or String -> String, if a = String. Let’s see what happens when we supply various arguments to id:

#eval id 42 >> 42
#eval id "hello" >> "hello"

Some Examples

Let’s see a few more examples of polymorphism. First, let’s see this one:

def doSomeStuff f x := f x
#check doSomeStuff>> (a -> b) -> a -> b

Here, doSomeStuff has type (a -> b) -> a -> b. That is, we can call doSomeStuff on any values f and x, as long as f is a function and x’s type is the same as the input type to f.

If we didn’t call f on x then we would get a less constrained type:

def doOtherStuff f x := x
#check doOtherStuff>> a -> b -> b

Here, f has type a, while x has type b. Thus f and x can be anything, and they don’t have to have types that are related to each other.

Let’s look at one final example:

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

Here we see that the type of applyTwice is (a -> a) -> a -> a. This type is even more specialized than doSomeStuff: not only does x need to be the input to f, but the output of f must also be a valid input to f (since we call f on f x).

Polymorphism and Type Annotations

We can use type annotations with polymorphic functions.

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

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
#check eq>> a -> a -> Bool
#check toString>> a -> String

As we see above, eq has type a -> a -> Bool, while toString has type a -> String.

An important quirk of equality is that, while Lait allows us to compare any type for equality, some types (most importantly function types) do not work:

-- This throws an error, because are comparing functions for equality.
#eval (fun (x : Int) => x) == (fun (y : Int) => y)

Complex Data, Part I: Lists and Option

import Lait
#lait

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

#check Nil>> List<a>
#check Cons>> a -> List<a> -> List<a>
#eval Cons 1 (Cons 2 (Cons 3 Nil)) >> Cons 1 (Cons 2 (Cons 3 Nil))

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]>> 6

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

def sumList2 xs := 
  match xs with
  | [] => 0
  | h :: t => h + sumList2 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))

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. We give a few examples here; more can be seen in the standard library reference.

List.append : 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)))))

Identifiers in Lait can have periods in the middle of them. We use this as a simple form of namespacing: List.append is the name we give to an operation on lists (as opposed to an append operation on, say, strings).

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

#eval List.length [1, 2, 3]>> 3

List.member : 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>> true
#eval List.member [1, 2, 3] 4 >> false

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

List.find : 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
#eval List.find [1, 2, 3] (fun x => x > 3)>> None

(Option types are discussed below.)

Options

Lists are one example of user-defined data type, which is built up out of constructors (e.g., Nil and Cons for lists). Another common example built into 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  >> Option<a>
#check Some 1>> 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.

Pattern Matching: No Nesting

Lait does not support nested pattern matching, where we match on multiple constructors at once. Thus, the following does not work:

def getSecondOrZero (xs : List<Int>) : Int :=
match xs with
 | Cons x (Cons y ys) => y
 | Cons x Nil => 0
 | Nil => 0
end

When we pattern match on a constructor (be it Cons or a user-defined one), we can only pattern match “one layer deep”. Hence, the two arguments to Cons in a pattern match must both be variables; not constructors themselves (such as Cons or Nil). So the above needs to instead be written:

def getSecondOrZero (xs : List<Int>) : Int :=
  match xs with
  | Cons x xs' => 
    match xs' with
    | Cons y zs => y
    | Nil => 0
    end
  | Nil => 0
  end

Complex Data, Part II: User-Defined Types

import Lait
#lait

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

-- Constructors are functions from their arguments to the type.
#check Leaf>> Int -> Tree
#check Node>> Tree -> Tree -> Tree

Here, we are using the type keyword, which requires a number of constructors. Each constructor takes any number of arguments. Each constructor can be seen as a function from its fields to the data type.

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 : ParamTree<a>) (right : ParamTree<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.

Records

Often, one wants to hold a collection of a bunch of values at once. While one could do this with a nested pair:

type FiveInts := Int * Int * Int * Int * Int

def getFourth (v : FiveInts) := fst (snd (snd (snd v)))

this is far from ideal. To handle this in Lait, we use a record. A record is simply a datatype with exactly one case:

type MyRecord := | MkMyRecord (x : Int) 
                              (y : Int) 
                              (z : Int) 
                              (w : Int) 
                              (a : Int)

As before, this defines a function MkMyRecord : Int -> Int -> Int -> Int -> MyRecord. To get out the fourth element, we can then pattern match:

def getW (m : MyRecord) :=
  match m with
  | MkMyRecord _ _ _ w _ => w
  end

However, there is an easier way. When we have a record, Lait automatically generates the appropriate getters, which behave similarly to the above pattern match:

#check MyRecord.x>> MyRecord -> Int
#check MyRecord.y>> MyRecord -> Int
#check MyRecord.z>> MyRecord -> Int
#check MyRecord.w>> MyRecord -> Int
#check MyRecord.a>> MyRecord -> Int

Getters are only defined for data types that have one constructor.

Type Aliases

import Lait
#lait

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

Printing and the Unit type

import Lait
#lait

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"
>> hello


>> ---

>> world

>> ---

>> ()

If you click on “hello” in the above code snippet, you can see the rest of what is printed out. (We use underscores in let to indicate that we don’t care about the value of the expression, since we know it will return ().)

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

def myPrint := print "hello"…

(In the textbook, you can see the print effects by hovering over the ... to the right of the definition.)

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


>> ---

>> ()

Mutable References

import Lait
#lait

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 := get x in 
  set x (v + 1)

def myInt := mkBox ()

#eval get myInt>> 0
#eval incr myInt>> ()
#eval incr myInt>> ()
#eval get myInt>> 2
#eval incr myInt>> ()
#eval get myInt>> 3

We now detail the language features related to mutation.

• To create a reference, one uses the function alloc : a -> Ref<a>.
• To read the current value of a reference, one uses the function get : Ref<a> -> a.
• To update the value of a reference, one uses the function set : a -> Ref<a> -> 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:

-- `List.iter f xs` runs `f` on each element of `xs` in order.
def List.iter (f : a -> Unit) (xs : List<a>) : Unit := 
  match xs with 
  | [] => ()
  | x :: xs' => let _ := f x in List.iter f xs'
  end

-- Imperative sum over a list.
def List.sum (xs : List<Int>) : Int := 
  -- First, allocate a reference holding 0.
  let sum : Ref<Int> := alloc 0 in
  -- Iterate over the list: when we see an element `x`, 
  -- set `sum` to be the `x` plus the current value of `sum`.
  let _ := List.iter (fun x => set sum (get sum + x)) xs in 
  -- Return the value of `sum` after the iteration.
  get sum

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

Mutually Recursive Functions

import Lait
#lait

Normally, a definition in Lait can only refer to itself and to definitions that come before it. Sometimes, though, two (or more) functions need to call each other. To do this, we link the definitions together with the and keyword:

def isEven (n : Int) : Bool :=
  if n == 0 then true else isOdd (n - 1)
and isOdd (n : Int) : Bool :=
  if n == 0 then false else isEven (n - 1)

#eval isEven 10>> true
#eval isOdd 7>> true

Each clause after the first begins with and instead of def, and otherwise looks just like a named function. Every function in the group can call every other function in the group. Each function in a mutually recursive group must take at least one argument.

Mutually Recursive Types

Types can be mutually recursive too, using the same and syntax. Below, a Tree holds either a single value or a Forest of subtrees, and a Forest is a list of Trees:

type Tree<a> := | Leaf (v : a) | Node (c : Forest<a>)
and Forest<a> := | FNil | FCons (t : Tree<a>) (f : Forest<a>)

def treeSize (t : Tree<a>) : Int :=
  match t with
  | Leaf v => 1
  | Node c => forestSize c
  end
and forestSize (f : Forest<a>) : Int :=
  match f with
  | FNil => 0
  | FCons t f' => treeSize t + forestSize f'
  end

#eval treeSize (Node (FCons (Leaf 1) (FCons (Leaf 2) FNil)))>> 2

Errors

import Lait
-- This command below is just used to fix some printing of errors. 
-- You don't need to use this in your own code. 
#no_file 
#lait

In Lait, you can raise an error at runtime as follows:

def throw () := error "Hello"

#eval throw ()

You can use this to create algorithms which are partial. For example:

def List.unsafe_head (xs : List<a>) : a :=
 match xs with 
 | Nil => error "List is empty"
 | Cons x _ => x
 end

#eval List.unsafe_head [1, 2, 3]>> 1

#eval List.unsafe_head []

Special syntax: ...

In Lait, ... (three dots in a row) is synonymous with error "unimplemented":

def fill_this_in () : Int := ...

#eval fill_this_in ()

Testing for errors

In Lait, you can write tests for the presence of an error. If you have an expression e that should error, you can write #test_error e ensure that e will error.

def only_return_nonneg (i : Int) : Int :=
  if i < 0 then error "Bad input!" else i

#test only_return_nonneg 32 === 32
#test_error only_return_nonneg (- 5)
#test_error only_return_nonneg 32

Additionally, #test_error has a form where you can also assert the exact error you expect:

#test_error only_return_nonneg (-5) ~ "Bad input!"
#test_error only_return_nonneg (-5) ~ "some other error"

Lait Standard Library

import Lait
#lait

This file documents the functions and types that are included with Lait. See the tutorial for documentation about the basic types of Lait, including Int, Bool, String, function types, Unit, and product types.

Lists

Lists are defined as the following data type:

type List<a> := | Nil | Cons (h : a) (t : List<a>)

The following functions are already included with Lait:

• List.append : List<a> -> List<a> -> List<a>. Append the two lists.
• List.length : List<a> -> Int.
• List.member : List<a> -> a -> Bool. Return true only if the second argument is in the list. Calls equality, so will fail if the list is holding functions.
• List.filter : List<a> -> (a -> Bool) -> List<a>. Filter out members of the list for which the predicate does not hold. The predicate is ran in order on all elements of the list.
• List.find : List<a> -> (a -> Bool) -> Option<a>. Find the first element of the list for which the predicate holds.
• List.map : List<a> -> (a -> b) -> List<b>. Run the function in order on all elements in the list, and return the new list.

Option

The Option type is defined as follows:

type Option<a> := | None | Some (x : a)

It has the following functions included:

• Option.andThen : Option<a> -> (a -> Option<b>) -> Option<b>. If the first argument is None, do nothing; otherwise, the argument is Some x; run the function on x and return the result.

Maps

If you want to use a key-value map, use the following datatype:

type Map<k,v> := ...

(We elide the internal details of Map here, since you should just use it via its functions below.) Here, the first type parameter k is the type of keys, and the second parameter v is the type of values. You can use the following operations on maps:

• Map.empty, which has type Map<k,v> for any k and v. This is the empty map.
• Map.delete : Map<k,v> -> k -> Map<k,v>. Delete the key from the map.
• Map.insert : Map<k,v> -> k -> v -> Map<k,v>. Add the given key-value pair to the map.
• Map.lookup : Map<k,v> -> k -> Option<v>.

Below are some examples:

def myTest : Option<Int> := 
  let m1 : Map<Int, Int> := Map.empty in 
  let m2 : Map<Int, Int> := Map.insert m1 1 42 in 
  let m3 : Map<Int, Int> := Map.insert m2 2 43 in 
  let m4 : Map<Int, Int> := Map.delete m3 1 in 
  let res : Option<Int> := Map.lookup m4 2 in 
  res

#test myTest === Some 43

Note

If the above code snippet isn’t working for you, you likely need to update lait. Old versions of Lait had a different type for Map.insert.

Mutable References

We have the following functions available for mutable references:

• alloc : a -> Ref<a>. Create a new memory cell and fill it with its contents.
• get : Ref<a> -> a. Read the memory cell.
• set : Ref<a> -> a -> Unit. Write to the memory cell.

Other functions

• toString : a -> String. Render the value as a string.
• print : String -> Unit. Print the string as output.