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 shorthand, 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. For the latter, the additional rules for recursive templates 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. A binding can shadow an existing one in a let construction:

val shadowing = let
  val a = 1
  val b = a + 1 // { a = 1 }
  val a = 42    // { a = 1, b = 2 }
  val c = a + 1 // { a = 42, b = 2 }
in c
// { a = 42, b = 2, c = 43 }

Because the second binding of a shadows the first one, c = 43 whereas b = 2. It is not allowed to redeclare top-level 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. In such a case we can bind them simultaneously with the with keyword:

val simultaneousBinding = let
  val a = 42

  // Simultaneous binding of 'a' and 'b'
  val  a = 1 // { a = 42 }
  with b = a // { a = 42 }

  val d = a  // { a = 1, b = 42 }
in d
// { a = 1, b = 42, d = 1 }

Here we bind two different values to a, but the value bound to b is the first one of those two because the second one is bound simultaneously with b and hence is out of scope for the same reason that a is out of scope in its own binding. However, once the block of simultaneous bindings is ended, the new binding of a will shadow the old one, so the new value of 1 will be used in the binding of d. Note that a block of simultaneous bindings may contain several bindings, not just two:

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.

Local scopes

As the examples above have demonstrated, bindings can shadow one another if a binding that is identical to an existing one is introduced in a scope. In other words, when a binding is shadowed, its scope is implicitly ended in the entire scope of the new binding. 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 letin 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.

It is possible for a local binding to shadow a global one:

val a = 5
val b = // { a = 5 }
let
  val a = 7
in a // { a = 7 }
// {a = 5, b = 7 }

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 x = 42 in x + 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 a = 42
val c = let
  val  a = 1     // { a = 42 }
  with b = a * 2 // { a = 42 }
  in
  a + b          // { a = 1, b = 84 }
val d = let
  val c = c + 7  // { a = 42, c = 85 }
  in
  c              // { a = 42, c = 92 }
// { a = 42, c = 85, d = 92 }

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:

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 }

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 }
template 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 }
template 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 can shadow one another just like bindings introduced in any other way:

type E0 : Event { x : Int }
type E1 : Event { x : Int }
template C2() =
  <*> e : E0
  where e.x > 0 // { e : E0 }
  then
  <*> e : E1
  where e.x < 0 // { e : E1 }

In this example, the first e is bound to an event whose x field must be greater than zero while the second e is bound to an event whose x field must be negative.

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 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 }
template 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 contract templates are the same as for values and contract abbreviations regarding the difference between sequentially and simultaneously bound templates, but they also handle the case of recursive templates. A recursive template is written by adding the rec modifier after template when binding it. Adding this modifier has the effect that the template can be referred to in its own definition – the binding is in scope in its definition:

// Error: Template Bad not in scope
// template Bad() = <*> Event then Bad()

// OK: Template Good is in scope
template 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:

template rec RecA() = <*> Event then RecA()
template rec RecB() = RecA() or <*> Event then RecB()
template 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 templates:

template 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'
// template RecA() = <*> Event then RecB()
// with     RecB() = <*> Event then RecA()

Overview

The table below is a summary of the different ways values, contract abbreviations, and contract templates can be assigned scope:

Kind Sequential with rec let Function Prefix contract Type case
val X X   X X X X
contract X X   X      
template X X X X