Miscellaneous Other Notes
Extensible Variants
To complete our discussion of ML-like languages, we need a theory of extensible
variants. We will do this by adding a new type constructor \(\tau\ tag\), a reified
type tag that will be used to differentiate dynamically-added variants. It, and
the exn
type, is defined by the rules
\[\require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \UnaryInfC{$\Gamma \vdash \tau\ tag:*$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \UnaryInfC{$\Gamma \vdash newtag[\tau]:\tau\ tag$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau\ tag$} \AxiomC{$\Gamma \vdash e_2:\tau$} \BinaryInfC{$\Gamma \vdash tag(e_1, e_2):exn$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau\ tag$} \AxiomC{$\Gamma \vdash e_2:exn$} \AxiomC{$\Gamma, x:\tau \vdash e_3:\tau'$} \AxiomC{$\Gamma \vdash e_4:\tau'$} \QuaternaryInfC{$\Gamma \vdash iftag(e_1,e_2,x.e_3,e_4)$} \end{prooftree} \]
Evaluating iftag
checks if the expression e_2
is tagged with e_1
. If so,
bind the captured \(\tau\) value to x
in e_3
, otherwise, evaluate e_4
.
The initial continuation
One issue with our CPS-conversion translation is that we currently produce, as our final program, a strange expression \(k.k_{ex}.e\), with these bound \(k\) and \(k_{ex}\). At the top level, these are effectively free! To resolve this, we will define the judgment
\[\Gamma \vdash_{prod} e:\tau \rightsquigarrow e'\]
for use on the top level program. We can then define
\[ \begin{prooftree} \AxiomC{$\cdot \vdash e:\overline{\tau} \rightsquigarrow k.k_{ex}.e'$} \UnaryInfC{$ \begin{aligned} \cdot \vdash_{prod} e:\tau \rightsquigarrow &let\ k=\lambda(x:\overline{\tau}).halt\ in\\ &let\ k_{ex} = \lambda(x:\overline{\tau_{ex}}). (print\ \unicode{x201C}\text{uncaught exception}\unicode{x201D}; halt)\ in\\ &e' \end{aligned} $} \end{prooftree} \]
(where ;
represents obvious sequencing)
Note that we simply throw the result of the entire program on the floor and halt. With this setup, a program's practical usage is in its IO behavior, not in the result of its evaluation. It is possible to set it up otherwise, but that requires more complicated translations at the top level.