# 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.