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 section 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", "\"".

• Instant, 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).

The value expression language also supports the unit type Unit which has only one element.

Unit trivia

In fact, Unit is just an alias for Tuple i.e. the tuple with 0 elements.

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.

• ContractInstance 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 64-bit integers as their underlying implementation. They are in the range from -9223372036854775808 to 9223372036854775807. Calculations with integers wrap around at their bounds: in CSL 5000000000000000000 + 5000000000000000000 = -8446744073709551616 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.

Instant literals

Instant 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 Instant 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#

Instants specified with different offsets from UTC 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 Instant 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 Instant 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 Instant, 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, 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 }
contract 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, Instant, Year, YearMonth, Date, Time, ZoneOffset, and Duration

• 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 Instant 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, Instant, 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 Instant Float, and we can use x and h anywhere we need a OneOrTheOther Int Float and so on.

Sum types may not be recursive. In other words, the type being defined is not available in its own definition, so the following code is not allowed:

type Tree a
  | Empty
  | Branch a (Tree a) (Tree a)

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

The Bool type is not a part of the standard library; instead, it is a builtin types in the expression language. This is because it has special support in the if syntax.

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.

Lists

If CSL supported recursive datatypes, then it would be possible to define lists as follows:

.. code-block:: csl-unchecked

type List a

Nil

Cons a (List a)

Internally, lists are represented as if they were defined this way.

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)

It is useful to have a more concise notation for lists 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 func, and returns a new function. This new function takes a single argument, calls it x and invokes the function bound as func 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:

1. that they are monomorphic, that is, their argument and result types do not contain any type variables, and

2. 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 entrypoints, 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

Each pattern-matching function must be exhaustive, which means that every potential case is considered. For instance, the following function is rejected:

val twoBits =
      \ (False, False) -> 0
      | (False, True)  -> 1
      | (True,  True)  -> 3

It does not cover the (True, False) case. Each function is considered in isolation, so the following is also rejected even though it actually does cover all cases, because the inner function is checked without taking the outer function’s pattern into account:

val twoBits =
      \ (False, False) -> 0
      | other ->
        (\ (False, True) -> 1
         | (True, False) -> 2
         | (True, True) -> 3) other

Direct pattern matching syntax

In addition to pattern matching functions, you can also directly pattern match on a value using the match keyword, for example:

val addOrSubtract = \shouldAdd -> \x -> \y -> match shouldAdd with {
  | True -> x + y
  | False -> x - y
}

The general form of the match expression is:

match <EXPRESSION> with {
  | <PATTERN_0> -> <EXPRESSION_0>
  | <PATTERN_1> -> <EXPRESSION_1>
  ...
  | <PATTERN_N> -> <EXPRESSION_N>
}

Remember that if you write lambdas within the body of a match expression, you should parenthesize them. The below example will not work as intended:

val addOrSubtract = \shouldAdd -> match shouldAdd with {
  | True -> \x -> \y -> x + y
  | False -> \x -> \y -> x - y
}

In this case, the second case of the match expression will be parsed as belonging to the innermost lambda of the first case, i.e:

val addOrSubtract = \shouldAdd -> match shouldAdd with {
  | True -> \x ->
    (\ y -> x + y
     | False -> \x -> \y -> x - y)
}

To avoid this, put a parenthesis around your inner lambdas.

val addOrSubtract = \shouldAdd -> match shouldAdd with {
  | True -> (\x -> \y -> x + y)
  | False -> (\x -> \y -> x - y)
}

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.

CSL only permits patterns that are guaranteed to match all values in let. The following example is not allowed, because the empty list could otherwise cause a run-time failure.

val fails =
    let val Cons x xs = Nil in "should fail"

The error messages is helpful:

Missing cases: Nil

The order of 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.

Polymorphic type annotations

We can also annotate polymorphic definitions. However, we must first explicitly bind the type parameters before we can refer to them in annotations. The following definition is therefore not valid.

// Not valid, as `a` is not in scope
val my_annotated_id_1 : a -> a = \x -> x

We bind type parameters by enclosing them in angle brackets (< and >) prior to the defined name. For example, the function that swaps the elements of a pair can be annotated as follows:

val <a, b> swap : Tuple a b -> Tuple b a = \(x, y) -> (y, x)

Type variables, once bound, can be referenced in any pattern, and not just top level type signatures:

val <a> maybeFallback = \fallback -> \Some (x : a) -> x | None -> fallback

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-recursive other 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

External declarations

The CSL expression language is by design more limited than a typical general purpose programming language. However, there are situations where workflow specific functionality require the ability to call out to third party libraries. To accommodate this, you can declare external values and functions in CSL. These externals will have to be implemented by the operator of the specific CSL platform on which you’ll be instantiating any contracts that depend on them.

To declare an external function repeatString that repeats a given string a number of times, we write the following:

external prim__repeatString : String -> Int -> String

The declaration is started by the keyword external and followed by prim__ and a name you decide. Then follows a colon and the type of the external. Your externals have to be named starting with prim__.

You can use an external like any normal function. However, it is common to alias it with a normal val in order to hide the fact that it is an external from callers.

val repeatString = prim__repeatString