Mutable State

Typing relation. Usually written Γe:τ, where Γ is a map from identifiers to types, e is an expression, and τ is a type.

TypeContextExpression:Type

Anonymous function.

λParameterName:ParameterType.Body

Type abstraction.

ΛTypeVariable.Body

Function type.

ParameterTypeReturnType

Subtyping relation.

Read τ<:τ as: τ is a subtype of τ. If τ and τ are records, τ has a superset of the fields in τ. Alternatively, anything that expects a τ can take a τ.

In previous notes, we introduced IMP. IMP is a very simple language—it has a single global scope and variables in that scope are mutable. When we discussed functional programming, did it in the context of FL, which has first-class functions but does not have mutable state. This was a deliberate choice: it's surprisingly tricky to include mutable state and first-class functions in the same language.

In this section, we'll extend FL with mutable state in the form of reference cells (aka ref cells or references). A ref cell is a new kind of value that acts like a mutable container. Ref cells have three associated operations:

Ref cells are not very expressive on their own, but adding them to FL forces us to deal with the problems of mutable state. In combination of other features like records, ref cells allow us to implement a wide variety of mutable data structures.

References & Heaps

::== | < | > | + |  |  | / | and | oroperatorse::=xvariable|ninteger|bboolean|e eapplication|λx.efunction abstraction|if e then e else econditional|eeoperator application|{xi=eii1n}record|e.xfield access|let x=e in elet binding|ref ereference cell creation|!ereference cell read|e:=ereference cell write
def seq(e1, e2):
"""Desugars e1; e2 to let _ = e1 in e2"""
return Let("_", e2, e1)
def incr(e):
"""Desugars incr e to let x = e in x := !x + 1"""
return Let("x", e, Assign(Var("x"), Deref(Var("x")) + Int(1)))
# let x = ref 1 in let r = {a = x; b = x} in incr r.a
term = Let("x", Ref(Int(1)),
Let("r", Record({"a": Var("x"), "b": Var("x")}),
incr(Proj(Var("r"), "a"))))
print_cbv_ref_eval(term)
הההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההההה
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Help

Last updated: 2023-05-05 Fri 18:04