Scoping
When an entity is bound to name a binding is created.
A binding has a scope in which it is effective (or “visible”).
An entity can be a value, defined with val; a contract template, defined with template; or a contract, defined with contract.
In this section we will use the convention that a comment of the form // { a = 1, b : Int } means that there are two bindings in scope on the line of the comment: one binding of the name a to the value 1 and one binding of the name b to some value of type Int.
We use this to illustrate how the scoping of names behaves.
We illustrate most of the scoping rules with values (val), but the same rules apply for contract abbreviations (contract) and contract templates (template) unless otherwise specified.
Additional rules for recursive definitions also apply – see below.
Sequential bindings
In the basic case, the scope of a binding is the lexical substructure of the code that follows immediately after the binding itself. For example, consider the following code snippet:
val a = 1
val b = a + 1 // { a = 1 }
val c = b + 1 // { a = 1, b = 2}
// { a = 1, b = 2, c = 3 }
In the binding of b to a value, a is in scope and in the binding of c both a and b are in scope.
Recursive values are disallowed in CSL, so the binding of a to 1 is not visible to itself and likewise for b and c.
It is not allowed to redeclare definitions, so we cannot shadow existing top-level definitions like so:
val someValue = 10
val someValue = 2000 // not allowed
Simultaneous bindings
Sometimes it is not desirable to bind names sequentially. If we need to bind, e.g., three values to names and they are not dependent on one another, the order in which they are written in the source code should not have any effect on them. A block of simultaneous bindings may contain several bindings:
val severalWiths = let
val a = 1
with b = 2
with c = "hello"
with d = False
// with e = a
in d
Had we not commented out the last line in this example it would not have typechecked: we would have attempted to bind e to a before a had been bound.
Note that each individual binding in a block can be marked as a report, making it accessible by sic interfaces and subjecting it to the additional requirements of reports:
val report a = 1
with b = 2 // not a report
with report c = 3
Local scopes
It is also possible to explicitly mark where a scope should end: such scopes we call local scopes.
A binding can be introduced in a local scope by using the let … in construction (see also here and here).
The general form is as follows:
let
<bindings>
in
<body>
The <bindings> can be one or more bindings like described above; <body> is the scope in which these bindings are visible.
In the code following the <body> the definitions from <bindings> are out of scope.
The scoping rules for locally bound names in a let and on the top-level are the same.
In particular, sequential bindings can be “unrolled” as a sequence of nested let blocks:
val myVal0 =
let
val a = 1
val b = 2
val c = a + b
in
c
// is equivalent to
val myVal1 =
let val a = 1
in
let
val b = 2
val c = a + b
in c
// is equivalent to
val myVal2 =
let val a = 1
in
let val b = 2
in
let val c = a + b
in
c
When we are working in the value language, a let-expression is itself also a value.
This means that we may use it anywhere a value can be used:
val x = 2
val a = (let val x1 = 42 in x1 + 1) + (let val y = 15 in x + y)
// a = (42 + 1) + (2 + 15)
// { a = 60, x = 2 }
One must take care that the body of a let-expression does not accidentally span over more than what was intended.
For example, if we had forgotten the parentheses in the above code snippet the meaning would have been different because the inner x1 with a value of 42 would have been in scope in the second subexpression x1 + y as well:
val x = 2
val a = let val x2 = 42 in x2 + 1 + let val y = 15 in x2 + y
// a = 42 + 1 + 42 + 15
// { a = 100, x = 2 }
Locally scoped bindings do not differ from bindings at the top level apart from their scope.
We may for example also use simultaneous bindings in let-blocks:
val c = let
val a = 1
with b = 2
in
a + b // { a = 1, b = 2 }
Note that it is not allowed to shadow names locally in let blocks:
val x = 10
val f = let x = 5 in x // not allowed
Local scopes without let
Attention
This only applies to values, not to contract abbreviations or templates.
Aside from let-expressions, bindings with a local scope can be introduced in three ways:
with a function;
as a named event in the prefix contract construction;
with the type case construct; or
as value parameters for templates.
Function scope
Binding a name in a function is similar to binding a name in a let-expression.
The binding has a scope that covers the body of the function, and for everything outside of the function body the binding does not exist:
val f = \ x ->
x + 1 // { x : Int }
val x = f 1 // { f : Int -> Int }
val y = x + 1 // { f : Int -> Int, x = 2 }
Recall that parameters to functions are patterns; every variable in the pattern is introduced as a binding in the scope of the function body:
val g =
\ (x : Int) ->
\ (a, b) ->
(a + x, b + x) // { a : Int, b : Int, x : Int }
val p = g 1 (10, 11) // { g : Int -> Tuple Int Int -> Tuple Int Int }
// { g : Int -> Tuple Int Int -> Tuple Int Int, p = (11, 12) }
Bindings of names introduced by patterns in multi-case functions only have scope in the body of the their own case:
type T | Left Int | Right Int
val h =
\ (x : Int) ->
\ Left l -> Left (l + x) // { x : Int, l : Int }
| Right r -> Right (r + x) // { x : Int, r : Int }
val l = h 1 (Left 10) // { h : Int -> T -> T }
val r = h 2 (Right 10) // { h : Int -> T -> T, l : T }
// { h : Int -> T -> T, l : T, r : T }
Note that it is not allowed to shadow names in parameter patterns:
val x = 10
val f = \x -> x // not allowed
Prefix-contract scope
If a prefix contract binds a name to the matched event, that binding has a scope that covers the predicate and the residual of the prefix contract:
type M0 : Event { x : Int }
contract c0 =
<*> e0 : M0
where e0.x > 0 // { e0 : M0 }
then
<*> e1 : M0
where e1.x > e0.x // { e0 : M0, e1 : M0 }
then
<*> e2 : M0
where e2.x > e1.x // { e0 : M0, e1 : M0, e2 : M0 }
The scope only spans the residual contract of the prefix in which the binding is made; hence, the scoping can be altered with parentheses:
type M1 : Event { x : Int }
contract c1 =
(<*> e0 : M1
where e0.x > 0 // { e0 : M1 }
then
<*> e1 : M1
where e1.x > e0.x // { e0 : M1, e1 : M1 }
)
then
<*> e2 : M1
where e2.x > 0 // { e2 : M1 }
Bindings introduced this way cannot shadow one another:
contract c2 =
<*> e : Event
then
<*> e : Event // fails check because we bind e again
Type case scope
The type case construct introduces a binding of the value that is being matched against in the scope of all cases. The binding in each case will have the same name but a value of a different type, as it will bind the name to a value of the specific type of the case. The mandatory default case is the exception: here, the type case construct does not introduce any bindings, so the only ones in scope are those that are in the scope of the entire construct:
type Rec { def : Int }
type A : Rec { aField : Int }
type B : Rec { bField : Int }
val fn = \(r : Rec) ->
type x = r of { // { r : Rec }
A -> x.aField + x.def; // { r : Rec, x : A }
B -> x.bField + x.def; // { r : Rec, x : B }
_ -> r.def // { r : Rec }
}
val a = fn (A { aField = 1, def = 1 } :> Rec) // { fn : Rec -> Int }
val b = fn (B { bField = a, def = 2 } :> Rec) // { fn : Rec -> Int, a = 2 }
val c = fn (Rec { def = 42 }) // { fn : Rec -> Int, a = 2, b = 4 }
// { fn : Rec -> Int, a = 2, b = 4, c = 42 }
Note that in the default case above only {r : Rec} is in scope.
This binding is in scope because it was introduced by the function in which the type case expression resides.
Value parameters in templates
Bindings for value parameters in contract templates behave like bindings introduced in functions. A binding is made for each variable name in the patterns, and the scope of those bindings is the entire body of the contract template:
type E : Event { x : Int }
contract a = \(x : Int) -> \(a : Int, b : Int) ->
<*> e1: E // { a : Int, b : Int, x : Int }
where e1.x = x // { a : Int, b : Int, x : Int, e1 : E }
then
<*> e2: E // { a : Int, b : Int, x : Int, e1 : E }
where e2.x = a // { a : Int, b : Int, x : Int, e1 : E, e2 : E }
Recursive bindings
So far we have only discussed scoping that disallows recursion.
The scoping rules for contracts and templates are the same as for values regarding the difference between sequentially and simultaneously bound templates, but they also handle the case of recursive bindings.
A recursive contract is written by adding the rec modifier after contract when binding it.
Adding this modifier has the effect that the binding can be referred to in its own definition – the binding is in scope in its definition:
// Error: 'bad' not in scope
// contract bad = <*> Event then bad
// OK: 'good' is in scope
contract rec good = <*> Event then good
The addition of recursion is orthogonal to the distinction between sequential and simultaneous bindings.
That is, in the following code snippet we sequentially bind three recursive contracts, each one able to see both itself (due to rec) and the preceding definitions:
contract rec recA = <*> Event then recA
contract rec recB = recA or <*> Event then recB
contract rec recC = recA or recB or <*> Event then recC
It is also possible to simultaneously bind recursive contracts. This has the effect that all bindings from the simultaneous block are visible in all of the right-hand-sides, thereby allowing us to write mutually recursive definitions:
contract rec recA = <*> Event then recB
with recB = <*> Event then recA
// This would fail as 'recA' and 'recB' are not scope due to the missing 'rec'
// contract recA = <*> Event then recB
// with recB = <*> Event then recA
Overview
The table below is a summary of the different ways values, contracts, and contract templates can be assigned scope:
Kind |
Sequential |
|
|
|
Function |
Prefix contract |
Type case |
|---|---|---|---|---|---|---|---|
|
X |
X |
X |
X |
X |
X |
|
|
X |
X |
X |
X |
|||
|
X |
X |
X |
X |