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.

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 are a couple of primitive types that you can manipulate but you cannot construct in the syntax:

• Agent which represents agents that can send events.
• ContractId which represents an identifier given to an instantiated contract.
• PublicKey which represents a cryptographic public key used for asymmetric encryption.
• Signed which represents a string signed by some private 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:

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

2. 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#

DateTimes 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

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 and 3.001 seconds
val duration3 = #-P1DT2.5H3.001S#   // negative (1 day, 2 hours and 3.001 seconds)
val duration4 = #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 value contains a message that was signed by some private key. You can check if a Signed value was signed by a private key corresponding to a specific private, and you can also extract the message from the Signed 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 (=):

  Equate Int, Float, String, DateTime, Duration, Agent, and ContractId.

• 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 OneOrTheOthers 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.

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.

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

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

1. the specified record name in the pattern designates the record’s type or a supertype of the record, and
2. 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 most of the primitive types. Int, Float, String, DateTime, Duration, Agent, and ContractId all support it, and the result is a Bool value.

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.

We cannot check equality of record types, lists or tuples, or of user-defined types created with the type construct. We also cannot test equality on the Bool type itself using =, so writing True = False results in a type error. Finally, PublicKey and Signed do not support the = operator.

Equality of lists

For lists of Int, Float, String and DateTime types, appropriate equality checks are available as part of the standard library. For lists of other types, List::equalsWith can be used, for instance to compare lists of lists of Int values, we can use the following code:

val a = List::equalsWith List::Int::equals [[1]] [[1]]
//    = True

val b = List::equalsWith List::Int::equals [[1], []] [[1]]
//    = False

val c = List::equalsWith List::Int::equals [[1]] [[1], [1]]
//    = False

Equality of sum types

For most sum types, we can specify an equality function ourselves, for instance:

type IntFloatOrNothing
  | AnInt Int
  | AFloat Float
  | NoneOfTheAbove

val eqIntFloatOrNothing =
  \ AnInt x ->
    (\AnInt y -> x = y
     | _ -> False)
  | AFloat x ->
    (\AFloat y -> x = y
    | _ -> False)
  | NoneOfTheAbove ->
    (\NoneOfTheAbove -> True
    | _ -> False)

Equality of record types

Similarly, equality for record types can be checked by comparing records field by field:

type AnIntAndAFloat {
  theInt : Int,
  theFloat : Float
}

val eqAnIntAndAFloat =
  \(r1 : AnIntAndAFloat) -> \(r2 : AnIntAndAFloat) ->
    r1.theInt = r2.theInt &&
    r1.theFloat = r2.theFloat

In our examples both for the records and for sum types, we rely on the presence of equality checking functions for underlying types – Int and Float. However, if our record type had a Bool field, we would first need to define an equality check for Bool and use that in place of = operator:

type AnIntAndABool {
  theInt : Int,
  theBool : Bool
}

val eqB =
\ True  -> (\True  -> True | False -> False)
| False -> (\False -> True | True -> False)

val eqAnIntAndABool =
  \(r1 : AnIntAndABool) -> \(r2 : AnIntAndABool) ->
    r1.theInt = r2.theInt &&
    eqB r1.theBool r2.theBool