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
.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.
DateTime
literals¶
The literal format for Int
, Float
, and String
are straight-forward from the examples above.
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 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
andFloat
. Note that we don’t have implicit conversion of numeric types. That means2.0 * 4
will be rejected by the type checker.Equate (
=
):Equate
Int
,Float
,String
,DateTime
,Duration
,Agent
, andContractId
.Comparison operators (
<
,>
,<=
, and>=
):Works on
Int
,Float
, andDateTime
.Logical operators (“and”
&&
and “or”||
):Combine
Bool
values.Unary minus (
-
):Negates an
Int
orFloat
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 x = 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 r = 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 = \f -> \x -> f 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
- 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 = \(r : Delivery) ->
type d = r 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