Skip to main content


When you have a leased value, you can lease it again, creating a sublease. Here is an example where we create a lease l1 and then a sublease l2. Try putting your cursor after let l2: leased = l1, you will see that both p and l1 are drawn with "dashes", indicating that those variables have leased our their object to another:

class Point(x: our, y: our)

let p: my = Point(22, 44)

# `l1` is leased from `p`
let l1: leased = p

# `l2` is leased from `l1`
let l2: leased = l1
# β–²
# β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜

# You see:
# β”Œβ”€β”€β”€β”€β”
# β”‚ β”‚
# β”‚ p β”œβ•Œmyβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ–Ίβ”Œβ”€β”€β”€β”€β”€β”€β”€β”
# β”‚ β”‚ β”‚ Point β”‚
# β”‚ l1 β”œβ•Œleasedβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ•Œβ–Ίβ”‚ ───── β”‚
# β”‚ β”‚ β”‚ x: 22 β”‚
# β”‚ l2 β”œβ”€leased──────────►│ y: 44 β”‚
# β”‚ β”‚ β””β”€β”€β”€β”€β”€β”€β”€β”˜
# β””β”€β”€β”€β”€β”˜

Subleases can be ended just like any other lease, except that a sublease can be terminated either by the lessor (l1, here) or by the original owner (p, here). Try inserting commands like l1.x += 1 or p.x += 1 and see how the diagram changes.

Giving a leased value​

When you give a lease value, it results in a sublease. This preserves the rule for "give", that giving an object always creates a new value with equivalent permissions: a sublease permits all the same access to the object as the original lease.

class Point(x: our, y: our)
let p: my = Point(22, 44)
let l1: leased = p
let l2: any = l1.give # subleases from `l1`
l2.x += 1 # modifies the `Point`