# Value expression language¶

The *value expression language* is the part of the CSL language that lets us specify conditional expressions for event predicates and for defining values using the keyword `val`

.
It is also used by the reporting engine to define the values returned by reports.

Values may be defined at the top-most level, or as local values inside expressions with the let construct.
It takes the form `val p = e`

where `e`

is an expression and `p`

is a *pattern*.
For top-level values the pattern may be exactly one of `n`

or `n : T`

where `n`

is an identifier beginning with a lower-case letter and `T`

is a type.
Values declared inside a let construct may take one of these forms as well as the more complex patterns described in the sectino below.
Note that in both cases the type annotation `T`

must be *closed*, i.e., it cannot contain any type variables.

## Primitive values and value literals¶

The value expression language has the following built-in primitive types, all of which can be written with *literals*:

`Int`

, e.g.`0`

,`1`

,`123`

.`Float`

, e.g.`0.0`

,`1.23`

,`12.46`

,`1e6`

,`1E10`

,`1E-3`

,`1.234E3`

.`String`

, e.g.`""`

,`"abc"`

,`"\""`

.`DateTime`

, e.g.`#1969-07-20T20:18:04Z#`

,`#2018-02-02T11:06:08Z#`

.`Duration`

, e.g.`#P1DT2H3M4S#`

,`#-PT42.314S#`

.

The value expression language has support for tuples of at least 2 elements where each value in the tuple can be of a different type:

`Tuple`

, e.g.`(1, 2)`

,`("a", "b", 42)`

.

Furthermore, there is a type of *symbols* which are references to ledger entities.
The type of a symbol is one of the following *entity types*:

`Agent`

which represents agents that can send events. Agent symbols can be compared for equality, and they compare equal if they refer to the same agent.`Contract`

which represents an instantiated contract on the ledger. Contract symbols can be compared for equality similarly to agents.`PublicKey`

which represents a cryptographic public key used for asymmetric encryption. Public keys can be compared for equality and be used for checking signatures on signed data.`Signed`

which represents a value (whose serialized representation is) signed by some private key. Signed value symbols can be compared for equality, and their signatures can be checked respective to a public key.

### Number literals¶

Integer numbers (`Int`

) use signed Two’s complement 32-bit integers as their underlying implementation.
They are in the range from `-2147483648`

to `2147483647`

.
Calculations with integers wrap around at their bounds: in CSL `2000000000 + 2000000000 = -294967296`

is `True`

.

Floating-point numbers (`Float`

) use decimal128 as their underlying implementation.
This representation allows for exact financial calculations.
With decimal representation `0.1 + 0.2 = 0.3`

as you would expect, not `0.30000000000000004`

as one would see with binary64.
With decimal128 you get up to 34 digits of precision.
`1.0 / 3.0 = 0.3333333333333333333333333333333333`

.
Arithmetic operations on floating-point numbers round half to even also called Bankers rounding.
We have `1.0 + 2.5e-33 = 1.0 + 2e-33`

but because we round to the nearest even digit we also have `1.0 + 1.5e-33 = 1.0 + 2e-33`

.

`DateTime`

literals¶

`DateTime`

literals, however, deserve a bit of elaboration.
They are fenced by the `#`

symbol, and between these a subset of the ISO 8601 standard for date and time formatting is expected.
Specifically, a `DateTime`

in CSL takes one of the following forms from the ISO standard:

- A date and a time in UTC format:

```
// 28th of February 2018, at 13:37 o'clock UTC
val a = #2018-02-28T13:37:00Z#
// Christmas eve 2017, half past six in the evening UTC
val b = #2017-12-24T18:30:00Z#
// Christmas eve 2017, half past six in the evening UTC with high precision
val c = #2017-12-24T18:30:00.000Z# // Up to 3 decimals on the seconds.
```

- A date and time with an explicit time zone offset:

```
// 28th of February 2018, at 13:37 o'clock (in UTC+1)
val a = #2018-02-28T13:37:00+01:00#
// Christmas eve 2017, half past six in the evening (in timezone UTC-9)
val b = #2017-12-24T18:30:00-09:00#
// Same, with high precision
val c = #2017-12-24T18:30:00.000-09:00#
```

`DateTime`

s specified in different time zones can be compared:

```
// 13:37 in UTC+1 is 12:37 in UTC
val a = #2018-02-28T13:37:00+01:00# = #2018-02-28T12:37:00Z#
// = True
```

To allow for more readable contracts, CSL supports a shorthand syntax for writing `DateTime`

literals where parts may be omitted.
The omitted parts are treated as either `01`

for months and days or `00`

for hours, minutes, and seconds.
The time zone designator may be appended to any literal in one of the shorthand forms.
When it is not present, the time zone is UTC.
Therefore, the following `DateTime`

literals all denote the same point in time:

```
// We may forgo writing the time zone, in which case the time is in UTC.
val datetime0 = #2018#
val datetime1 = #2018Z#
val datetime2 = #2018+00:00#
val datetime3 = #2018+0000#
// The following could also be written with a UTC time zone designator.
val datetime4 = #2018-01#
val datetime5 = #2018-01-01#
val datetime6 = #2018-01-01T00#
val datetime7 = #2018-01-01T00:00#
val datetime8 = #2018-01-01T00:00:00#
// Between 0 and 3 decimals after the decimal point.
val datetime9 = #2018-01-01T00:00:00.#
val datetime10 = #2018-01-01T00:00:00.0# // Etc.
val datetime11 = #2018-01-01T00:00:00.000#
```

`Duration`

literals¶

Like `DateTime`

, the syntax for durations follows the ISO 8601 standard.
A Duration is written between two `#`

symbols and contains an optional sign, a `P`

, a date component and/or a time component.

The date component designates days and consists of a number with up to three fractional decimals followed by a

`D`

.The time component is prefixed with a

`T`

and is comprised of three sub-components. Each component is optional but the order must be adhered to and at least one must be present.- The hour component is a number with up to three fractional decimals followed by an
`H`

- The minute component is a number with up to three fractional decimals followed by an
`M`

- The seconds component is a number with up to three fractional decimals followed by an
`S`

- The hour component is a number with up to three fractional decimals followed by an

These are all valid duration literals:

```
val duration0 = #P1D# // 1 day
val duration1 = #PT1.2S# // 1.2 seconds
val duration2 = #P1DT2.5H3.001S# // 1 day, 2 hours, 30 minutes, and 3.001 seconds
val duration3 = #P1DT2.5H2M3.001S# // 1 day, 2 hours, 32 minutes, and 3.001 seconds
val duration4 = #-P1DT2.5H3.001S# // negative (1 day, 2 hours, 30 minutes, and 3.001 seconds)
val duration5 = #PT62M0S# // 62 minutes
```

Note that at least one component must be present, so `#P#`

is not a valid duration.
It’s easy to forget the prefixed `T`

of the time component, e.g. #P1S” is not valid
since the leading `T`

of the time component is missing. A trailing `T`

is also not
allowed as in `P1DT`

.

Note that durations are compared down to the millisecond and thus `#PT62M# = #PT1H2M#`

.

`Signed`

data¶

A `Signed a`

value refers to a message of type `a`

that was signed by some private key.
You can check if a `Signed a`

value was signed by a private key corresponding to a specific public key, and you can also extract the message from the `Signed a`

value.

```
type Answer : Event { answer: Signed String }
template WaitForAnswer(deepThought: PublicKey) =
<*> a:Answer where
Signed::checkSignature deepThought a.answer
&& Signed::message a.answer = "42"
```

## Operators¶

There are a number of arithmetic, comparison, and logical operators defined:

*Arithmetic operators*(`+`

,`-`

,`*`

, and`/`

):Work on

`Int`

and`Float`

. Note that we don’t have implicit conversion of numeric types. That means`2.0 * 4`

will be rejected by the type checker.*Equate*(`=`

):This operator compares values for equality. See the section below for a more detailed description

*Comparison operators*(`<`

,`>`

,`<=`

, and`>=`

):Works on

`Int`

,`Float`

, and`DateTime`

.*Logical operators*(“and”`&&`

and “or”`||`

):Combine

`Bool`

values.*Unary minus*(`-`

):Negates an

`Int`

or`Float`

value.

Note that the only valid operation on `Agent`

is equality.

The usual precedence rules between the operators are in effect.
Thus, for the arithmetic operators the multiplication/division operators have higher precedence than the addition/subtraction operators, and for the logical operators the “and” operator (`&&`

) binds tighter than the “or” (`||`

) operator.
We may use parentheses to enforce a different order of operators.

```
val a = (1 + 2) * 4 // = 12
val b = 1 + 2 * 4 // = 9
val c = 1.5 * 3.0 // = 4.5
// Wrong! Int and Float mixed up!
// val d = 1 - 1.0
val e = 4 <= 4 // True
val f = #1969-07-20T20:18:04Z# < #2018-02-02T11:06:08Z# // True
val g = 4 = 3 // = False
val h = "stringA" = "stringA" // = True
val i = #1969-07-20T20:18:04Z# = #2018-02-02T11:06:08Z# // False
val j = True && True // = True
val k = True && False // = False
val l = (True || False) && (False || False) // = False
val m = - 1 * 3 // = - 3
```

## Constructors and sum types¶

CSL lets you define *sum types*.
Values of sum types can be constructed in only those ways that are specified in the declaration of the sum type.
This is very handy when you have to model something that can only take values of certain forms.

We declare sum types with the `type`

keyword followed by the name of the new type and a list of *constructors*:

```
type YesOrNo
| Yes
| No
```

The sum type `YesOrNo`

has two constructors, `Yes`

and `No`

.
Both constructors take zero parameters, but in general constructors of sum types can take parameters.
For example, a type called `IntFloatOrNothing`

with three constructors that takes one `Int`

, one `Float`

, or nothing as its parameter, respectively, is declared as:

```
type IntFloatOrNothing
| AnInt Int
| AFloat Float
| NoneOfTheAbove
```

Values of our new type `IntFloatOrNothing`

can be constructed in three ways since there are three constructors:

```
val anInt = AnInt 43 // 'anInt' has the type IntFloatOrNothing
val aFloat = AFloat 42.4 // 'aFloat' has the type IntFloatOrNothing
val none = NoneOfTheAbove // 'none' has the type IntFloatOrNothing
```

Sum types can be declared with *type parameters* by writing them after the type name.
These act as placeholders for concrete types, and they can be used in the constructor declarations as types for their parameters.
The following type declares values that are either of one type, `a`

, or of some other type, `b`

:

```
type OneOrTheOther a b
| One a
| TheOther b
```

This type takes two type parameters `a`

and `b`

.
We can therefore make many different kinds of `OneOrTheOther`

s depending on how we instantiate the `a`

and `b`

:

```
val oneFortyTwo = One 42 // This is a 'OneOrTheOther Int b'
val y = TheOther "Hello" // This is a 'OneOrTheOther a String'
val z = One #2018-02-02T11:06:08Z# // This is a 'OneOrTheOther DateTime b'
val h = TheOther 42.42 // This is a 'OneOrTheOther a Float'
```

Notice that `x`

, `y`

, `z`

, and `h`

above do not have complete types yet: The constructors only restrict one of the two parameters to be `Int`

, `String`

, `DateTime`

, or `Float`

.
Because they do not place conflicting restrictions on the parameters, we may use both `x`

and `y`

anywhere that expects a `OneOrTheOther Int String`

.
Likewise we can use both `z`

and `h`

anywhere that expects a `OneOrTheOther DateTime Float`

, and we can use `x`

and `h`

anywhere we need a `OneOrTheOther Int Float`

and so on.

### Examples¶

`Bool`

is a sum type with two constructors that each take zero parameters.
The `Bool`

-type could be defined as follows:

```
type Bool
| True
| False
```

That is, `Bool`

has zero type parameters and two constructors called `True`

and `False`

, each taking zero parameters.
We can therefore construct an instance of a `Bool`

in two ways, just as one would expect from a boolean data type:

```
val trueValue = True
val falseValue = False
```

Similarly, the type of lists with elements of some type `a`

, `List a`

, can be defined as a sum type as follows:

```
type List a
| Nil
| Cons a (List a)
```

A list is either the empty list `Nil`

or the list `Cons x l`

with one element `x`

followed by the the list `l`

.
The actual type of elements in the list is not important to the list structure itself, as long as all elements in the list are of the same type.
This is enforced by the `Cons`

constructor: To make a `Cons`

value one must provide a value of type `a`

as the first parameter and a value of type `List a`

as the second.
For example, creating a list with numbers or strings is done by writing:

```
val oneTwoThree = Cons 1 (Cons 2 (Cons 3 Nil))
val strings = Cons "First string" (Cons "Second string" Nil)
```

Note that CSL also supports a special shorthand syntax for lists that allows us to write lists in a more readable way than the above.

Neither of the `Bool`

and `List a`

types are defined in the standard library.
Both types are builtin types in the expression language.

A number of functions that work with lists are defined in the standard library.

The standard library defines a type `Maybe a`

that represents values that can be undefined:

```
type Maybe a
| None
| Some a
```

We may construct a `Maybe a`

in one of two ways: By using the constructor `None`

with zero arguments, or by using the constructor `Some x`

where `x`

is an object of type `a`

.
This is useful when a value is only present in some cases.

## List shorthand¶

Although the `List`

type is an ordinary sum type with two constructors, it is useful to have a more concise notation than writing the constructor names `Cons`

and `Nil`

explicitly.
Therefore we may write `[]`

for the empty list, `[1]`

for the singleton list with one integer element, `["a", "b", "c"]`

for a list with three strings etc., as exemplified by the following table:

Shorthand | Equivalent expression |
---|---|

`[]` |
`Nil` |

`[[]]` |
`Cons Nil Nil` |

`[1]` |
`Cons 1 Nil` |

`[1.0, 2.0]` |
`Cons 1.0 (Cons 2.0 Nil)` |

`[[1], [2,3]]` |
`Cons (Cons 1 Nil) (Cons (Cons 2 (Cons 3 Nil)) Nil)` |

Using the shorthand syntax makes for more readable contract specification and is therefore encouraged. Because there is no difference between writing a list in the short or long form, the type of a list is not affected by the choice of notation. In particular, the following all specify the same list:

```
val a = Cons 1 (Cons 2 (Cons 3 Nil))
val b = Cons 1 (Cons 2 [3])
val c = Cons 1 [2, 3]
val d = [1, 2, 3]
```

Pattern matching on lists can use this shorthand notation as well.

## Records¶

A *record* is a data type that contains named fields with possibly different types.
To instantiate a value of a record type one must assign a value to each field that is declared as part of the record.
Record types are declared with the `type`

keyword followed by the (upper-case) name and a list of (lower-case) field names with their associated types.

The following is a declaration of a record type with the name `AnIntAndAFloat`

.
It has two fields called `theInt`

and `theFloat`

with the types `Int`

and `Float`

, respectively:

```
type AnIntAndAFloat {
theInt : Int,
theFloat : Float
}
```

To make values of this type we must assign values to both fields:

```
val intAndFloat1 = AnIntAndAFloat { theInt = 42, theFloat = 42.42 }
val intAndFloat2 = AnIntAndAFloat { theInt = 1, theFloat = 0.0 }
// Wrong: we forgot to specify 'theFloat'!
// val intAndFloat3 = AnIntAndAFloat { theInt = 0 }
```

Individual fields in a value of a record type can be accessed with the `.`

projection syntax:

```
val theInt = intAndFloat1.theInt // = 42
val theFloat = intAndFloat1.theFloat // = 42.42
```

A record can *inherit* fields from another record if it is declared as a *subtype*.
All records are implicitly subtypes of the built-in type `Record`

with zero fields.
To make a record a subtype of another record—the “parent record”—we annotate our record definition with `: ParentName`

after the name of the new type.
For example, if we wanted to make a new record type that not only contains an `Int`

and `Float`

, but also a `String`

, we could write the following:

```
type IntFloatAndString : AnIntAndAFloat {
theString : String
}
```

A value of type `IntFloatAndString`

is now *also* of the type `AnIntAndAFloat`

.
This means that to make a new value, we must fill out all the fields, including inherited ones:

```
val intFloatAndString = IntFloatAndString {
theString = "some string value",
theInt = 17, // These two fields are inherited and
theFloat = 117.4 // therefore a part of the new type.
}
```

Records can inherit from records that themselves inherit from other records.
The record type `IntFloatStringAndListOfInt`

below inherits from `IntFloatAndString`

, which itself inherits from `AnIntAndAFloat`

.
This means that an `IntFloatStringAndListOfInt`

record has all of the fields `theInt`

, `theFloat`

`theString`

, and `theList`

:

```
type IntFloatStringAndListOfInt : IntFloatAndString {
theList : List Int
}
val intFloatList = IntFloatStringAndListOfInt {
theList = [1, 2, 3],
theString = "I have four fields", // From IntFloatAndString
theInt = 42, // From AnIntAndAFloat
theFloat = 2.0 * 21.0 // From AnIntAndAFloat
}
```

Record types cannot be recursive, that is, we cannot have a field in a record of the record’s own type. Unlike sum types, they also cannot take type parameters.

### Record extension¶

When you want to create a new record that contains mostly the same fields as another you can use the *record extension* syntax.
Assuming a record expression `r`

of type `R`

is in scope, whenever you create a new record of type `R`

or a subtype thereof you can add `use r with`

in the beginning of list of field assigments.
This means that all fields of the record denoted by `r`

that are not explicitly set in the list of assignments are carried over unchanged:

```
type R { a : Int, b : Float }
type S : R { c : String }
val r = R { a = 1, b = 2.0 }
val r2 = R { use r with a = 3 }
// = R { a = 3, b = 2.0 }
val s = S { use r with c = "123" }
// = S { a = 1, b = 2.0, c = "123" }
// The record expression can be any expression that is of a supertype of S
val s2 = S { use S { use s with a = 15 } with b = 5.0 }
// = S { a = 15, b = 5.0, c = "123" }
```

### Examples¶

Even though a record type cannot contain fields of its own type, it can contain fields of other record types or sum types:

```
type Address {
streetName : String,
houseNumber : Int
}
type Person {
name : String,
idNumber : Int
}
type Direction
| Left
| Right
type DirectionsTo {
person : Person,
from : Address,
to : Address,
how : List Direction
}
```

We create instances of `DirectionsTo`

by nesting the record creation:

```
val dirs = DirectionsTo {
person = Person { name = "Bob", idNumber = 1 },
from = Address { streetName = "Main st.", houseNumber = 2 },
to = Address { streetName = "Side av.", houseNumber = 1334 },
how = [Left, Left, Right, Right]
}
// We can use the projection syntax '.' to access nested fields:
val fromStreet = dirs.from.streetName // "Main st."
val toStreet = dirs.to.streetName // "Side av."
```

Events in CSL contracts are records that inherit from the `Event`

record type of the standard library.
For instance, in a contract that uses delivery events encoded the type `DeliveryEvent`

we must define the record `DeliveryEvent`

as a subtype of `Event`

:

```
type DeliveryEvent : Event {
product : String
}
```

This means that `DeliveryEvent`

will have the fields `timestamp`

and `agent`

from `Event`

defined in addition to the field `product`

.

## Type aliases¶

It is possible to declare *type aliases* for types.
This can sometimes help in readability, as for example type parameters that are guaranteed to be of a certain type can be expressed using a type alias.
The general form of a type alias is `typealias <NAME> <type parameters> = <TYPE>`

where `<TYPE>`

may contain type parameters from the given list.
For instance, to construct a pair-like type where the first component may be missing we could write

```
typealias PartialPair a b = Tuple (Maybe a) b
```

This alias takes two type parameters, `a`

and `b`

.
Say we now have a use case for a `PartialPair`

but we know that the component that may be missing is always an integer.
This can be handled by refining the `PartialPair`

we just defined:

```
typealias IntPartialPair a = PartialPair Int a
```

Furthermore, if we at some other point know that both the first and second component of the tuple is an integer we can omit the type parameters entirely:

```
typealias T = IntPartialPair Int
```

## Functions¶

We can define *functions* in CSL by using *lambda notation*.
A function that takes an `Int`

and increments it is written:

```
val f = \x -> x + 1
```

The function `f`

takes an integer as argument, binds it to the parameter `x`

in the *function body* `x + 1`

, and returns the result of that computation.
We *apply* the function to an argument by writing the argument immediately after the function:

```
val two = f 1 // Apply 'f' to '1'
val three = (\x -> x + 1) 2 // Apply an anonymous/unnamed function to '2'
```

We have used the `val`

keyword because functions themselves are just values.
This means that we can pass them around just like we do with other values:

```
val addOne = \x -> x + 1
val callFuncWithValue = \func -> \x -> func x
val onePlusOne = callFuncWithValue addOne 1 // = 2
```

`addOne`

is the function that increments an integer and `callFuncWithValue`

is a function that takes first another function as argument, binds it to the name `f`

, and returns a new function.
This new function takes a single argument, calls it `x`

and invokes the function bound as `f`

with that argument.
It is instructive to see how we can derive that the `onePlusOne`

is `2`

:

```
val onePlusOneDerived = callFuncWithValue addOne 1
// = callFuncWithValue (\x -> x + 1) 1
// = (\f -> \x -> f x) (\x -> x + 1) 1
// = (\x -> (\x -> x + 1) x) 1
// = (\x -> x + 1) 1
// = 1 + 1
// = 2
```

Function application is *left associative*, meaning that the following values are all equivalent:

```
// 'f', 'g', and 'h' are functions
val x = f g h 0
val y = (f g) h 0
val z = ((f g) h) 0
```

### Reports¶

Functions are called *reports* when they are intended to be called from the outside, for example by using the interfaces generated by sic.
Such functions must be marked with the `report`

keyword, which ensures:

- that they are
monomorphic, that is, their argument and result types do not contain any type variables, and- neither their argument nor result types contain any occurrence of a function type, e.g.
`Int -> Int`

.

This ensures that the function can be called via the external API – it also serves a bit like the `public`

of Java.

```
val report f = \(agent : Agent) -> addUpTotalsFor agent
```

As with entry points, reports may only occur as top-level definitions; local `let`

-bound values cannot be reports

### Multi-case functions and patterns¶

Functions can consist of several function bodies, each associated with a *pattern*.
The particular function that is used for a certain input is chosen as the first one with a *matching* pattern.
The general form of a function is:

```
\ pattern0 -> body0
| pattern1 -> body1
| ...
| patternN -> bodyN
```

Patterns are used to inspect the arguments to functions and assign names to them. A pattern is a restriction of the “shape” that the argument value has to be in for the associated function branch to be taken.

The least restrictive pattern for input arguments is the one that does not restrict at all – the *wildcard*.
A wildcard pattern is written with an underscore, and it matches anything:

```
val fortyTwo = \_ -> 42
```

The above is this a function that will return `42`

no matter the input.
If the value of a matched wildcard is needed in a function, we may give it a name:

```
val addThree = \x -> x + 3
```

Here, `x`

is a wildcard pattern that matches anything and binds it to the name `x`

in the function body.

Writing patterns that restrict the allowed arguments is done by specifying how the value would have had to be constructed for it to be accepted for that particular branch. For sum types, this usually means that there is a pattern for each constructor:

```
val isEmpty =
\ Nil -> True
| Cons _ _ -> False
```

Here we have declared a function `isEmpty`

that takes a list and returns `True`

if and only if it is empty.
This is done by inspecting the way that list was constructed: Either it was constructed with the `Nil`

constructor, in which case it is an empty list by definition, or it was constructed with the `Cons`

constructor with some arguments (which we ignore with nested wildcard patterns), which means it is a non-empty list by definition.

We can combine named wildcard with restrictions:

```
val duplicateHead =
\ Nil -> Nil // equivalently: []
| Cons x l -> Cons x (Cons x l)
```

In the function `duplicateHead`

, different branches are selected based on the shape of the input list, just like in `isEmpty`

above.
However, if the input list is a `Cons`

element, the element and the remaining list are given the names `x`

and `l`

, respectively.
Sometimes it is useful to be able to name both substructures and the enclosing structure.
We may attach an extra name with the `as`

keyword:

```
val duplicateHead =
\ Nil -> Nil // equivalently: []
| (Cons x _) as l -> Cons x l
```

The result of `duplicateHead`

is the same as for `duplicateHead`

, but we have used the `as`

keyword to give the name `l`

to the *entire* non-empty input list, while still giving the head element the name `x`

.

Branches in a function can be selected by looking deeper into the arguments:

```
val isFirstTwoElementsFive =
// The list contains at least two elements and both of them are 5
\ Cons 5 (Cons 5 _) -> True
// The list does not start with two 5s
| _ -> False
```

The order of the patterns is important because the first match is picked.
Therefore, had we defined `isFirstTwoElementsFive`

as below, it would always return `False`

:

```
val isFirstTwoElementsFive =
\ _ -> False // Wrong! Any input will be caught by this pattern
| Cons 5 (Cons 5 _) -> True // This will never be reached
```

Pattern-matching is also supported for tuples.
A function that extracts the third element of a value of type `Tuple a b c`

can be defined as:

```
val third = \(_, _, c) -> c
```

The type of the `third`

function is `Tuple a b c -> c`

for any types `a`

, `b`

, and `c`

.

We can restrict the pattern of `third`

so that it requires the third value to be of type `Int`

:

```
val third1 = \(_, _, c : Int) -> c
```

### Record pattern matching¶

We can do pattern matching on records and their fields by writing the record name prefixed with a `?`

.
A record pattern can contain sub-patterns for each field.
The pattern match is successful if

- the specified record name in the pattern designates the record’s type or a supertype of the record, and
- all field patterns match their associated field value.

The following code snippet illustrates this:

```
// Address as defined above
type BusinessAddress : Address {
company : String
}
val isMainStreet =
// Bind the local name "sn" to contents of "streetName"
\ ?Address { streetName = sn } ->
sn = "Main street"
| _ -> False
val isMainStreet12 =
// Match the field values with literal values
\ ?Address {
streetName = "Main street",
houseNumber = 12
} -> True
| _ -> False
```

One important caveat to remember when using pattern matching on records is that they cause the type inferer to derive the most general record type – `Record`

– as the input type for the function.
Therefore, if you construct an instance of a record type and want to pattern match on it you must upcast it to `Record`

first:

```
// isMainStreet : Record -> True
val mainStreeAddresses = List::map isMainStreet [
BusinessAddress {
streetName = "Main street",
houseNumber = 12,
company = "Deon"
} :> Record,
Address {
streetName = "Wall st.",
houseNumber = 10
} :> Record,
BusinessAddress {
streetName = "Main street",
houseNumber = 17,
company = "Acme"
} :> Record
]
// [True, False, True]
```

## Conditional expressions (if-then-else)¶

It is possible to define conditional expressions using the syntax:

```
val a = if (True) 1.0 else 2.0 // = 1.0
val b = if (False) 1.0 else 2.0 // = 2.0
```

The condition must be some a value of the `Bool`

type.
We can also use more complex expressions:

```
val isGreaterThanTwo = \x -> x > 2
val g = \x -> if (isGreaterThanTwo x)
"greater than two"
else
"smaller than two"
val a = g 1 // = "smaller than two"
val b = g 3 // = "greater than two"
```

## Type case expressions¶

Type casing is used to split the control flow based on the type of a record. This is useful when we have a hierarchy of record types and want to perform different computations depending on which type is encountered. Given the two record definitions:

```
type Delivery : Event { deliveryMultiplier : Int }
type DroneDelivery : Delivery { droneDeliveryAddition : Int }
```

We can formulate a function that computes the prices for a `DroneDelivery`

and a `Delivery`

like so:

```
val deliveryCost = \(delivery : Delivery) ->
type d = delivery of {
// Here 'd' is a 'DroneDelivery', so we can access both fields.
DroneDelivery -> d.deliveryMultiplier * 100 + d.droneDeliveryAddition ;
// Here, 'd' is just a 'Delivery', so there is no droneDeliveryAddition field.
Delivery -> d.deliveryMultiplier * 100 ;
// Here we cannot access fields of 'd' because we don't know its type.
_ -> 100
}
```

A type case expression consists of several branches separated by `;`

.
The type case is evaluated to the first branch where the record type (left of the `->`

) is a super type of the input record.
There must always be a final *default case*, written with the `_`

wildcard syntax.
The record being cased on is bound to a name (`d`

in this example), and in each branch the name refers to a value with the appropriate record type.
Thus, in line 4 the `d`

is a `DroneDelivery`

record and therefore we may read both the field `deliveryMultiplier`

and `droneDeliveryAddition`

.
In line 6 the `d`

is a `Delivery`

record, so we can only read the field `deliveryMultiplier`

.
Finally, in line 8 `d`

is not accessible because we do not know the type of `d`

.

## Upcast annotation¶

Upcasts (`:>`

) are used to lift record expressions to a super type.
For instance we can write:

```
val delivery = \(amazon : Agent) -> DroneDelivery {
timestamp = #2018-07-20T20:18:04Z#, agent = amazon,
deliveryMultiplier = 2, droneDeliveryAddition = 50
} :> Delivery
```

Here `delivery`

will be of type `Delivery`

instead of `DroneDelivery`

to the type checker.
We can now use the `deliveryCost`

function above to calculate delivery costs: `deliveryCost delivery`

.
Note that `deliveryCost`

uses a type case expression to discern between differently instantiated records.
Calling the function with `delivery`

causes the `DroneDelivery`

case to be selected, as the value `delivery`

was instantiated as a `DroneDelivery`

, so a cost of `2 * 100 + 50`

is returned.

The upcast annotation also allows us to specify a list of events (of type `List Event`

):

```
type BikeDelivery : Event { recipient: Agent }
type BikeOrder : Event { amount: Int, recipient: Agent }
val bikeEvents = \(bob : Agent) -> \(alice : Agent) -> [
BikeDelivery {
timestamp = #2018-07-20T20:18:04Z#, agent = bob,
recipient = alice
} :> Event,
BikeOrder {
timestamp = #2018-07-20T20:18:04Z#, agent = bob,
recipient = alice, amount = 100
} :> Event
]
```

These upcasts are necessary, as `BikeDelivery`

and `BikeOrder`

are of different types and otherwise couldn’t be in the same list.

## Let-expressions¶

We use *let-expressions* to name sub-expressions within an expression:

```
val twelve =
let
val x = 5
val y = 7
in
x + y
```

In this example, `twelve`

is an expression in which `x`

and `y`

are *locally* bound to the values `5`

and `7`

.
Locally bound names are visible only in the expression after the associated `in`

keyword.
Thus, here we may use `x`

and `y`

in the expression `x + y`

to produce the value `12`

.

After the `let`

keyword we can use any pattern to deconstruct values:

```
val twelve =
let
val (x, y) = (5, 7)
in
x + y
```

In this example, a value of the type Tuple Int Int is created and immediately used in a pattern that assigns the left and right component of the pair to the names `x`

and `y`

, respectively.
In the body after the `in`

we can therefore use `x`

and `y`

in the same way as in the previous example.

One should be careful that the pattern always matches. The following example fails at run time as the empty list does not match a pattern for a non-empty list.

```
val fails =
let val Cons x xs = Nil in "should fail" // fails at run-time
```

The order the definitions of values in the let-expressions matter: early definitions are visible by later ones but not the other way around:

```
val twelve =
let
// val addTo = \n -> x + n // Wrong! 'x' is not in scope here!
val x = 5
val addTo = \n -> x + n // OK, addTo has 'x' in scope.
val y = 7
in
addTo y
```

## Type annotations¶

When working with records we are sometimes required to insert type-annotations in order to tell the type checker what kind of record we are projecting on.
The following is a function that takes a value of the type `Event`

and returns the `agent`

field:

```
val getAgent = \(e: Event) -> e.agent
```

Without the annotation `: Event`

on the function’s parameter, the type checker cannot know which type the function expects.
By inserting the annotation we make it possible for the type checker to continue with checking the function body.
Because the `Event`

type defines an `agent`

field, the type checker can infer that this function has the type `Event -> String`

.

## Equality checking¶

CSL allows equality checking using the `=`

operator for values of any type satisfying the following:

- It does not contain any occurrences of type variables.
- It does not contain any occurrence of a function type
`a -> b`

.- It is
non-recursiveother than the built-in`List`

type.- It does not contain any occurrences of the signed type
`Signed a`

.

Note that we can only test equality for elements of the same type, i.e. typing `5 = 5.0`

will result in a type error.

```
val a = [[1]] = [[1]]
// = True
val b = [[1], []] = [[1]]
// = False
val c = [[1]] = [[1], [1]]
// = False
type IntFloatOrNothing
| AnInt Int
| AFloat Float
| NoneOfTheAbove
val eqIntFloatOrNothing = \(x : IntFloatOrNothing) -> \y -> x = y
type AnIntAndAFloat {
theInt : Int,
theFloat : Float
}
val eqAnIntAndAFloat = \(x : AnIntAndAFloat) -> \y -> x = y
```