Mutable State
\[ \newcommand{\target}[2]{\class{mathjax-symbol mathjax-symbol-#1}{#2}} \newcommand{\type}[3]{#1 \target{type}{\vdash} #2 \target{type}{:} #3} \newcommand{\abs}[3]{\target{abs}{\lambda} #1 \target{abs}{:} #2\target{abs}{.} #3} \newcommand{\tabs}[2]{\target{tabs}{\Lambda} #1 \target{tabs}{.} #2} \newcommand{\arrow}{\target{arrowT}{\rightarrow}} \newcommand{\subt}{\target{subT}{<:}} \newcommand{\Int}{\mathsf{Int}} \newcommand{\Bool}{\mathsf{Bool}} \newcommand{\lett}[3]{\mathsf{let}\ \mathit{#1} : #2 = #3\ \mathsf{in}} \newcommand{\letu}[2]{\mathsf{let}\ \mathit{#1} = #2\ \mathsf{in}\ } \newcommand{\ite}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3} \DeclareMathOperator{\proj}{.} \newcommand{\object}[1]{\mathsf{object}\ #1\ \mathsf{end}} \newcommand{\call}[2]{#1 \# \mathit{#2}} \newcommand{\method}[2]{\mathsf{method}\ \mathit{#1} = #2} \newcommand{\self}{\mathit{self}} \newcommand{\super}{\mathit{super}} \newcommand{\refc}{\mathsf{ref}\ } \newcommand{\inherit}[2]{\mathsf{inherit}\ #1\ \mathsf{as}\ \mathit{#2}} \newcommand{\pack}[3]{\mathsf{pack}\ (#1, #2)\ \mathsf{as}\ #3} \newcommand{\unpack}[4]{\mathsf{unpack}\ (#1, #2) = #3\ \mathsf{in}\ #4} \newcommand{\override}{\ \mathsf{override}\ } \newcommand{\loc}[1]{l_{#1}} \]
Typing relation. Usually written \(\type{\Gamma}{e}{\tau}\), where \(\Gamma\) is a map from identifiers to types, \(e\) is an expression, and \(\tau\) is a type.
\(\type{\mathrm{Type Context}}{\mathrm{Expression}}{\mathrm{Type}}\)
Anonymous function.
\(\abs{\mathrm{Parameter Name}}{\mathrm{Parameter Type}}{\mathrm{Body}}\)
Type abstraction.
\(\tabs{\mathrm{Type Variable}}{\mathrm{Body}}\)
Function type.
\(\mathrm{Parameter Type} \arrow \mathrm{Return Type}\)
Subtyping relation.
Read \(\tau \subt \tau'\) as: \(\tau\) is a subtype of \(\tau'\). If \(\tau\) and \(\tau'\) are records, \(\tau\) has a superset of the fields in \(\tau'\). Alternatively, anything that expects a \(\tau'\) can take a \(\tau\).
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:
- Create: \(\mathsf{ref}\ e\) creates a cell that contains the value of \(e\).
- Read: If \(e\) evaluates to a reference cell, then \(!e\) returns its contents.
- Write: If \(e\) evaluates to a reference cell \(r\), then \(e := e'\) replaces the contents of \(r\) with the value of \(e'\).
FLis an expression oriented language; unlikeIMP, it doesn't separate expressions from statements.
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.