\documentclass[]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
    \usepackage{xltxtra,xunicode}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Mapping=tex-text,Scale=MatchLowercase}
  \newcommand{\euro}{€}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{\usepackage{microtype}}{}
\usepackage[margin=1in]{geometry}
\usepackage{color}
\usepackage{fancyvrb}
\newcommand{\VerbBar}{|}
\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
% Add ',fontsize=\small' for more characters per line
\newenvironment{Shaded}{}{}
\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\BuiltInTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{#1}}
\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\ExtensionTok}[1]{#1}
\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
\newcommand{\ImportTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{\textbf{#1}}}
\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\NormalTok}[1]{#1}
\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
\newcommand{\RegionMarkerTok}[1]{#1}
\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\ifxetex
  \usepackage[setpagesize=false, % page size defined by xetex
              unicode=false, % unicode breaks when used with xetex
              xetex]{hyperref}
\else
  \usepackage[unicode=true]{hyperref}
\fi
\hypersetup{breaklinks=true,
            bookmarks=true,
            pdfauthor={Justin Le},
            pdftitle={Extreme Haskell: Typed Expression EDSLs (Part 1)},
            colorlinks=true,
            citecolor=blue,
            urlcolor=blue,
            linkcolor=magenta,
            pdfborder={0 0 0}}
\urlstyle{same}  % don't use monospace font for urls
% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\setcounter{secnumdepth}{0}

\title{Extreme Haskell: Typed Expression EDSLs (Part 1)}
\author{Justin Le}
\date{July 7, 2026}

\begin{document}
\maketitle

\emph{Originally posted on
\textbf{\href{https://blog.jle.im/entry/extreme-haskell-typed-expression-edsls-1.html}{in
Code}}.}

\documentclass[]{}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
\else % if luatex or xelatex
  \ifxetex
    \usepackage{mathspec}
    \usepackage{xltxtra,xunicode}
  \else
    \usepackage{fontspec}
  \fi
  \defaultfontfeatures{Mapping=tex-text,Scale=MatchLowercase}
  \newcommand{\euro}{€}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{\usepackage{microtype}}{}
\usepackage[margin=1in]{geometry}
\ifxetex
  \usepackage[setpagesize=false, % page size defined by xetex
              unicode=false, % unicode breaks when used with xetex
              xetex]{hyperref}
\else
  \usepackage[unicode=true]{hyperref}
\fi
\hypersetup{breaklinks=true,
            bookmarks=true,
            pdfauthor={},
            pdftitle={},
            colorlinks=true,
            citecolor=blue,
            urlcolor=blue,
            linkcolor=magenta,
            pdfborder={0 0 0}}
\urlstyle{same}  % don't use monospace font for urls
% Make links footnotes instead of hotlinks:
\renewcommand{\href}[2]{#2\footnote{\url{#1}}}
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\setcounter{secnumdepth}{0}

\textbackslash begin\{document\}

I always say, inside every Haskeller there are two wolves, living on opposite
ends of the Haskell Fancy Code Spectrum. Are you going to write ``simple
Haskell'', using basic GHC 2010 tools and writing universal Haskell that every
introductory course offers, trying to keep the code as immediately
understandable and accessible? Or are you going to pile in all of the Haskell
type system and evaluation tricks you can find and turn on all the extensions,
and go full fancy?

In my
\href{https://blog.jle.im/entry/levels-of-type-safety-haskell-lists.html}{Seven
Levels of Type Safety} post, I described different extremes of type safety and
fancy code. I talked about how writing effective code was finding the correct
compromise for the level of communication and safety you need.

But this is not that kind of blog post. This is the kind of blog post where we
celebrate terrifying type-safety, facetious fanciness, and masochistic
meta-analysis. This series is about what happens when we dare to go full fancy.
Let's write code that is so inscrutable, so painful and torturous to write, yet
so \emph{undeniably useful} that you can't help but try to throw it into every
single thing you write and will feel a gnawing emptiness in your soul until you
do.

As our example, let's write a type-safe method to specify your program as a
series of states, with triggered transitions between them: a type-safe state
machine graph using a type-safe lambda calculus. We want to specify this in a
way that we can write once and then:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  be interpretable in a type-safe way within Haskell.
\item
  be inspectable with visualizable control flow.
\item
  be compilable to multiple actual back-ends, letting you run the same function
  under multiple implementations.
\end{enumerate}

This exact thing is something I've needed and used multiple times now in
projects. I want to specify one program graph within Haskell, but in a way that
can compile both in C and javascript while also being visualizable and
interactively explorable.

Once you go down this road, everything you ever write will feel woefully unsafe
and limited. And everything you want to write will be hopelessly inscrutable by
normal humans and borderline unusable. But such is the curse we all bear. Turn
around now, you have been warned.

This post will build up the embedded typed expression language. Part 2 will use
that expression language to define typed state machines with embedded predicates
and visualize them, and Part 3 will compile those machines to different
languages and verify they execute identically, with some live demos.

All of the code here is
\href{https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/flake.nix}{available
online}, and if you check out the repo and run \texttt{nix\ develop} you should
be able to load it all in ghci:

\begin{Shaded}
\begin{Highlighting}[]
\ExtensionTok{$}\NormalTok{ cd code{-}samples/typed{-}sm{-}lc}
\ExtensionTok{$}\NormalTok{ nix develop}
\ExtensionTok{$}\NormalTok{ ghci}
\ExtensionTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ :load ExprStage1.hs}
\end{Highlighting}
\end{Shaded}

\section{The Lambda Calculus}\label{the-lambda-calculus}

Let's derive a way to express an algorithm or expression in Haskell that can be
reified and analyzed within Haskell, and eventually be a form we can compile to
different backends, interpret in Haskell, or generate Graphviz visualizations
for.

\subsection{A First Pass}\label{a-first-pass}

One basic thing we can do is start with:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L18{-}L34}

\KeywordTok{data} \DataTypeTok{Prim} \OtherTok{=} \DataTypeTok{PInt} \DataTypeTok{Int} \OperatorTok{|} \DataTypeTok{PBool} \DataTypeTok{Bool} \OperatorTok{|} \DataTypeTok{PString} \DataTypeTok{String}
  \KeywordTok{deriving}\NormalTok{ (}\DataTypeTok{Eq}\NormalTok{, }\DataTypeTok{Show}\NormalTok{)}

\KeywordTok{data} \DataTypeTok{Op} \OtherTok{=} \DataTypeTok{OPlus} \OperatorTok{|} \DataTypeTok{OTimes} \OperatorTok{|} \DataTypeTok{OLte} \OperatorTok{|} \DataTypeTok{OAnd}
  \KeywordTok{deriving}\NormalTok{ (}\DataTypeTok{Eq}\NormalTok{, }\DataTypeTok{Show}\NormalTok{)}

\KeywordTok{data} \DataTypeTok{Expr}
  \OtherTok{=} \DataTypeTok{EPrim} \DataTypeTok{Prim}
  \OperatorTok{|} \DataTypeTok{EVar} \DataTypeTok{String}
  \OperatorTok{|} \DataTypeTok{ELambda} \DataTypeTok{String} \DataTypeTok{Expr}
  \OperatorTok{|} \DataTypeTok{EApply} \DataTypeTok{Expr} \DataTypeTok{Expr}
  \OperatorTok{|} \DataTypeTok{EOp} \DataTypeTok{Op} \DataTypeTok{Expr} \DataTypeTok{Expr}
  \OperatorTok{|} \DataTypeTok{ERecord}\NormalTok{ (}\DataTypeTok{Map} \DataTypeTok{String} \DataTypeTok{Expr}\NormalTok{)}
  \OperatorTok{|} \DataTypeTok{EAccess} \DataTypeTok{Expr} \DataTypeTok{String}
  \OperatorTok{|} \DataTypeTok{EChoice} \DataTypeTok{String} \DataTypeTok{Expr}
  \OperatorTok{|} \DataTypeTok{ECase} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{Map} \DataTypeTok{String}\NormalTok{ (}\DataTypeTok{String}\NormalTok{, }\DataTypeTok{Expr}\NormalTok{))}
  \KeywordTok{deriving}\NormalTok{ (}\DataTypeTok{Eq}\NormalTok{, }\DataTypeTok{Show}\NormalTok{)}
\end{Highlighting}
\end{Shaded}

And you can write \texttt{(\textbackslash{}x\ -\textgreater{}\ x\ *\ 3)\ 5} as:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L36{-}L37}

\OtherTok{fifteen ::} \DataTypeTok{Expr}
\NormalTok{fifteen }\OtherTok{=} \DataTypeTok{ELambda} \StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OTimes}\NormalTok{ (}\DataTypeTok{EVar} \StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{))) }\OtherTok{\textasciigrave{}EApply\textasciigrave{}} \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{5}\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The strings in \texttt{ELambda} introduce variables, and \texttt{EVar} refers to
the bound variable. As you can see, this is\ldots pretty untyped. We could
easily write something that is meaningless:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L67{-}L69}

\OtherTok{badTypeExample ::} \DataTypeTok{Expr}
\NormalTok{badTypeExample }\OtherTok{=}
  \DataTypeTok{EOp} \DataTypeTok{OAnd}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{2}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

Of course, GHC can typecheck our code if we literally write
\texttt{\textbackslash{}x\ -\textgreater{}\ x\ +\ 3} and reject
\texttt{1\ \&\&\ 2}. But we aren't trying to build opaque Haskell code here,
we're trying to represent our expression as an ADT that we can analyze
\emph{within} the language.

If we want a record projection and one labeled choice with a case analysis over
it:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L39{-}L62}

\OtherTok{recordExample ::} \DataTypeTok{Expr}
\NormalTok{recordExample }\OtherTok{=}
  \DataTypeTok{EOp}
    \DataTypeTok{OPlus}
\NormalTok{    ( }\DataTypeTok{EAccess}
\NormalTok{        ( }\DataTypeTok{ERecord} \OperatorTok{$}
\NormalTok{            M.fromList}
\NormalTok{              [ (}\StringTok{"value"}\NormalTok{, }\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{)),}
\NormalTok{                (}\StringTok{"label"}\NormalTok{, }\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"found"}\NormalTok{))}
\NormalTok{              ]}
\NormalTok{        )}
        \StringTok{"value"}
\NormalTok{    )}
\NormalTok{    (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{))}

\OtherTok{sumExample ::} \DataTypeTok{Expr}
\NormalTok{sumExample }\OtherTok{=}
  \DataTypeTok{ECase}
\NormalTok{    (}\DataTypeTok{EChoice} \StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{)))}
\NormalTok{    ( M.fromList}
\NormalTok{        [ (}\StringTok{"Found"}\NormalTok{, (}\StringTok{"value"}\NormalTok{, }\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \StringTok{"value"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))),}
\NormalTok{          (}\StringTok{"Missing"}\NormalTok{, (}\StringTok{"message"}\NormalTok{, }\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{0}\NormalTok{)))}
\NormalTok{        ]}
\NormalTok{    )}
\end{Highlighting}
\end{Shaded}

Now, for the entire point of \texttt{Expr}, we can write a function to
pretty-print it, using the
\emph{\href{https://hackage.haskell.org/package/prettyprinter}{prettyprinter}}
library:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L253{-}L299}

\OtherTok{ppPrim ::} \DataTypeTok{Prim} \OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppPrim }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{PInt}\NormalTok{ n }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty n}
  \DataTypeTok{PBool} \DataTypeTok{True} \OtherTok{{-}\textgreater{}} \StringTok{"true"}
  \DataTypeTok{PBool} \DataTypeTok{False} \OtherTok{{-}\textgreater{}} \StringTok{"false"}
  \DataTypeTok{PString}\NormalTok{ s }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty (}\FunctionTok{show}\NormalTok{ s)}

\OtherTok{ppOp ::} \DataTypeTok{Op} \OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppOp }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \StringTok{"+"}
  \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \StringTok{"*"}
  \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \StringTok{"\textless{}="}
  \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \StringTok{"\&\&"}

\OtherTok{ppExpr ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppExpr paren }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ p }\OtherTok{{-}\textgreater{}}\NormalTok{ ppPrim p}
  \DataTypeTok{EVar}\NormalTok{ v }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty v}
  \DataTypeTok{ELambda}\NormalTok{ n body }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$} \StringTok{"\textbackslash{}\textbackslash{}"} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty n }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ f }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppOp o }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ y}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}
\NormalTok{    PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{", "} \OperatorTok{$}
\NormalTok{      [PP.pretty k }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"="} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ v }\OperatorTok{|}\NormalTok{ (k, v) }\OtherTok{\textless{}{-}}\NormalTok{ M.toList xs]}
  \DataTypeTok{EAccess}\NormalTok{ e k }\OtherTok{{-}\textgreater{}}
\NormalTok{    ppExpr }\DataTypeTok{True}\NormalTok{ e }\OperatorTok{\textless{}\textgreater{}} \StringTok{"."} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty k}
  \DataTypeTok{EChoice}\NormalTok{ tag x }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ PP.pretty tag }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}
\NormalTok{      PP.sep}
\NormalTok{        [ }\StringTok{"case"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"of"}
\NormalTok{        , PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{"; "} \OperatorTok{$}
\NormalTok{            [ PP.pretty tag }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ PP.pretty n }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ body}
            \OperatorTok{|}\NormalTok{ (tag, (n, body)) }\OtherTok{\textless{}{-}}\NormalTok{ M.toList hs}
\NormalTok{            ]}
\NormalTok{        ]}
  \KeywordTok{where}
\NormalTok{    wrap}
      \OperatorTok{|}\NormalTok{ paren }\OtherTok{=}\NormalTok{ PP.parens}
      \OperatorTok{|} \FunctionTok{otherwise} \OtherTok{=} \FunctionTok{id}

\OtherTok{prettyExpr ::} \DataTypeTok{Expr} \OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{prettyExpr }\OtherTok{=}\NormalTok{ ppExpr }\DataTypeTok{False}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr fifteen}
\NormalTok{(\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ x }\OperatorTok{*} \DecValTok{3}\NormalTok{) }\DecValTok{5}
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr badTypeExample}
\DecValTok{1} \OperatorTok{\&\&} \DecValTok{2}
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr recordExample}
\NormalTok{\{ label }\OtherTok{=} \StringTok{"found"}\NormalTok{, value }\OtherTok{=} \DecValTok{7}\NormalTok{ \}}\OperatorTok{.}\NormalTok{value }\OperatorTok{+} \DecValTok{1}
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr sumExample}
\KeywordTok{case} \DataTypeTok{Found} \DecValTok{7} \KeywordTok{of}\NormalTok{ \{ }\DataTypeTok{Found}\NormalTok{ value }\OtherTok{{-}\textgreater{}}\NormalTok{ value }\OperatorTok{+} \DecValTok{1}\NormalTok{; }\DataTypeTok{Missing}\NormalTok{ message }\OtherTok{{-}\textgreater{}} \DecValTok{0}\NormalTok{ \}}
\end{Highlighting}
\end{Shaded}

Now, we can write a quick typechecker for this using a greedy type-checking
algorithm
(\href{https://github.com/mstksg/inCode/tree/master/code-samples/typed-sm-lc/ExprStage1.hs\#L77-L89}{written
out here}), which is a fun exercise, but it's beyond the point of this post. For
our purposes, we're going to write the in-Haskell evaluator, which is one
sure-fire evidential/constructive way to prove an expression was valid
after-the-fact.

So\ldots how can you ``evaluate'' this to 15, within Haskell? What would the
type even be? The best we can do at this point is make the entire thing monadic
by returning \texttt{Maybe} or \texttt{Either}, and split out the expressions we
write from the values we can actually evaluate to:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L228{-}L330}

\KeywordTok{data} \DataTypeTok{EValue}
  \OtherTok{=} \DataTypeTok{EVInt} \DataTypeTok{Int}
  \OperatorTok{|} \DataTypeTok{EVBool} \DataTypeTok{Bool}
  \OperatorTok{|} \DataTypeTok{EVString} \DataTypeTok{String}
  \OperatorTok{|} \DataTypeTok{EVFun}\NormalTok{ (}\DataTypeTok{EValue} \OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe} \DataTypeTok{EValue}\NormalTok{)}
  \OperatorTok{|} \DataTypeTok{EVRecord}\NormalTok{ (}\DataTypeTok{Map} \DataTypeTok{String} \DataTypeTok{EValue}\NormalTok{)}
  \OperatorTok{|} \DataTypeTok{EVChoice} \DataTypeTok{String} \DataTypeTok{EValue}

\OtherTok{eval ::} \DataTypeTok{Map} \DataTypeTok{String} \DataTypeTok{EValue} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe} \DataTypeTok{EValue}
\NormalTok{eval env }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ p }\OtherTok{{-}\textgreater{}}\NormalTok{ evalPrim p}
  \DataTypeTok{EVar}\NormalTok{ v }\OtherTok{{-}\textgreater{}}\NormalTok{ M.lookup v env}
  \DataTypeTok{ELambda}\NormalTok{ n body }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVFun}\NormalTok{ (\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (M.insert n x env) body))}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}\NormalTok{ eval env f }\OperatorTok{\textgreater{}\textgreater{}=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{EVFun}\NormalTok{ f\textquotesingle{} }\OtherTok{{-}\textgreater{}}\NormalTok{ eval env x }\OperatorTok{\textgreater{}\textgreater{}=}\NormalTok{ f\textquotesingle{}}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
\NormalTok{    u }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
\NormalTok{    v }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
    \KeywordTok{case}\NormalTok{ (u, v) }\KeywordTok{of}
\NormalTok{      (}\DataTypeTok{EVInt}\NormalTok{ a, }\DataTypeTok{EVInt}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ o }\KeywordTok{of}
        \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{+}\NormalTok{ b))}
        \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{*}\NormalTok{ b))}
        \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\textless{}=}\NormalTok{ b))}
        \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
\NormalTok{      (}\DataTypeTok{EVBool}\NormalTok{ a, }\DataTypeTok{EVBool}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ o }\KeywordTok{of}
        \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\&\&}\NormalTok{ b))}
\NormalTok{        \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
\NormalTok{      \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVRecord} \OperatorTok{\textless{}$\textgreater{}} \FunctionTok{traverse}\NormalTok{ (eval env) xs}
  \DataTypeTok{EAccess}\NormalTok{ e k }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVRecord}\NormalTok{ xs }\OtherTok{\textless{}{-}}\NormalTok{ eval env e}
\NormalTok{    M.lookup k xs}
  \DataTypeTok{EChoice}\NormalTok{ tag x }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVChoice}\NormalTok{ tag }\OperatorTok{\textless{}$\textgreater{}}\NormalTok{ eval env x}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVChoice}\NormalTok{ tag payload }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
\NormalTok{    (n, body) }\OtherTok{\textless{}{-}}\NormalTok{ M.lookup tag hs}
\NormalTok{    eval (M.insert n payload env) body}
\end{Highlighting}
\end{Shaded}

This would properly evaluate:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ eval M.empty fifteen}
\DataTypeTok{Just}\NormalTok{ (}\DataTypeTok{EVInt} \DecValTok{15}\NormalTok{)}
\end{Highlighting}
\end{Shaded}

We can also produce closures as values:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage1.hs\#L64{-}L65}

\OtherTok{plusThree ::} \DataTypeTok{Expr}
\NormalTok{plusThree }\OtherTok{=} \DataTypeTok{ELambda} \StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{)))}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ for\_ (eval M.empty plusThree) \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{EVFun}\NormalTok{ f }\OtherTok{{-}\textgreater{}} \FunctionTok{print}\NormalTok{ (f (}\DataTypeTok{EVInt} \DecValTok{4}\NormalTok{))}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \FunctionTok{putStrLn} \StringTok{"not a function"}
\DataTypeTok{Just}\NormalTok{ (}\DataTypeTok{EVInt} \DecValTok{7}\NormalTok{)}
\end{Highlighting}
\end{Shaded}

This kind of works if you remember to thread everything through \texttt{Maybe}
(or \texttt{Either}) or what have you. But this is not ideal. You should be able
to know, at compile-time, that your \texttt{Expr} is valid. After all, you want
to be able to create one ``valid'' \texttt{Expr}, and run it at every context.
It's useless to you if every single time you used an \texttt{Expr}, you had to
manually handle the \texttt{Nothing} case. Your diagram generator, your Haskell
runner, your code generator, will always be in \texttt{Either} even though you
know your \texttt{Expr} is valid, via tests or something. We want GHC to reject
badly typed expressions, so we never need to unwrap or handle a \texttt{Nothing}
or \texttt{Left}!

No, no, this is not okay and not acceptable. We should be able to verify in the
types if an \texttt{Expr} is valid.

\section{Type-Indexed Expressions}\label{type-indexed-expressions}

\subsection{Just Add the Index}\label{just-add-the-index}

The next step you'll see in posts online is to add a phantom index type to
\texttt{Expr}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L19{-}L49}

\KeywordTok{type} \KeywordTok{data} \DataTypeTok{Ty}
  \OtherTok{=} \DataTypeTok{TInt}
  \OperatorTok{|} \DataTypeTok{TBool}
  \OperatorTok{|} \DataTypeTok{TString}
  \OperatorTok{|} \DataTypeTok{Ty} \OperatorTok{:{-}\textgreater{}} \DataTypeTok{Ty}

\KeywordTok{data} \DataTypeTok{Prim}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{PInt}\OtherTok{ ::} \DataTypeTok{Int} \OtherTok{{-}\textgreater{}} \DataTypeTok{Prim} \DataTypeTok{TInt}
  \DataTypeTok{PBool}\OtherTok{ ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Prim} \DataTypeTok{TBool}
  \DataTypeTok{PString}\OtherTok{ ::} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{Prim} \DataTypeTok{TString}

\KeywordTok{data} \DataTypeTok{Op}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{OPlus}\OtherTok{ ::} \DataTypeTok{Op} \DataTypeTok{TInt} \DataTypeTok{TInt} \DataTypeTok{TInt}
  \DataTypeTok{OTimes}\OtherTok{ ::} \DataTypeTok{Op} \DataTypeTok{TInt} \DataTypeTok{TInt} \DataTypeTok{TInt}
  \DataTypeTok{OLte}\OtherTok{ ::} \DataTypeTok{Op} \DataTypeTok{TInt} \DataTypeTok{TInt} \DataTypeTok{TBool}
  \DataTypeTok{OAnd}\OtherTok{ ::} \DataTypeTok{Op} \DataTypeTok{TBool} \DataTypeTok{TBool} \DataTypeTok{TBool}

\KeywordTok{data} \DataTypeTok{Expr}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EPrim}\OtherTok{ ::} \DataTypeTok{Prim}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t}
  \DataTypeTok{EVar}\OtherTok{ ::} \DataTypeTok{STy}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t}
  \DataTypeTok{ELambda}\OtherTok{ ::} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
  \DataTypeTok{EApply}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b}
  \DataTypeTok{EOp}\OtherTok{ ::} \DataTypeTok{Op}\NormalTok{ a b c }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ c}
\end{Highlighting}
\end{Shaded}

(We'll explain each part of this declaration eventually)

A phantom type is a type parameter that doesn't represent any actual
\emph{value} ``contained'' inside the data type, but just serves to ``tag'' or
distinguish values for the compiler to reject or unify things in useful ways.

This introduces several new language features, so bear with me as I break them
down.

First, we use \texttt{-XTypeData} to define a data kind: \texttt{Ty} is a kind
with types \texttt{TInt\ ::\ Ty}, \texttt{TBool\ ::\ Ty}, etc. And in
\texttt{Expr\ t}, we have an expression tagged with \texttt{t}, which describes
the result type. (In fact, \emph{all} data types are automatically promoted to
the type level with \texttt{-XDataKinds}. You might see the
\texttt{\textquotesingle{}Nothing} quote prefix syntax in cases where it's
ambiguous if you're talking about the data constructor or the type constructor,
like \texttt{\textquotesingle{}{[}{]}} and \texttt{\textquotesingle{}(,)})

For example, because we have
\texttt{EPrim\ ::\ Prim\ t\ -\textgreater{}\ Expr\ t}, and
\texttt{PInt\ 3\ ::\ Prim\ TInt}, we have
\texttt{EPrim\ (PInt\ 3)\ ::\ Expr\ TInt}: a primitive 3 is an expression
describing an integer.

And because
\texttt{EOp\ ::\ Op\ a\ b\ c\ -\textgreater{}\ Expr\ a\ -\textgreater{}\ Expr\ b\ -\textgreater{}\ Expr\ c},
and \texttt{OLte\ ::\ Op\ TInt\ TInt\ TBool}, we have

\begin{Shaded}
\begin{Highlighting}[]
\DataTypeTok{EOp} \DataTypeTok{OLte}\OtherTok{ ::} \DataTypeTok{Expr} \DataTypeTok{TInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \DataTypeTok{TInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \DataTypeTok{TBool}
\end{Highlighting}
\end{Shaded}

So we can write an operation on two \texttt{Expr}s that typecheck how we'd
expect:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{EOp} \DataTypeTok{OLte}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{)) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{4}\NormalTok{))}
\DataTypeTok{Expr} \DataTypeTok{TBool}
\end{Highlighting}
\end{Shaded}

We also have
\texttt{EOp\ OAnd\ ::\ Expr\ TBool\ -\textgreater{}\ Expr\ TBool\ -\textgreater{}\ Expr\ TBool},
which means the compiler will reject our previous \texttt{1\ \&\&\ 2} example:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{EOp} \DataTypeTok{OAnd}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{2}\NormalTok{))}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{Couldn\textquotesingle{}t}\NormalTok{ match }\KeywordTok{type}\NormalTok{ ‘}\DataTypeTok{TInt}\NormalTok{’ with ‘}\DataTypeTok{TBool}\NormalTok{’}
      \DataTypeTok{Expected}\OperatorTok{:} \DataTypeTok{Prim} \DataTypeTok{TBool}
        \DataTypeTok{Actual}\OperatorTok{:} \DataTypeTok{Prim} \DataTypeTok{TInt}
\end{Highlighting}
\end{Shaded}

We can write lambdas in this system too:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L51{-}L55}

\OtherTok{fifteen ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{fifteen }\OtherTok{=}
  \DataTypeTok{EApply}
\NormalTok{    (}\DataTypeTok{ELambda} \DataTypeTok{STInt} \StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OTimes}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{))))}
\NormalTok{    (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{5}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

Because of \texttt{Ty}, we can also make a new indexed data type with phantoms
of ``fully resolved'' values:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L115{-}L119}

\KeywordTok{data} \DataTypeTok{EValue}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EVInt}\OtherTok{ ::} \DataTypeTok{Int} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TInt}
  \DataTypeTok{EVBool}\OtherTok{ ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TBool}
  \DataTypeTok{EVString}\OtherTok{ ::} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TString}
  \DataTypeTok{EVFun}\OtherTok{ ::}\NormalTok{ (}\DataTypeTok{EValue}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (}\DataTypeTok{EValue}\NormalTok{ b)) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
\end{Highlighting}
\end{Shaded}

This is what we want to eventually \texttt{eval} into, as we can guarantee
ourselves to get a value of the correct type based on the \texttt{Ty}:

\begin{Shaded}
\begin{Highlighting}[]
\OtherTok{eValueToInt ::} \DataTypeTok{EValue} \DataTypeTok{TInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Int}
\NormalTok{eValueToInt }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{EVInt}\NormalTok{ x }\OtherTok{{-}\textgreater{}}\NormalTok{ x}
\end{Highlighting}
\end{Shaded}

And GHC will verify this as a total pattern match because \texttt{EVInt} is the
only possible way to create an \texttt{EValue\ TInt}.

\subsection{Singletons and Existentials}\label{singletons-and-existentials}

We'll keep our bound variables stored as an ambient map of variable names to
their evaluated values for now. But, to do this, we need to turn the
heterogeneous \texttt{EValue\ t} into the homogeneous
\texttt{Map\ String\ SomeValue} by wrapping the type variable as an existential
type.

You might notice we have a
\href{https://blog.jle.im/entries/series/+introduction-to-singletons.html}{singleton}
for our \texttt{Ty} type, \texttt{STy}, that pops up in multiple situations.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L27{-}L31}

\KeywordTok{data} \DataTypeTok{STy}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{STInt}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TInt}
  \DataTypeTok{STBool}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TBool}
  \DataTypeTok{STString}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TString}
  \DataTypeTok{STFun}\OtherTok{ ::} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
\end{Highlighting}
\end{Shaded}

Firstly, it might help to recognize the general pattern where \texttt{STy} (the
singleton) appears. It \emph{usually} pops up whenever we have existentially
scoped variables, like in
\texttt{data\ SomeValue\ =\ forall\ t.\ SomeValue\ (STy\ t)\ (EValue\ t)}. In
this case, the \texttt{t} is completely lost to the outside world, and
\texttt{STy\ t} is used to allow us to recover a runtime witness to what
\texttt{t} was, after pattern matching on \texttt{STy}. This is the
\emph{dependent sum} pattern, and is similar to how \texttt{Typeable} is used in
\emph{Data.Dynamic}.

In our case, because variables are still stored ambiently in the environment and
validated at runtime, we \emph{do} need singletons to implement \texttt{eval} .
The type \texttt{Expr\ t} only specifies the type of the result, but the type
information of the ambient variables is not available. So, you can write
\texttt{EVar\ STInt\ "myVar"\ ::\ Expr\ TInt}, but:

\begin{itemize}
\tightlist
\item
  \texttt{myVar} might not be a variable in scope at all, so \texttt{eval} will
  fail at runtime
\item
  \texttt{myVar} might be in scope, but might be a \texttt{TString} and not a
  \texttt{TInt}
\end{itemize}

The first case is easy enough to deal with (\texttt{M.lookup} returns
\texttt{Nothing}), but the second one is a little more subtle. Let's say we
\emph{do} have a \texttt{SomeValue} under our key \texttt{myVar}\ldots how do we
make sure it has the correct type?

\subsection{Runtime Type Equality}\label{runtime-type-equality}

We can do ad-hoc pattern matching on \texttt{EValue}, but that won't get us too
far. Mostly because some of the \texttt{EValue} constructors actually don't have
enough information for us to validate their actual type (try it! \texttt{EVFun}
will give you a lot of trouble). So, what we can do is write a function that
takes two \texttt{STy} at runtime and \emph{unifies} them conditionally if they
are the same. We'll write a function
\texttt{sameTy\ ::\ STy\ a\ -\textgreater{}\ STy\ b\ -\textgreater{}\ Maybe\ (a\ :\textasciitilde{}:\ b)},
where

\begin{Shaded}
\begin{Highlighting}[]
\KeywordTok{data}\OtherTok{ (:\textasciitilde{}:) ::}\NormalTok{ k }\OtherTok{{-}\textgreater{}}\NormalTok{ k }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
    \DataTypeTok{Refl}\OtherTok{ ::}\NormalTok{ a }\OperatorTok{:\textasciitilde{}:}\NormalTok{ a}
\end{Highlighting}
\end{Shaded}

\emph{pattern matching} on a value of type \texttt{a\ :\textasciitilde{}:\ b}
will reveal that \texttt{a} and \texttt{b} are the same type variable, because
the only way to construct it is with
\texttt{Refl\ ::\ a\ :\textasciitilde{}:\ a}.

With that, we can write \texttt{sameTy}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L133{-}L143}

\OtherTok{sameTy ::} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (a }\OperatorTok{:\textasciitilde{}:}\NormalTok{ b)}
\NormalTok{sameTy }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{STInt} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STBool} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STBool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STString} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STString} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STFun}\NormalTok{ a b }\OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{STFun}\NormalTok{ c d }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy a c}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy b d}
      \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
\end{Highlighting}
\end{Shaded}

There's a typeclass in \emph{base} (or rather, a ``kindclass''),
\texttt{TestEquality}, that encapsulates this pattern:

\begin{Shaded}
\begin{Highlighting}[]
\KeywordTok{class} \DataTypeTok{TestEquality}\NormalTok{ f }\KeywordTok{where}
\OtherTok{    testEquality ::}\NormalTok{ f a }\OtherTok{{-}\textgreater{}}\NormalTok{ f b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (a }\OperatorTok{:\textasciitilde{}:}\NormalTok{ b)}
\end{Highlighting}
\end{Shaded}

In fact, we can write our \texttt{sameTy} as an instance:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L130{-}L131}

\KeywordTok{instance} \DataTypeTok{TestEquality} \DataTypeTok{STy} \KeywordTok{where}
\NormalTok{  testEquality }\OtherTok{=}\NormalTok{ sameTy}
\end{Highlighting}
\end{Shaded}

We're now at a higher fanciness level than before. But you might see the problem
here: \texttt{EVar\ STInt\ "x"}. \texttt{x} might not be defined, and it also
might not have the correct type. Soooo yes, we still have issues here.

But now at least we can write \texttt{eval}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L145{-}L176}

\OtherTok{eval ::} \DataTypeTok{Map} \DataTypeTok{String} \DataTypeTok{SomeValue} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (}\DataTypeTok{EValue}\NormalTok{ t)}
\NormalTok{eval env }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt}\NormalTok{ n) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ n)}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PBool}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ b)}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString}\NormalTok{ s) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVString}\NormalTok{ s)}
  \DataTypeTok{EVar}\NormalTok{ t v }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{SomeValue}\NormalTok{ t\textquotesingle{} v\textquotesingle{} }\OtherTok{\textless{}{-}}\NormalTok{ M.lookup v env}
    \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy t t\textquotesingle{}}
    \FunctionTok{pure}\NormalTok{ v\textquotesingle{}}
  \DataTypeTok{ELambda}\NormalTok{ ta n body }\OtherTok{{-}\textgreater{}}
    \FunctionTok{pure} \OperatorTok{$} \DataTypeTok{EVFun} \OperatorTok{$}\NormalTok{ \textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (M.insert n (}\DataTypeTok{SomeValue}\NormalTok{ ta x) env) body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVFun}\NormalTok{ g }\OtherTok{\textless{}{-}}\NormalTok{ eval env f}
\NormalTok{    x\textquotesingle{} }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
\NormalTok{    g x\textquotesingle{}}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ o }\KeywordTok{of}
    \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{+}\NormalTok{ b))}
    \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{*}\NormalTok{ b))}
    \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\textless{}=}\NormalTok{ b))}
    \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVBool}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVBool}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\&\&}\NormalTok{ b))}
\end{Highlighting}
\end{Shaded}

This does seem to work:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ for\_ (eval M.empty fifteen) \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{EVInt}\NormalTok{ x }\OtherTok{{-}\textgreater{}} \FunctionTok{print}\NormalTok{ x}
\DecValTok{15}
\end{Highlighting}
\end{Shaded}

Our system also allows us to produce closures and functions as values:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L63{-}L64}

\OtherTok{plusThree ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TInt} \OperatorTok{:{-}\textgreater{}} \DataTypeTok{TInt}\NormalTok{)}
\NormalTok{plusThree }\OtherTok{=} \DataTypeTok{ELambda} \DataTypeTok{STInt} \StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{)))}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ for\_ (eval M.empty plusThree) \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{EVFun}\NormalTok{ f }\OtherTok{{-}\textgreater{}}\NormalTok{ for\_ (f (}\DataTypeTok{EVInt} \DecValTok{4}\NormalTok{)) \textbackslash{}}\KeywordTok{case}
      \DataTypeTok{EVInt}\NormalTok{ x }\OtherTok{{-}\textgreater{}} \FunctionTok{print}\NormalTok{ x    }\CommentTok{{-}{-} compiler{-}verified to always be EVInt}
\DecValTok{7}
\end{Highlighting}
\end{Shaded}

We have a type-safe \texttt{eval} now that will create a value of the type we
want. But we still have the same errors when looking at variables: variables can
still not be defined, or be defined as the wrong type.

\subsection{Pretty-Printing}\label{pretty-printing}

One nice consequence of this type-index method is that if you choose to consume
them into an untyped target, you can do it more or less in the same way as the
non-indexed untyped data.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L87{-}L113}

\OtherTok{ppPrim ::} \DataTypeTok{Prim}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppPrim }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{PInt}\NormalTok{ n }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty n}
  \DataTypeTok{PBool}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \KeywordTok{if}\NormalTok{ b }\KeywordTok{then} \StringTok{"true"} \KeywordTok{else} \StringTok{"false"}
  \DataTypeTok{PString}\NormalTok{ s }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty (}\FunctionTok{show}\NormalTok{ s)}

\OtherTok{ppOp ::} \DataTypeTok{Op}\NormalTok{ a b c }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppOp }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \StringTok{"+"}
  \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \StringTok{"*"}
  \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \StringTok{"\textless{}="}
  \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \StringTok{"\&\&"}

\OtherTok{ppExpr ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppExpr paren }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ p }\OtherTok{{-}\textgreater{}}\NormalTok{ ppPrim p}
  \DataTypeTok{EVar}\NormalTok{ \_ v }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty v}
  \DataTypeTok{ELambda}\NormalTok{ \_ n body }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$} \StringTok{"\textbackslash{}\textbackslash{}"} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty n }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ f }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppOp o }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ y}
  \KeywordTok{where}
\NormalTok{    wrap}
      \OperatorTok{|}\NormalTok{ paren }\OtherTok{=}\NormalTok{ PP.parens}
      \OperatorTok{|} \FunctionTok{otherwise} \OtherTok{=} \FunctionTok{id}

\OtherTok{prettyExpr ::} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{prettyExpr }\OtherTok{=}\NormalTok{ ppExpr }\DataTypeTok{False}
\end{Highlighting}
\end{Shaded}

And they render the same way:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr fifteen}
\NormalTok{(\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ x }\OperatorTok{*} \DecValTok{3}\NormalTok{) }\DecValTok{5}
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr plusThree}
\NormalTok{\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ x }\OperatorTok{+} \DecValTok{3}
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr badVariable}
\NormalTok{(\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ x }\OperatorTok{+} \DecValTok{3}\NormalTok{) true}
\end{Highlighting}
\end{Shaded}

\subsection{Still Not Fully Verified}\label{still-not-fully-verified}

Implicit in the previous section was the admission of failure: this system lets
us use indexed types to help propagate unification (the result types of
\texttt{OLte}, \texttt{OAnd}, \texttt{OPlus}, etc.), but it can't prevent all
ill-defined programs from compiling.

The issue is \texttt{EVar}: its type
\texttt{EVar\ ::\ STy\ t\ -\textgreater{}\ String\ -\textgreater{}\ Expr\ t}
lets us bind \emph{any} variable name as \emph{any} type, and it'll still
typecheck. Even with the help of everything we have, we can just straight-up
declare a reference to an unbound variable

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L71{-}L72}

\OtherTok{unboundVariable ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{unboundVariable }\OtherTok{=} \DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"missing"}
\end{Highlighting}
\end{Shaded}

This typechecks in GHC even though it's meaningless in the domain. We can also
reference the variable under any \emph{type}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage2.hs\#L57{-}L61}

\OtherTok{badVariable ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{badVariable }\OtherTok{=}
  \DataTypeTok{EApply}
\NormalTok{    (}\DataTypeTok{ELambda} \DataTypeTok{STBool} \StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{))))}
\NormalTok{    (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PBool} \DataTypeTok{True}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

That's because \texttt{EVar} can freely take any \texttt{STy} without any
restriction, and no association with the binder name, so there's no way for GHC
to stop us.

So, again, we cannot create a \emph{fully} type-checked \texttt{Expr}. We still
have to deal with \emph{most} of the same errors. This is noble, but clearly not
good enough. We have to go deeper.

\section{Typed Records and Sums}\label{typed-records-and-sums}

A quick detour: you might have noticed that this past implementation dropped
records and sums. Before we move on, let's go ahead and add those. Introducing
records and sums at the same time as type-indexed \texttt{Expr} is a bit
\emph{too} much of a jump to fit into a single section.

Let's add sums and records, which can use pretty similar mechanisms (via
duality) for implementation.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L31{-}L79}

\KeywordTok{type} \KeywordTok{data} \DataTypeTok{Ty}
  \OtherTok{=} \DataTypeTok{TInt}
  \OperatorTok{|} \DataTypeTok{TBool}
  \OperatorTok{|} \DataTypeTok{TString}
  \OperatorTok{|} \DataTypeTok{TRecord}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)]}
  \OperatorTok{|} \DataTypeTok{TSum}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)]}
  \OperatorTok{|} \DataTypeTok{Ty} \OperatorTok{:{-}\textgreater{}} \DataTypeTok{Ty}

\KeywordTok{data} \DataTypeTok{STy}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{STInt}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TInt}
  \DataTypeTok{STBool}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TBool}
  \DataTypeTok{STString}\OtherTok{ ::} \DataTypeTok{STy} \DataTypeTok{TString}
  \DataTypeTok{STRecord}\OtherTok{ ::} \DataTypeTok{Rec} \DataTypeTok{STyField}\NormalTok{ as }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ as)}
  \DataTypeTok{STSum}\OtherTok{ ::} \DataTypeTok{Rec} \DataTypeTok{STyField}\NormalTok{ as }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ as)}
  \DataTypeTok{STFun}\OtherTok{ ::} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
\end{Highlighting}
\end{Shaded}

\texttt{Ty} now includes \texttt{TRecord\ {[}(Symbol,\ Ty){]}} and
\texttt{TSum\ {[}(Symbol,\ Ty){]}}, which represent the field names and
constructor payloads (\texttt{Symbol} being a type-level string). So, for
example, \texttt{TRecord\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]}}
would be the type of a record with ordered fields \texttt{value} and
\texttt{label} of integers and strings, respectively.
\texttt{TSum\ {[}"Found"\ :::\ TInt,\ "Missing"\ :::\ TString{]}} would be the
type of a sum between \texttt{Found} containing an integer and \texttt{Missing}
containing a string. Note we take a page out of
\href{https://hackage.haskell.org/package/vinyl}{vinyl} by defining the type
alias \texttt{(:::)\ =\ \textquotesingle{}(,)} to make things syntactically
nicer.

\subsection{Record Access}\label{record-access}

We need the fields and types at the type level because we have to answer what
the \texttt{Expr} phantom type of field access is. If we had an
\texttt{x\ ::\ Expr\ (TRecord\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]})},
we want the type of \texttt{x.value} to be \texttt{Expr\ TInt}.

To do this, we need to have a \emph{value} in our \texttt{Expr} for field access
that can ``point'' at a specific field in the type. One way to do that is to
take a field of type \texttt{Index}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L47{-}L49}

\KeywordTok{data} \DataTypeTok{Index}\OtherTok{ ::}\NormalTok{ [k] }\OtherTok{{-}\textgreater{}}\NormalTok{ k }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{IZ}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ (x }\OperatorTok{:}\NormalTok{ xs) x}
  \DataTypeTok{IS}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ xs x }\OtherTok{{-}\textgreater{}} \DataTypeTok{Index}\NormalTok{ (y }\OperatorTok{:}\NormalTok{ xs) x}
\end{Highlighting}
\end{Shaded}

You can read this as: ``\texttt{IZ} is an index to the head of the type-level
list, and \texttt{IS\ n} is an index to the n-th item of the tail''. So,
\texttt{IS\ IZ} is an index into the second element, \texttt{IS\ (IS\ IZ)} is an
index into the third, etc.

If we have \texttt{{[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]}}, then we
have values:

\begin{Shaded}
\begin{Highlighting}[]
\DataTypeTok{IZ}\OtherTok{    ::} \DataTypeTok{Index}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] (}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{)}
\DataTypeTok{IS} \DataTypeTok{IZ}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] (}\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{)}
\end{Highlighting}
\end{Shaded}

Note that the way this is constructed, it's impossible for
\texttt{IS\ (IS\ IZ)\ ::\ Index\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]}\ \_}
to typecheck as anything!

In this way, we have a well-typed field accessor syntax, which takes an
\texttt{Expr} of a record of fields and indexes it to get an \texttt{Expr} of
the type at that index:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L105{-}L105}

  \DataTypeTok{EAccess}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ as) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Index}\NormalTok{ as (l }\OperatorTok{:::}\NormalTok{ a) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a}
\end{Highlighting}
\end{Shaded}

Which is typed as:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(}\OtherTok{\textasciigrave{}EAccess\textasciigrave{}} \DataTypeTok{IZ}\NormalTok{)}\OtherTok{    ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{(}\OtherTok{\textasciigrave{}EAccess\textasciigrave{}} \DataTypeTok{IS} \DataTypeTok{IZ}\NormalTok{)}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr} \DataTypeTok{TString}
\end{Highlighting}
\end{Shaded}

To \emph{create} an \texttt{Expr} of a record, we can use \texttt{Rec} from
\emph{\href{https://hackage.haskell.org/package/vinyl}{vinyl}} or \texttt{NP}
from \emph{\href{https://hackage.haskell.org/package/sop-core}{sop-core}}: a
heterogeneous list indexed by a type-level list.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L43{-}L45}

\KeywordTok{data} \DataTypeTok{Rec}\OtherTok{ ::}\NormalTok{ (k }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type}\NormalTok{) }\OtherTok{{-}\textgreater{}}\NormalTok{ [k] }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{RNil}\OtherTok{ ::} \DataTypeTok{Rec}\NormalTok{ f \textquotesingle{}[]}
\OtherTok{  (:\&) ::}\NormalTok{ f x }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ f xs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ f (x }\OperatorTok{:}\NormalTok{ xs)}
\end{Highlighting}
\end{Shaded}

If you haven't seen \texttt{Rec} before, basically \texttt{Rec\ f\ {[}a,b,c{]}}
is a tuple of \texttt{f\ a}, \texttt{f\ b}, and \texttt{f\ c}. For example:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{Identity} \DecValTok{3} \OperatorTok{:\&} \DataTypeTok{Identity} \DataTypeTok{True} \OperatorTok{:\&} \DataTypeTok{Identity} \StringTok{"hello"} \OperatorTok{:\&} \DataTypeTok{RNil}
\DataTypeTok{Rec} \DataTypeTok{Identity}\NormalTok{ [}\DataTypeTok{Int}\NormalTok{, }\DataTypeTok{Bool}\NormalTok{, }\DataTypeTok{String}\NormalTok{]}
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{Const} \StringTok{"x"} \OperatorTok{:\&} \DataTypeTok{Const} \StringTok{"y"} \OperatorTok{:\&} \DataTypeTok{RNil}
\DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{Const} \DataTypeTok{String}\NormalTok{) [x1, x2]}
\end{Highlighting}
\end{Shaded}

Keeping \texttt{Rec\ f\ as} instead of a direct heterogeneous list of
\texttt{a}s lets us store more interesting things than just \texttt{Type}-kinded
things. For example, since our lists here are lists of \texttt{(Symbol,\ Ty)},
we can create a container to hold fields:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L109{-}L110}

\KeywordTok{data} \DataTypeTok{ExprField}\OtherTok{ ::}\NormalTok{ (}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EField}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{ExprField}\NormalTok{ (l }\OperatorTok{:::}\NormalTok{ a)}
\end{Highlighting}
\end{Shaded}

The field constructor keeps a \texttt{KnownSymbol\ l} constraint, so the
type-level label is still available later when we need to render it:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{EField} \OperatorTok{@}\StringTok{"value"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}
            \OperatorTok{:\&} \DataTypeTok{EField} \OperatorTok{@}\StringTok{"label"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"found"}\NormalTok{))}
            \OperatorTok{:\&} \DataTypeTok{RNil}
\DataTypeTok{Rec} \DataTypeTok{ExprField}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]}
\end{Highlighting}
\end{Shaded}

So, we can create
\texttt{Expr\ (TRecord\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]})} by
taking a \texttt{Rec}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L104{-}L104}

  \DataTypeTok{ERecord}\OtherTok{ ::} \DataTypeTok{Rec} \DataTypeTok{ExprField}\NormalTok{ as }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ as)}
\end{Highlighting}
\end{Shaded}

We can make this a little more ergonomic by using
\texttt{-XRequiredTypeArguments} (as of GHC 9.10) to get rid of the
\texttt{-XTypeApplication} ugliness:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L115{-}L150}

\OtherTok{eField ::} \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{ExprField}\NormalTok{ (l }\OperatorTok{:::}\NormalTok{ a)}
\NormalTok{eField l }\OtherTok{=} \DataTypeTok{EField} \OperatorTok{@}\NormalTok{l}

\OtherTok{makeRecordExample ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ [}\StringTok{"value"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"label"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{])}
\NormalTok{makeRecordExample }\OtherTok{=}
  \DataTypeTok{ERecord}
\NormalTok{    ( eField }\StringTok{"value"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}
        \OperatorTok{:\&}\NormalTok{ eField }\StringTok{"label"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"found"}\NormalTok{))}
        \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{    )}

\OtherTok{recordExample ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{recordExample }\OtherTok{=} \DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EAccess} \OperatorTok{@}\StringTok{"value"}\NormalTok{ makeRecordExample }\DataTypeTok{IZ}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

\subsection{Sum Injection and Case
Analysis}\label{sum-injection-and-case-analysis}

We also need a type-level list witness for \emph{sum} types, because we need to
be able to implement the correct continuations for pattern matches: How do we
know \emph{what} thing to handle in each pattern match, unless the sum type has
that information in its type?

Luckily due to the magic of duality, we can use the same tools, for the most
part! We can inject into a sum with an \texttt{Index}, let's say for a
\texttt{Expr\ (TSum\ {[}"Found"\ :::\ TInt,\ "Missing"\ :::\ TString{]})}: sum
type with \texttt{Found} containing an integer and \texttt{Missing} containing a
string:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L106{-}L106}

  \DataTypeTok{EChoice}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Index}\NormalTok{ as (l }\OperatorTok{:::}\NormalTok{ a) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ as)}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\DataTypeTok{EChoice} \OperatorTok{@}\StringTok{"Found"} \DataTypeTok{IZ}\OtherTok{        ::} \DataTypeTok{Expr} \DataTypeTok{TInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ [}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{])}
\DataTypeTok{EChoice} \OperatorTok{@}\StringTok{"Missing"}\NormalTok{ (}\DataTypeTok{IS} \DataTypeTok{IZ}\NormalTok{)}\OtherTok{ ::} \DataTypeTok{Expr} \DataTypeTok{TString} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ [}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{])}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L181{-}L182}

\OtherTok{makeSumExample ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ [}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{])}
\NormalTok{makeSumExample }\OtherTok{=} \DataTypeTok{EChoice} \OperatorTok{@}\StringTok{"Found"} \DataTypeTok{IZ}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

And we can re-use \texttt{Rec} to define a type that can \emph{handle} a
\texttt{{[}"Found"\ :::\ TInt,\ "Missing"\ :::\ TString{]}} sum:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L112{-}L133}

\KeywordTok{data} \DataTypeTok{ExprHandler}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}}\NormalTok{ (}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EHandler}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{ExprHandler}\NormalTok{ b (l }\OperatorTok{:::}\NormalTok{ a)}

\OtherTok{eHandler ::} \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{ExprHandler}\NormalTok{ b (l }\OperatorTok{:::}\NormalTok{ a)}
\NormalTok{eHandler l }\OtherTok{=} \DataTypeTok{EHandler} \OperatorTok{@}\NormalTok{l}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t eHandler }\StringTok{"Found"} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
\DataTypeTok{ExprHandler} \DataTypeTok{TInt}\NormalTok{ (}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{)}
         \CommentTok{{-}{-} \^{} result           \^{} payload}
\end{Highlighting}
\end{Shaded}

And we can put these into a \texttt{Rec} to handle each option in the list:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t eHandler }\StringTok{"Found"} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
           \OperatorTok{:\&}\NormalTok{ eHandler }\StringTok{"Missing"} \DataTypeTok{STString} \StringTok{"message"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{0}\NormalTok{))}
           \OperatorTok{:\&} \DataTypeTok{RNil}
\DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprHandler} \DataTypeTok{TInt}\NormalTok{) [}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]}
\end{Highlighting}
\end{Shaded}

And that's exactly what a case statement is:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L107{-}L107}

  \DataTypeTok{ECase}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ as) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprHandler}\NormalTok{ b) as }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ b}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L184{-}L191}

\OtherTok{sumExample ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{sumExample }\OtherTok{=}
  \DataTypeTok{ECase}
\NormalTok{    makeSumExample}
\NormalTok{    ( eHandler }\StringTok{"Found"} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
        \OperatorTok{:\&}\NormalTok{ eHandler }\StringTok{"Missing"} \DataTypeTok{STString} \StringTok{"message"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{0}\NormalTok{))}
        \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{    )}
\end{Highlighting}
\end{Shaded}

Note that we're still using string binders, so there's still an element of
unsafety here\ldots{} we say that the variable name is \texttt{"value"} and that
it is a \texttt{TInt}, but when we later refer to the variable with
\texttt{EVar\ STInt\ "value"}, it isn't type-checked that later references use
the same type. The compiler would be just as happy with
\texttt{EVar\ STString\ "value"}.

Here's an example demonstrating both failure modes: the first handler references
a variable that doesn't exist, and the second handler references a variable that
does exist as an incorrect type! How unfortunate.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L202{-}L209}

\OtherTok{badCaseBranchExample ::} \DataTypeTok{Expr} \DataTypeTok{TInt}
\NormalTok{badCaseBranchExample }\OtherTok{=}
  \DataTypeTok{ECase}
\NormalTok{    (}\DataTypeTok{EChoice} \OperatorTok{@}\StringTok{"Found"} \DataTypeTok{IZ}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{)))}
\NormalTok{    ( eHandler }\StringTok{"Found"} \DataTypeTok{STInt} \StringTok{"value"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"missing"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
        \OperatorTok{:\&}\NormalTok{ eHandler }\StringTok{"Missing"} \DataTypeTok{STString} \StringTok{"message"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{STInt} \StringTok{"message"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
        \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{    )}
\end{Highlighting}
\end{Shaded}

\subsection{Runtime Equality for Records and
Sums}\label{runtime-equality-for-records-and-sums}

One complication is that we need to update the \texttt{TestEquality} instance
for \texttt{STy}. The record and sum labels are type-level \texttt{Symbol}s, so
we compare those with the \texttt{sameSymbol} (kind of like
\texttt{testEquality} for any \texttt{KnownSymbol} instance) and then compare
the payload types recursively.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L284{-}L324}

\KeywordTok{instance} \DataTypeTok{TestEquality} \DataTypeTok{STy} \KeywordTok{where}
\NormalTok{    testEquality }\OtherTok{=}\NormalTok{ sameTy}

\KeywordTok{instance} \DataTypeTok{TestEquality} \DataTypeTok{STyField} \KeywordTok{where}
\NormalTok{    testEquality }\OtherTok{=}\NormalTok{ sameField}

\OtherTok{sameTy ::} \DataTypeTok{STy}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{STy}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (a }\OperatorTok{:\textasciitilde{}:}\NormalTok{ b)}
\NormalTok{sameTy }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{STInt} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STInt} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STBool} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STBool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STString} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case} \DataTypeTok{STString} \OtherTok{{-}\textgreater{}} \DataTypeTok{Just} \DataTypeTok{Refl}\NormalTok{; \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STRecord}\NormalTok{ as }\OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{STRecord}\NormalTok{ bs }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameFields as bs}
      \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STSum}\NormalTok{ as }\OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{STSum}\NormalTok{ bs }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameFields as bs}
      \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}
  \DataTypeTok{STFun}\NormalTok{ a b }\OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}}\KeywordTok{case}
    \DataTypeTok{STFun}\NormalTok{ c d }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy a c}
      \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy b d}
      \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{    \_ }\OtherTok{{-}\textgreater{}} \DataTypeTok{Nothing}

\OtherTok{sameFields ::} \DataTypeTok{Rec} \DataTypeTok{STyField}\NormalTok{ xs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec} \DataTypeTok{STyField}\NormalTok{ ys }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (xs }\OperatorTok{:\textasciitilde{}:}\NormalTok{ ys)}
\NormalTok{sameFields }\DataTypeTok{RNil} \DataTypeTok{RNil} \OtherTok{=} \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{sameFields (x }\OperatorTok{:\&}\NormalTok{ xs) (y }\OperatorTok{:\&}\NormalTok{ ys) }\OtherTok{=} \KeywordTok{do}
  \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameField x y}
  \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameFields xs ys}
  \DataTypeTok{Just} \DataTypeTok{Refl}
\NormalTok{sameFields \_ \_ }\OtherTok{=} \DataTypeTok{Nothing}

\OtherTok{sameField ::} \DataTypeTok{STyField}\NormalTok{ x }\OtherTok{{-}\textgreater{}} \DataTypeTok{STyField}\NormalTok{ y }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (x }\OperatorTok{:\textasciitilde{}:}\NormalTok{ y)}
\NormalTok{sameField (}\DataTypeTok{STyField} \OperatorTok{@}\NormalTok{l tx) (}\DataTypeTok{STyField} \OperatorTok{@}\NormalTok{m ty) }\OtherTok{=} \KeywordTok{do}
    \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameSymbol (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l) (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{m)}
    \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy tx ty}
    \DataTypeTok{Just} \DataTypeTok{Refl}
\end{Highlighting}
\end{Shaded}

\subsection{The Full Eval}\label{the-full-eval}

Before we write the final \texttt{eval}, let's practice using \texttt{Index} and
\texttt{Rec} together. If we have an index \texttt{Index\ as\ a} that picks out
a value \texttt{a} in \texttt{as}, then we can pick out the \texttt{f\ a} from a
\texttt{Rec\ f\ as}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L60{-}L63}

\OtherTok{indexRec ::} \DataTypeTok{Index}\NormalTok{ xs x }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ f xs }\OtherTok{{-}\textgreater{}}\NormalTok{ f x}
\NormalTok{indexRec }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{IZ} \OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}(x }\OperatorTok{:\&}\NormalTok{ \_) }\OtherTok{{-}\textgreater{}}\NormalTok{ x}
  \DataTypeTok{IS}\NormalTok{ i }\OtherTok{{-}\textgreater{}}\NormalTok{ \textbackslash{}(\_ }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{{-}\textgreater{}}\NormalTok{ indexRec i xs}
\end{Highlighting}
\end{Shaded}

We also can recursively iterate a function over each item, assuming the function
\texttt{forall\ x.\ f\ x\ -\textgreater{}\ g\ x}: that is, we can turn a
\texttt{Rec\ f\ as} into a \texttt{Rec\ g\ as} assuming our function is
polymorphic over each \texttt{x}, and only depends on the shape of \texttt{f}.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L65{-}L67}

\OtherTok{traverseRec ::} \DataTypeTok{Applicative}\NormalTok{ m }\OtherTok{=\textgreater{}}\NormalTok{ (}\KeywordTok{forall}\NormalTok{ x}\OperatorTok{.}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}\NormalTok{ m (g x)) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ f xs }\OtherTok{{-}\textgreater{}}\NormalTok{ m (}\DataTypeTok{Rec}\NormalTok{ g xs)}
\NormalTok{traverseRec \_ }\DataTypeTok{RNil} \OtherTok{=} \FunctionTok{pure} \DataTypeTok{RNil}
\NormalTok{traverseRec f (x }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{=}\NormalTok{ (}\OperatorTok{:\&}\NormalTok{) }\OperatorTok{\textless{}$\textgreater{}}\NormalTok{ f x }\OperatorTok{\textless{}*\textgreater{}}\NormalTok{ traverseRec f xs}
\end{Highlighting}
\end{Shaded}

With that, we can write our full \texttt{eval}.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L326{-}L369}

\OtherTok{eval ::} \DataTypeTok{Map} \DataTypeTok{String} \DataTypeTok{SomeValue} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{Maybe}\NormalTok{ (}\DataTypeTok{EValue}\NormalTok{ t)}
\NormalTok{eval env }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt}\NormalTok{ n) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ n)}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PBool}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ b)}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString}\NormalTok{ s) }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVString}\NormalTok{ s)}
  \DataTypeTok{EVar}\NormalTok{ t v }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{SomeValue}\NormalTok{ t\textquotesingle{} v\textquotesingle{} }\OtherTok{\textless{}{-}}\NormalTok{ M.lookup v env}
    \DataTypeTok{Refl} \OtherTok{\textless{}{-}}\NormalTok{ sameTy t t\textquotesingle{}}
    \FunctionTok{pure}\NormalTok{ v\textquotesingle{}}
  \DataTypeTok{ELambda}\NormalTok{ ta n body }\OtherTok{{-}\textgreater{}}
    \FunctionTok{pure} \OperatorTok{$} \DataTypeTok{EVFun} \OperatorTok{$}\NormalTok{ \textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (M.insert n (}\DataTypeTok{SomeValue}\NormalTok{ ta x) env) body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVFun}\NormalTok{ g }\OtherTok{\textless{}{-}}\NormalTok{ eval env f}
\NormalTok{    x\textquotesingle{} }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
\NormalTok{    g x\textquotesingle{}}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ o }\KeywordTok{of}
    \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{+}\NormalTok{ b))}
    \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{*}\NormalTok{ b))}
    \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVInt}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVInt}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\textless{}=}\NormalTok{ b))}
    \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \KeywordTok{do}
      \DataTypeTok{EVBool}\NormalTok{ a }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
      \DataTypeTok{EVBool}\NormalTok{ b }\OtherTok{\textless{}{-}}\NormalTok{ eval env y}
      \FunctionTok{pure}\NormalTok{ (}\DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\&\&}\NormalTok{ b))}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}
    \DataTypeTok{EVRecord} \OperatorTok{\textless{}$\textgreater{}}\NormalTok{ traverseRec (evalField env) xs}
  \DataTypeTok{EAccess}\NormalTok{ e i }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVRecord}\NormalTok{ xs }\OtherTok{\textless{}{-}}\NormalTok{ eval env e}
    \KeywordTok{case}\NormalTok{ indexRec i xs }\KeywordTok{of}
      \DataTypeTok{EVField}\NormalTok{ v }\OtherTok{{-}\textgreater{}} \FunctionTok{pure}\NormalTok{ v}
  \DataTypeTok{EChoice}\NormalTok{ i x }\OtherTok{{-}\textgreater{}}
    \DataTypeTok{EVSum}\NormalTok{ i }\OperatorTok{\textless{}$\textgreater{}}\NormalTok{ eval env x}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}} \KeywordTok{do}
    \DataTypeTok{EVSum}\NormalTok{ i v }\OtherTok{\textless{}{-}}\NormalTok{ eval env x}
    \KeywordTok{case}\NormalTok{ indexRec i hs }\KeywordTok{of}
      \DataTypeTok{EHandler}\NormalTok{ t n body }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (M.insert n (}\DataTypeTok{SomeValue}\NormalTok{ t v) env) body}
\end{Highlighting}
\end{Shaded}

\subsection{Ergonomics of Records and
Sums}\label{ergonomics-of-records-and-sums}

Note that we could also choose to implement records and sums using row types
indexed by the name of the field itself, instead of an ordered list of tuples.
This would have the advantage of making, for example,
\texttt{\{\ value\ ::\ Int,\ label\ ::\ String\ \}} the same type as
\texttt{\{\ label\ ::\ String,\ value\ ::\ Int\ \}}. However, I personally
prefer the style of building things inductively (\texttt{:\&}/\texttt{RNil} and
\texttt{IS}/\texttt{IZ}), it makes the type errors and constructions a lot
easier to work with and reason with.

However, we can get a little bit of the best of both worlds by using typeclasses
to auto-insert the \texttt{Index} witnesses into a list.

First, we can write a typeclass that searches a type-level list of fields and
produces the right \texttt{Index}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L51{-}L58}

\KeywordTok{class} \DataTypeTok{ListIx}\NormalTok{ (}\OtherTok{l ::} \DataTypeTok{Symbol}\NormalTok{) (}\OtherTok{xs ::}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)]) (}\OtherTok{a ::} \DataTypeTok{Ty}\NormalTok{) }\OperatorTok{|}\NormalTok{ l xs }\OtherTok{{-}\textgreater{}}\NormalTok{ a }\KeywordTok{where}
\OtherTok{  listIx ::} \DataTypeTok{Index}\NormalTok{ xs (l }\OperatorTok{:::}\NormalTok{ a)}

\KeywordTok{instance} \DataTypeTok{ListIx}\NormalTok{ l (l }\OperatorTok{:::}\NormalTok{ a }\OperatorTok{:}\NormalTok{ xs) a }\KeywordTok{where}
\NormalTok{  listIx }\OtherTok{=} \DataTypeTok{IZ}

\KeywordTok{instance} \OtherTok{\{{-}\# OVERLAPPABLE \#{-}\}} \DataTypeTok{ListIx}\NormalTok{ l xs a }\OtherTok{=\textgreater{}} \DataTypeTok{ListIx}\NormalTok{ l (m }\OperatorTok{:::}\NormalTok{ b }\OperatorTok{:}\NormalTok{ xs) a }\KeywordTok{where}
\NormalTok{  listIx }\OtherTok{=} \DataTypeTok{IS}\NormalTok{ (listIx }\OperatorTok{@}\NormalTok{l)}
\end{Highlighting}
\end{Shaded}

The FunDep \texttt{l\ xs\ -\textgreater{}\ a} lets us use this like a function:
for a label \texttt{l} and a list \texttt{xs}, we should be able to uniquely
determine the \texttt{a} type it singles out, if it exists. So we have an
instance of
\texttt{ListIx\ "value"\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]}\ TInt},
where the label \texttt{"value"} and the list uniquely determines the result
type \texttt{TInt}.

We can now have a helper function that we can call like
\texttt{eAccess\ "value"} using GHC 9.10's \texttt{RequiredTypeArguments}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L118{-}L123}

\OtherTok{eAccess ::}
  \KeywordTok{forall}\NormalTok{ (}\OtherTok{l ::} \DataTypeTok{Symbol}\NormalTok{) }\OtherTok{{-}\textgreater{}}
\NormalTok{  (}\DataTypeTok{KnownSymbol}\NormalTok{ l, }\DataTypeTok{ListIx}\NormalTok{ l as a) }\OtherTok{=\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ as) }\OtherTok{{-}\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ a}
\NormalTok{eAccess l e }\OtherTok{=} \DataTypeTok{EAccess} \OperatorTok{@}\NormalTok{l e (listIx }\OperatorTok{@}\NormalTok{l)}
\end{Highlighting}
\end{Shaded}

That lets us write the field name directly, and the compiler will generate the
\texttt{Index} automatically for us:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L167{-}L176}

\OtherTok{namedAccessExample ::} \DataTypeTok{Expr} \DataTypeTok{TString}
\NormalTok{namedAccessExample }\OtherTok{=}
\NormalTok{  eAccess}
    \StringTok{"label"}
\NormalTok{    ( }\DataTypeTok{ERecord}
\NormalTok{        ( eField }\StringTok{"value"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}
            \OperatorTok{:\&}\NormalTok{ eField }\StringTok{"label"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"found"}\NormalTok{))}
            \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{        )}
\NormalTok{    )}
\end{Highlighting}
\end{Shaded}

Here,
\texttt{eAccess\ "value"\ ::\ Expr\ (TRecord\ {[}"value"\ :::\ TInt,\ "label"\ :::\ TString{]})\ -\textgreater{}\ Expr\ TInt},
its result type uniquely determined by the types in the record fields.

The same trick works for sum injections, so we can write the constructor name
directly:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L125{-}L179}

\OtherTok{eChoice ::}
  \KeywordTok{forall}\NormalTok{ (}\OtherTok{l ::} \DataTypeTok{Symbol}\NormalTok{) }\OtherTok{{-}\textgreater{}}
\NormalTok{  (}\DataTypeTok{KnownSymbol}\NormalTok{ l, }\DataTypeTok{ListIx}\NormalTok{ l as a) }\OtherTok{=\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ a }\OtherTok{{-}\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ as)}
\NormalTok{eChoice l e }\OtherTok{=} \DataTypeTok{EChoice} \OperatorTok{@}\NormalTok{l (listIx }\OperatorTok{@}\NormalTok{l) e}

\OtherTok{namedChoiceExample ::} \DataTypeTok{Expr}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ [}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{])}
\NormalTok{namedChoiceExample }\OtherTok{=}\NormalTok{ eChoice }\StringTok{"Missing"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"not here"}\NormalTok{))}
\end{Highlighting}
\end{Shaded}

Here,
\texttt{eChoice\ "Missing"\ ::\ Expr\ TString\ -\textgreater{}\ Expr\ (TSum\ {[}"Found"\ :::\ TInt,\ "Missing"\ :::\ TString{]})},
because the constructor name \texttt{"Missing"} uniquely determines the payload
type inside that sum.

\subsection{Pretty-Printing Records and
Sums}\label{pretty-printing-records-and-sums}

To pretty-print, we finally use that \texttt{KnownSymbol} constraint we've been
tracking this entire time. We can use
\texttt{symbolVal\ ::\ KnownSymbol\ s\ =\textgreater{}\ p\ s\ -\textgreater{}\ String}
to get the string \emph{value} from the type-level string.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage3.hs\#L237{-}L282}

\OtherTok{ppPrim ::} \DataTypeTok{Prim}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppPrim }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{PInt}\NormalTok{ n }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty n}
  \DataTypeTok{PBool}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \KeywordTok{if}\NormalTok{ b }\KeywordTok{then} \StringTok{"true"} \KeywordTok{else} \StringTok{"false"}
  \DataTypeTok{PString}\NormalTok{ s }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty (}\FunctionTok{show}\NormalTok{ s)}

\OtherTok{ppOp ::} \DataTypeTok{Op}\NormalTok{ a b c }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppOp }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \StringTok{"+"}
  \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \StringTok{"*"}
  \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \StringTok{"\textless{}="}
  \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \StringTok{"\&\&"}

\OtherTok{ppFields ::} \DataTypeTok{Rec} \DataTypeTok{ExprField}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}\NormalTok{ [}\DataTypeTok{PP.Doc}\NormalTok{ ann]}
\NormalTok{ppFields }\DataTypeTok{RNil} \OtherTok{=}\NormalTok{ []}
\NormalTok{ppFields (}\DataTypeTok{EField} \OperatorTok{@}\NormalTok{l x }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{=}
\NormalTok{  (PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l)) }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"="} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ x) }\OperatorTok{:}\NormalTok{ ppFields xs}

\OtherTok{ppHandlers ::} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprHandler}\NormalTok{ b) xs }\OtherTok{{-}\textgreater{}}\NormalTok{ [}\DataTypeTok{PP.Doc}\NormalTok{ ann]}
\NormalTok{ppHandlers }\DataTypeTok{RNil} \OtherTok{=}\NormalTok{ []}
\NormalTok{ppHandlers (}\DataTypeTok{EHandler} \OperatorTok{@}\NormalTok{l \_ n body }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{=}
\NormalTok{  (PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l)) }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ PP.pretty n }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ body) }\OperatorTok{:}\NormalTok{ ppHandlers xs}

\OtherTok{ppExpr ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppExpr paren }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ p }\OtherTok{{-}\textgreater{}}\NormalTok{ ppPrim p}
  \DataTypeTok{EVar}\NormalTok{ \_ v }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty v}
  \DataTypeTok{ELambda}\NormalTok{ \_ n body }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$} \StringTok{"\textbackslash{}\textbackslash{}"} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty n }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ f }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppOp o }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ y}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{", "}\NormalTok{ (ppFields xs)}
  \DataTypeTok{EAccess} \OperatorTok{@}\NormalTok{l e \_ }\OtherTok{{-}\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ e }\OperatorTok{\textless{}\textgreater{}} \StringTok{"."} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l))}
  \DataTypeTok{EChoice} \OperatorTok{@}\NormalTok{l \_ x }\OtherTok{{-}\textgreater{}}\NormalTok{ wrap }\OperatorTok{$}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l)) }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}
\NormalTok{      PP.sep}
\NormalTok{        [ }\StringTok{"case"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr }\DataTypeTok{False}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"of"}
\NormalTok{        , PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{"; "}\NormalTok{ (ppHandlers hs)}
\NormalTok{        ]}
  \KeywordTok{where}
\NormalTok{    wrap}
      \OperatorTok{|}\NormalTok{ paren }\OtherTok{=}\NormalTok{ PP.parens}
      \OperatorTok{|} \FunctionTok{otherwise} \OtherTok{=} \FunctionTok{id}

\OtherTok{prettyExpr ::} \DataTypeTok{Expr}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{prettyExpr }\OtherTok{=}\NormalTok{ ppExpr }\DataTypeTok{False}
\end{Highlighting}
\end{Shaded}

\section{Capturing Variables}\label{capturing-variables}

In order to have \texttt{EVar} be type-safe, the environment itself needs to be
a part of the \texttt{Expr} type, and you should only be able to use
\texttt{EVar} if the \texttt{Expr} enforces it. \texttt{ELambda} would,
therefore, introduce the new variable to the environment.

We'll have:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L80{-}L80}

\KeywordTok{data} \DataTypeTok{Expr}\OtherTok{ ::}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)] }\OtherTok{{-}\textgreater{}} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
\end{Highlighting}
\end{Shaded}

So a value of type \texttt{Expr\ {[}"x"\ :::\ TInt,\ "y"\ :::\ TBool{]}\ t} is
an expression with free variables \texttt{x} of type \texttt{Int} and \texttt{y}
of type \texttt{Bool}.

Surprise! That small detour to add records and sums to our language actually
ended up being a smooth precursor to all of the techniques we will be using to
solve for variable binders.

\texttt{ELambda} would therefore take an \texttt{Expr} with a free variable and
turn it into an \texttt{Expr} of a function type. We also keep a
\texttt{KnownSymbol} constraint for the name so that we can recover the name
when we render the expression.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L83{-}L83}

  \DataTypeTok{ELambda}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ n }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (n }\OperatorTok{:::}\NormalTok{ a \textquotesingle{}}\OperatorTok{:}\NormalTok{ vs) b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
\end{Highlighting}
\end{Shaded}

\texttt{EVar} then becomes exactly like \texttt{EAccess}! We ``index'' into the
environment of the \texttt{Expr\ vs\ a} using \texttt{Index}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L82{-}L82}

  \DataTypeTok{EVar}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ vs (n }\OperatorTok{:::}\NormalTok{ t) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs t}
\end{Highlighting}
\end{Shaded}

So it is legal to have
\texttt{EVar\ IZ\ ::\ Expr\ {[}"x"\ :::\ TInt,\ "y"\ :::\ TBool{]}\ TInt}, and
also it is automatically inferred to be a \texttt{TInt}. But we could \emph{not}
write \texttt{EVar\ IZ\ ::\ Expr\ {[}{]}\ TInt}.

And finally, our whole \texttt{Expr}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L80{-}L89}

\KeywordTok{data} \DataTypeTok{Expr}\OtherTok{ ::}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)] }\OtherTok{{-}\textgreater{}} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EPrim}\OtherTok{ ::} \DataTypeTok{Prim}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs t}
  \DataTypeTok{EVar}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ vs (n }\OperatorTok{:::}\NormalTok{ t) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs t}
  \DataTypeTok{ELambda}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ n }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (n }\OperatorTok{:::}\NormalTok{ a \textquotesingle{}}\OperatorTok{:}\NormalTok{ vs) b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
  \DataTypeTok{EApply}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ vs (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs b}
  \DataTypeTok{EOp}\OtherTok{ ::} \DataTypeTok{Op}\NormalTok{ a b c }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs c}
  \DataTypeTok{ERecord}\OtherTok{ ::} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprField}\NormalTok{ vs) as }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TRecord}\NormalTok{ as)}
  \DataTypeTok{EAccess}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TRecord}\NormalTok{ as) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Index}\NormalTok{ as (l }\OperatorTok{:::}\NormalTok{ a) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a}
  \DataTypeTok{EChoice}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Index}\NormalTok{ as (l }\OperatorTok{:::}\NormalTok{ a) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TSum}\NormalTok{ as)}
  \DataTypeTok{ECase}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TSum}\NormalTok{ as) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprHandler}\NormalTok{ vs b) as }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs b}
\end{Highlighting}
\end{Shaded}

Just like with record access, we can use the \texttt{ListIx} class to write a
named helper:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L47{-}L120}

\KeywordTok{class} \DataTypeTok{ListIx}\NormalTok{ (}\OtherTok{l ::} \DataTypeTok{Symbol}\NormalTok{) (}\OtherTok{xs ::}\NormalTok{ [(}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{)]) (}\OtherTok{a ::} \DataTypeTok{Ty}\NormalTok{) }\OperatorTok{|}\NormalTok{ l xs }\OtherTok{{-}\textgreater{}}\NormalTok{ a }\KeywordTok{where}
\OtherTok{  listIx ::} \DataTypeTok{Index}\NormalTok{ xs (l }\OperatorTok{:::}\NormalTok{ a)}

\KeywordTok{instance} \DataTypeTok{ListIx}\NormalTok{ l (l }\OperatorTok{:::}\NormalTok{ a \textquotesingle{}}\OperatorTok{:}\NormalTok{ xs) a }\KeywordTok{where}
\NormalTok{  listIx }\OtherTok{=} \DataTypeTok{IZ}

\KeywordTok{instance} \OtherTok{\{{-}\# OVERLAPPABLE \#{-}\}} \DataTypeTok{ListIx}\NormalTok{ l xs a }\OtherTok{=\textgreater{}} \DataTypeTok{ListIx}\NormalTok{ l (m }\OperatorTok{:::}\NormalTok{ b \textquotesingle{}}\OperatorTok{:}\NormalTok{ xs) a }\KeywordTok{where}
\NormalTok{  listIx }\OtherTok{=} \DataTypeTok{IS}\NormalTok{ (listIx }\OperatorTok{@}\NormalTok{l)}

\OtherTok{eVar ::} \KeywordTok{forall}\NormalTok{ n }\OtherTok{{-}\textgreater{}} \DataTypeTok{ListIx}\NormalTok{ n vs a }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a}
\NormalTok{eVar n }\OtherTok{=} \DataTypeTok{EVar}\NormalTok{ (listIx }\OperatorTok{@}\NormalTok{n)}
\end{Highlighting}
\end{Shaded}

Adding in our other \texttt{-XRequiredTypeArguments} helpers:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L91{-}L117}

\OtherTok{eLambda ::} \KeywordTok{forall}\NormalTok{ n }\OtherTok{{-}\textgreater{}} \DataTypeTok{KnownSymbol}\NormalTok{ n }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ (n }\OperatorTok{:::}\NormalTok{ a \textquotesingle{}}\OperatorTok{:}\NormalTok{ vs) b }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}
\NormalTok{eLambda n }\OtherTok{=} \DataTypeTok{ELambda} \OperatorTok{@}\NormalTok{n}

\OtherTok{eField ::} \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs a }\OtherTok{{-}\textgreater{}} \DataTypeTok{ExprField}\NormalTok{ vs (l }\OperatorTok{:::}\NormalTok{ a)}
\NormalTok{eField l }\OtherTok{=} \DataTypeTok{EField} \OperatorTok{@}\NormalTok{l}

\OtherTok{eAccess ::}
  \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}}
\NormalTok{  (}\DataTypeTok{KnownSymbol}\NormalTok{ l, }\DataTypeTok{ListIx}\NormalTok{ l as a) }\OtherTok{=\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TRecord}\NormalTok{ as) }\OtherTok{{-}\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ vs a}
\NormalTok{eAccess l e }\OtherTok{=} \DataTypeTok{EAccess} \OperatorTok{@}\NormalTok{l e (listIx }\OperatorTok{@}\NormalTok{l)}

\OtherTok{eChoice ::}
  \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}}
\NormalTok{  (}\DataTypeTok{KnownSymbol}\NormalTok{ l, }\DataTypeTok{ListIx}\NormalTok{ l as a) }\OtherTok{=\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ vs a }\OtherTok{{-}\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ vs (}\DataTypeTok{TSum}\NormalTok{ as)}
\NormalTok{eChoice l e }\OtherTok{=} \DataTypeTok{EChoice} \OperatorTok{@}\NormalTok{l (listIx }\OperatorTok{@}\NormalTok{l) e}

\OtherTok{eHandler ::}
  \KeywordTok{forall}\NormalTok{ n }\OtherTok{{-}\textgreater{}}
  \KeywordTok{forall}\NormalTok{ l }\OtherTok{{-}\textgreater{}}
\NormalTok{  (}\DataTypeTok{KnownSymbol}\NormalTok{ n, }\DataTypeTok{KnownSymbol}\NormalTok{ l) }\OtherTok{=\textgreater{}}
  \DataTypeTok{Expr}\NormalTok{ (n }\OperatorTok{:::}\NormalTok{ a \textquotesingle{}}\OperatorTok{:}\NormalTok{ vs) b }\OtherTok{{-}\textgreater{}}
  \DataTypeTok{ExprHandler}\NormalTok{ vs b (l }\OperatorTok{:::}\NormalTok{ a)}
\NormalTok{eHandler n l }\OtherTok{=} \DataTypeTok{EHandler} \OperatorTok{@}\NormalTok{n }\OperatorTok{@}\NormalTok{l}
\end{Highlighting}
\end{Shaded}

And we get something that is \emph{truly} type-safe: all expressions are
well-typed, and all variables are ensured to be bound!

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L139{-}L171}

\OtherTok{fifteen ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}
\NormalTok{fifteen }\OtherTok{=}
  \DataTypeTok{EApply}
\NormalTok{    (eLambda }\StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OTimes}\NormalTok{ (eVar }\StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{))))}
\NormalTok{    (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{5}\NormalTok{))}

\OtherTok{recordExample ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}
\NormalTok{recordExample }\OtherTok{=}
  \DataTypeTok{EOp}
    \DataTypeTok{OPlus}
\NormalTok{    ( eAccess}
        \StringTok{"value"}
\NormalTok{        ( }\DataTypeTok{ERecord}
\NormalTok{            ( eField }\StringTok{"value"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}
                \OperatorTok{:\&}\NormalTok{ eField }\StringTok{"label"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString} \StringTok{"found"}\NormalTok{))}
                \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{            )}
\NormalTok{        )}
\NormalTok{    )}
\NormalTok{    (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{))}

\OtherTok{sumExample ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}
\NormalTok{sumExample }\OtherTok{=}
  \DataTypeTok{ECase}
\NormalTok{    (eChoice }\StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{)))}
\NormalTok{    ( eHandler }\StringTok{"value"} \StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (eVar }\StringTok{"value"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
        \OperatorTok{:\&}\NormalTok{ eHandler }\StringTok{"message"} \StringTok{"Missing"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{0}\NormalTok{))}
        \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{    )}
\end{Highlighting}
\end{Shaded}

\subsection{What we gained}\label{what-we-gained}

Now all of the previous ``bad'' examples we gave are finally compiler-verified:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t (}\DataTypeTok{EVar} \DataTypeTok{IZ}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{)}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{Couldn\textquotesingle{}t}\NormalTok{ match }\KeywordTok{type}\OperatorTok{:}\NormalTok{ (n0 }\OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{) }\OperatorTok{:}\NormalTok{ xs0}
\NormalTok{                     with}\OperatorTok{:}\NormalTok{ \textquotesingle{}[]}
      \DataTypeTok{Expected}\OperatorTok{:} \DataTypeTok{Index}\NormalTok{ \textquotesingle{}[] (n0 }\OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{)}
        \DataTypeTok{Actual}\OperatorTok{:} \DataTypeTok{Index}\NormalTok{ ((n0 }\OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{) }\OperatorTok{:}\NormalTok{ xs0) (n0 }\OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{)}

\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t (}\DataTypeTok{EVar} \DataTypeTok{IZ}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] }\DataTypeTok{TInt}\NormalTok{)}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{Couldn\textquotesingle{}t}\NormalTok{ match }\KeywordTok{type}\NormalTok{ ‘}\DataTypeTok{TString}\NormalTok{’ with ‘}\DataTypeTok{TInt}\NormalTok{’}
      \DataTypeTok{Expected}\OperatorTok{:} \DataTypeTok{Index}\NormalTok{ \textquotesingle{}[}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] (}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{)}
        \DataTypeTok{Actual}\OperatorTok{:} \DataTypeTok{Index}\NormalTok{ \textquotesingle{}[}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] (}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{)}

\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{ECase}
\NormalTok{      (}\DataTypeTok{EChoice} \OperatorTok{@}\StringTok{"Found"} \DataTypeTok{IZ}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] (}\DataTypeTok{TSum}\NormalTok{ \textquotesingle{}[}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]))}
\NormalTok{      ( }\DataTypeTok{EHandler} \OperatorTok{@}\StringTok{"value"} \OperatorTok{@}\StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar}\NormalTok{ (}\DataTypeTok{IS} \DataTypeTok{IZ}\NormalTok{)) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
          \OperatorTok{:\&} \DataTypeTok{EHandler} \OperatorTok{@}\StringTok{"message"} \OperatorTok{@}\StringTok{"Missing"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (}\DataTypeTok{EVar} \DataTypeTok{IZ}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
          \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{      )}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{Couldn\textquotesingle{}t}\NormalTok{ match }\KeywordTok{type}\OperatorTok{:}\NormalTok{ (n0 }\OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{) }\OperatorTok{:}\NormalTok{ xs0}
\NormalTok{                     with}\OperatorTok{:}\NormalTok{ \textquotesingle{}[]}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{Couldn\textquotesingle{}t}\NormalTok{ match }\KeywordTok{type}\NormalTok{ ‘}\DataTypeTok{TString}\NormalTok{’ with ‘}\DataTypeTok{TInt}\NormalTok{’}
\end{Highlighting}
\end{Shaded}

And using the \texttt{ListIx} helpers, those same failures show up as failed
index searches:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t (eVar }\StringTok{"missing"}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{)}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{No} \KeywordTok{instance}\NormalTok{ for ‘}\DataTypeTok{ListIx} \StringTok{"missing"}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{’}

\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t (eVar }\StringTok{"x"}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{] }\DataTypeTok{TInt}\NormalTok{)}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{No} \KeywordTok{instance}\NormalTok{ for ‘}\DataTypeTok{ListIx} \StringTok{"x"}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{’}

\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{ECase}
\NormalTok{      (eChoice }\StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{7}\NormalTok{))}\OtherTok{ ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] (}\DataTypeTok{TSum}\NormalTok{ \textquotesingle{}[}\StringTok{"Found"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"Missing"} \OperatorTok{:::} \DataTypeTok{TString}\NormalTok{]))}
\NormalTok{      ( eHandler }\StringTok{"value"} \StringTok{"Found"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (eVar }\StringTok{"missing"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
          \OperatorTok{:\&}\NormalTok{ eHandler }\StringTok{"message"} \StringTok{"Missing"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (eVar }\StringTok{"message"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{1}\NormalTok{)))}
          \OperatorTok{:\&} \DataTypeTok{RNil}
\NormalTok{      )}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{No} \KeywordTok{instance}\NormalTok{ for ‘}\DataTypeTok{ListIx} \StringTok{"missing"}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{’}
\OperatorTok{\textless{}}\NormalTok{interactive}\OperatorTok{\textgreater{}} \FunctionTok{error}\OperatorTok{:}
\NormalTok{    • }\DataTypeTok{No} \KeywordTok{instance}\NormalTok{ for ‘}\DataTypeTok{ListIx} \StringTok{"message"}\NormalTok{ \textquotesingle{}[] }\DataTypeTok{TInt}\NormalTok{’}
\end{Highlighting}
\end{Shaded}

Expressions that are not well-typed in our domain language are now rejected by
GHC!\footnote{Excluding \texttt{\_\textbar{}\_} in Haskell-land (recursion or
  \texttt{undefined}), unfortunately.}

(As an exercise, can understand why those errors are what they are? Why they all
contain \texttt{ListIx\ \_\ \textquotesingle{}{[}{]}}? For more ergonomics there
is stuff we can do with \texttt{TypeError} machinery to make the messages a
little prettier; the \emph{vinyl} library does a lot to make error messages a
bit better, like in \texttt{HasField}
\href{https://hackage.haskell.org/package/vinyl/docs/Data-Vinyl-Derived.html\#t:FieldType}{instance})

Note that this is sometimes done using straight
\href{https://en.wikipedia.org/wiki/De_Bruijn_index}{De Bruijn indices}:
\texttt{Expr\ ::\ {[}Ty{]}\ -\textgreater{}\ Type}, so we don't use any names
but just the direct index, but the point of this exercise is to be
\emph{borderline} unbearable to write, and \emph{not} to be \emph{actually}
unbearable to write.

\subsection{Eval with a typed environment}\label{eval-with-a-typed-environment}

To actually write \emph{eval} now, we need to have a type-safe environment to
store these variables. In order to \texttt{eval} an \texttt{Expr\ vs}, we need
\texttt{EValue}s for each \texttt{v} in \texttt{vs}. So for
\texttt{Expr\ {[}"x"\ :::\ TInt,\ "y"\ :::\ TBool{]}}, we need to store a
\texttt{TInt} and a \texttt{TBool}. We can once again re-purpose \texttt{Rec}:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L130{-}L131}

\KeywordTok{data} \DataTypeTok{EValueField}\OtherTok{ ::}\NormalTok{ (}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EVField}\OtherTok{ ::} \DataTypeTok{EValue}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValueField}\NormalTok{ \textquotesingle{}(l, a)}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t (}\DataTypeTok{EVField}\NormalTok{ (}\DataTypeTok{EVInt} \DecValTok{3}\NormalTok{) }\OperatorTok{:\&} \DataTypeTok{EVField}\NormalTok{ (}\DataTypeTok{EVBool} \DataTypeTok{True}\NormalTok{) }\OperatorTok{:\&} \DataTypeTok{RNil}\OtherTok{ ::} \DataTypeTok{Rec} \DataTypeTok{EValueField}\NormalTok{ [}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"y"} \OperatorTok{:::} \DataTypeTok{TBool}\NormalTok{])}
\DataTypeTok{Rec} \DataTypeTok{EValueField}\NormalTok{ [}\StringTok{"x"} \OperatorTok{:::} \DataTypeTok{TInt}\NormalTok{, }\StringTok{"y"} \OperatorTok{:::} \DataTypeTok{TBool}\NormalTok{]}
\end{Highlighting}
\end{Shaded}

And so we can finally write:

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L122{-}L271}

\KeywordTok{data} \DataTypeTok{EValue}\OtherTok{ ::} \DataTypeTok{Ty} \OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{EVInt}\OtherTok{ ::} \DataTypeTok{Int} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TInt}
  \DataTypeTok{EVBool}\OtherTok{ ::} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TBool}
  \DataTypeTok{EVString}\OtherTok{ ::} \DataTypeTok{String} \OtherTok{{-}\textgreater{}} \DataTypeTok{EValue} \DataTypeTok{TString}
  \DataTypeTok{EVRecord}\OtherTok{ ::} \DataTypeTok{Rec} \DataTypeTok{EValueField}\NormalTok{ as }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ (}\DataTypeTok{TRecord}\NormalTok{ as)}
  \DataTypeTok{EVSum}\OtherTok{ ::} \DataTypeTok{Index}\NormalTok{ as (l }\OperatorTok{:::}\NormalTok{ a) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ (}\DataTypeTok{TSum}\NormalTok{ as)}
  \DataTypeTok{EVFun}\OtherTok{ ::}\NormalTok{ (}\DataTypeTok{EValue}\NormalTok{ a }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ (a }\OperatorTok{:{-}\textgreater{}}\NormalTok{ b)}

\OtherTok{eval ::} \DataTypeTok{Rec} \DataTypeTok{EValueField}\NormalTok{ vs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs t }\OtherTok{{-}\textgreater{}} \DataTypeTok{EValue}\NormalTok{ t}
\NormalTok{eval env }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt}\NormalTok{ n) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVInt}\NormalTok{ n}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PBool}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVBool}\NormalTok{ b}
  \DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PString}\NormalTok{ s) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVString}\NormalTok{ s}
  \DataTypeTok{EVar}\NormalTok{ i }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ indexRec i env }\KeywordTok{of}
    \DataTypeTok{EVField}\NormalTok{ v }\OtherTok{{-}\textgreater{}}\NormalTok{ v}
  \DataTypeTok{ELambda}\NormalTok{ body }\OtherTok{{-}\textgreater{}}
    \DataTypeTok{EVFun} \OperatorTok{$}\NormalTok{ \textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (}\DataTypeTok{EVField}\NormalTok{ x }\OperatorTok{:\&}\NormalTok{ env) body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ eval env f }\KeywordTok{of}
    \DataTypeTok{EVFun}\NormalTok{ g }\OtherTok{{-}\textgreater{}}\NormalTok{ g (eval env x)}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ (o, eval env x, eval env y) }\KeywordTok{of}
\NormalTok{    (}\DataTypeTok{OPlus}\NormalTok{, }\DataTypeTok{EVInt}\NormalTok{ a, }\DataTypeTok{EVInt}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{+}\NormalTok{ b)}
\NormalTok{    (}\DataTypeTok{OTimes}\NormalTok{, }\DataTypeTok{EVInt}\NormalTok{ a, }\DataTypeTok{EVInt}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVInt}\NormalTok{ (a }\OperatorTok{*}\NormalTok{ b)}
\NormalTok{    (}\DataTypeTok{OLte}\NormalTok{, }\DataTypeTok{EVInt}\NormalTok{ a, }\DataTypeTok{EVInt}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\textless{}=}\NormalTok{ b)}
\NormalTok{    (}\DataTypeTok{OAnd}\NormalTok{, }\DataTypeTok{EVBool}\NormalTok{ a, }\DataTypeTok{EVBool}\NormalTok{ b) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVBool}\NormalTok{ (a }\OperatorTok{\&\&}\NormalTok{ b)}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}
    \DataTypeTok{EVRecord} \OperatorTok{$}\NormalTok{ mapRec (\textbackslash{}(}\DataTypeTok{EField}\NormalTok{ x) }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVField}\NormalTok{ (eval env x)) xs}
  \DataTypeTok{EAccess}\NormalTok{ e i }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ eval env e }\KeywordTok{of}
    \DataTypeTok{EVRecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ indexRec i xs }\KeywordTok{of}
      \DataTypeTok{EVField}\NormalTok{ v }\OtherTok{{-}\textgreater{}}\NormalTok{ v}
  \DataTypeTok{EChoice}\NormalTok{ i x }\OtherTok{{-}\textgreater{}} \DataTypeTok{EVSum}\NormalTok{ i (eval env x)}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ eval env x }\KeywordTok{of}
    \DataTypeTok{EVSum}\NormalTok{ i y }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ indexRec i hs }\KeywordTok{of}
      \DataTypeTok{EHandler}\NormalTok{ h }\OtherTok{{-}\textgreater{}}\NormalTok{ eval (}\DataTypeTok{EVField}\NormalTok{ y }\OperatorTok{:\&}\NormalTok{ env) h}
\end{Highlighting}
\end{Shaded}

At least, we are here. A type-safe EDSL where only AST's that can be validly
evaluated are legal to represent in Haskell. At least, we can embrace the
freedom of not having to carefully construct your terms. You can relax now. The
compiler and the types have your back.

Even
\texttt{EVFun\ ::\ (EValue\ a\ -\textgreater{}\ EValue\ b)\ -\textgreater{}\ EValue\ (a\ :-\textgreater{}\ b)}
has a total \texttt{EValue\ a\ -\textgreater{}\ EValue\ b}, making the closure
evaluation also fully total.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L145{-}L147}

\OtherTok{plusThree ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] (}\DataTypeTok{TInt} \OperatorTok{:{-}\textgreater{}} \DataTypeTok{TInt}\NormalTok{)}
\NormalTok{plusThree }\OtherTok{=}
\NormalTok{  eLambda }\StringTok{"x"}\NormalTok{ (}\DataTypeTok{EOp} \DataTypeTok{OPlus}\NormalTok{ (eVar }\StringTok{"x"}\NormalTok{) (}\DataTypeTok{EPrim}\NormalTok{ (}\DataTypeTok{PInt} \DecValTok{3}\NormalTok{)))}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \KeywordTok{case}\NormalTok{ eval }\DataTypeTok{RNil}\NormalTok{ plusThree }\KeywordTok{of}
    \DataTypeTok{EVFun}\NormalTok{ f }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ f (}\DataTypeTok{EVInt} \DecValTok{4}\NormalTok{) }\KeywordTok{of}
      \DataTypeTok{EVInt}\NormalTok{ x }\OtherTok{{-}\textgreater{}} \FunctionTok{print}\NormalTok{ x}
\DecValTok{7}
\end{Highlighting}
\end{Shaded}

\subsection{Pretty-Printing Scoped
Expressions}\label{pretty-printing-scoped-expressions}

Now to get to the entire utility of this abstraction: inspecting and consuming
the structure. For our new structure, we took out the string name from
\texttt{EVar} in lieu of an index. This is intentional, so that we keep the
``responsibility'' of storing the string name at the \texttt{ELambda}
constructor and not have \texttt{EVar} redundantly store it.

However, this means that for pretty-printing, we will need to track the variable
names in the environment as we descend into lambdas. This is done very similar
to how it was done in \texttt{eval}, but instead of tracking and indexing out
the evaluated \texttt{EValue}s, we track and index out the string names of each
variable instead.

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L182{-}L183}

\KeywordTok{data} \DataTypeTok{NameField}\OtherTok{ ::}\NormalTok{ (}\DataTypeTok{Symbol}\NormalTok{, }\DataTypeTok{Ty}\NormalTok{) }\OtherTok{{-}\textgreater{}} \DataTypeTok{Type} \KeywordTok{where}
  \DataTypeTok{NameField}\OtherTok{ ::} \DataTypeTok{KnownSymbol}\NormalTok{ l }\OtherTok{=\textgreater{}} \DataTypeTok{NameField}\NormalTok{ (l }\OperatorTok{:::}\NormalTok{ a)}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}} \OperatorTok{:}\NormalTok{t }\DataTypeTok{NameField} \OperatorTok{@}\StringTok{"hello"} \OperatorTok{:\&} \DataTypeTok{NameField} \OperatorTok{@}\StringTok{"world"} \OperatorTok{:\&} \DataTypeTok{RNil}
\DataTypeTok{Rec} \DataTypeTok{NameField}\NormalTok{ [}\StringTok{"hello"} \OperatorTok{:::}\NormalTok{ a, }\StringTok{"world"} \OperatorTok{:::}\NormalTok{ b]}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\CommentTok{{-}{-} source: https://github.com/mstksg/inCode/tree/master/code{-}samples/typed{-}sm{-}lc/ExprStage4.hs\#L185{-}L245}

\OtherTok{ppPrim ::} \DataTypeTok{Prim}\NormalTok{ t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppPrim }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{PInt}\NormalTok{ n }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty n}
  \DataTypeTok{PBool}\NormalTok{ b }\OtherTok{{-}\textgreater{}} \KeywordTok{if}\NormalTok{ b }\KeywordTok{then} \StringTok{"true"} \KeywordTok{else} \StringTok{"false"}
  \DataTypeTok{PString}\NormalTok{ s }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty (}\FunctionTok{show}\NormalTok{ s)}

\OtherTok{ppOp ::} \DataTypeTok{Op}\NormalTok{ a b c }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppOp }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{OPlus} \OtherTok{{-}\textgreater{}} \StringTok{"+"}
  \DataTypeTok{OTimes} \OtherTok{{-}\textgreater{}} \StringTok{"*"}
  \DataTypeTok{OLte} \OtherTok{{-}\textgreater{}} \StringTok{"\textless{}="}
  \DataTypeTok{OAnd} \OtherTok{{-}\textgreater{}} \StringTok{"\&\&"}

\OtherTok{ppFields ::} \DataTypeTok{Rec} \DataTypeTok{NameField}\NormalTok{ vs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprField}\NormalTok{ vs) xs }\OtherTok{{-}\textgreater{}}\NormalTok{ [}\DataTypeTok{PP.Doc}\NormalTok{ ann]}
\NormalTok{ppFields \_ }\DataTypeTok{RNil} \OtherTok{=}\NormalTok{ []}
\NormalTok{ppFields names (}\DataTypeTok{EField} \OperatorTok{@}\NormalTok{l x }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{=}
\NormalTok{  (PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l)) }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"="} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr names }\DataTypeTok{False}\NormalTok{ x) }\OperatorTok{:}\NormalTok{ ppFields names xs}

\OtherTok{ppHandlers ::} \DataTypeTok{Rec} \DataTypeTok{NameField}\NormalTok{ vs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Rec}\NormalTok{ (}\DataTypeTok{ExprHandler}\NormalTok{ vs b) xs }\OtherTok{{-}\textgreater{}}\NormalTok{ [}\DataTypeTok{PP.Doc}\NormalTok{ ann]}
\NormalTok{ppHandlers \_ }\DataTypeTok{RNil} \OtherTok{=}\NormalTok{ []}
\NormalTok{ppHandlers names (}\DataTypeTok{EHandler} \OperatorTok{@}\NormalTok{n }\OperatorTok{@}\NormalTok{l body }\OperatorTok{:\&}\NormalTok{ xs) }\OtherTok{=}
\NormalTok{  ( PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l))}
      \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{n))}
      \OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"}
      \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr (}\DataTypeTok{NameField} \OperatorTok{@}\NormalTok{n }\OperatorTok{:\&}\NormalTok{ names) }\DataTypeTok{False}\NormalTok{ body}
\NormalTok{  )}
    \OperatorTok{:}\NormalTok{ ppHandlers names xs}

\OtherTok{ppExpr ::} \DataTypeTok{Rec} \DataTypeTok{NameField}\NormalTok{ vs }\OtherTok{{-}\textgreater{}} \DataTypeTok{Bool} \OtherTok{{-}\textgreater{}} \DataTypeTok{Expr}\NormalTok{ vs t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{ppExpr names paren }\OtherTok{=}\NormalTok{ \textbackslash{}}\KeywordTok{case}
  \DataTypeTok{EPrim}\NormalTok{ p }\OtherTok{{-}\textgreater{}}\NormalTok{ ppPrim p}
  \DataTypeTok{EVar}\NormalTok{ i }\OtherTok{{-}\textgreater{}} \KeywordTok{case}\NormalTok{ indexRec i names }\KeywordTok{of}
    \DataTypeTok{NameField} \OperatorTok{@}\NormalTok{n }\OtherTok{{-}\textgreater{}}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{n))}
  \DataTypeTok{ELambda} \OperatorTok{@}\NormalTok{n body }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}
      \StringTok{"\textbackslash{}\textbackslash{}"} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{n))}
        \OperatorTok{\textless{}+\textgreater{}} \StringTok{"{-}\textgreater{}"}
        \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr (}\DataTypeTok{NameField} \OperatorTok{@}\NormalTok{n }\OperatorTok{:\&}\NormalTok{ names) }\DataTypeTok{False}\NormalTok{ body}
  \DataTypeTok{EApply}\NormalTok{ f x }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ ppExpr names }\DataTypeTok{True}\NormalTok{ f }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr names }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{EOp}\NormalTok{ o x y }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ ppExpr names }\DataTypeTok{True}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppOp o }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr names }\DataTypeTok{True}\NormalTok{ y}
  \DataTypeTok{ERecord}\NormalTok{ xs }\OtherTok{{-}\textgreater{}}
\NormalTok{    PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{", "}\NormalTok{ (ppFields names xs)}
  \DataTypeTok{EAccess} \OperatorTok{@}\NormalTok{l e \_ }\OtherTok{{-}\textgreater{}}
\NormalTok{    ppExpr names }\DataTypeTok{True}\NormalTok{ e }\OperatorTok{\textless{}\textgreater{}} \StringTok{"."} \OperatorTok{\textless{}\textgreater{}}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l))}
  \DataTypeTok{EChoice} \OperatorTok{@}\NormalTok{l \_ x }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}\NormalTok{ PP.pretty (symbolVal (}\DataTypeTok{Proxy} \OperatorTok{@}\NormalTok{l)) }\OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr names }\DataTypeTok{True}\NormalTok{ x}
  \DataTypeTok{ECase}\NormalTok{ x hs }\OtherTok{{-}\textgreater{}}
\NormalTok{    wrap }\OperatorTok{$}
\NormalTok{      PP.sep}
\NormalTok{        [ }\StringTok{"case"} \OperatorTok{\textless{}+\textgreater{}}\NormalTok{ ppExpr names }\DataTypeTok{False}\NormalTok{ x }\OperatorTok{\textless{}+\textgreater{}} \StringTok{"of"}
\NormalTok{        , PP.encloseSep }\StringTok{"\{ "} \StringTok{" \}"} \StringTok{"; "}\NormalTok{ (ppHandlers names hs)}
\NormalTok{        ]}
  \KeywordTok{where}
\NormalTok{    wrap}
      \OperatorTok{|}\NormalTok{ paren }\OtherTok{=}\NormalTok{ PP.parens}
      \OperatorTok{|} \FunctionTok{otherwise} \OtherTok{=} \FunctionTok{id}

\OtherTok{prettyExpr ::} \DataTypeTok{Expr}\NormalTok{ \textquotesingle{}[] t }\OtherTok{{-}\textgreater{}} \DataTypeTok{PP.Doc}\NormalTok{ ann}
\NormalTok{prettyExpr }\OtherTok{=}\NormalTok{ ppExpr }\DataTypeTok{RNil} \DataTypeTok{False}
\end{Highlighting}
\end{Shaded}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{ghci}\OperatorTok{\textgreater{}}\NormalTok{ prettyExpr fifteen}
\NormalTok{(\textbackslash{}x }\OtherTok{{-}\textgreater{}}\NormalTok{ x }\OperatorTok{*} \DecValTok{3}\NormalTok{) }\DecValTok{5}
\end{Highlighting}
\end{Shaded}

\section{The Next Step}\label{the-next-step}

Well, we set out with a simple goal: an expression language that lives within
Haskell that we can inspect and interrogate within the language, but where it
was impossible to construct (in Haskell) a term that did not type-check (in the
domain language).

But, honestly, why does it matter that our expression language has to reject
invalid domain-level terms at the Haskell level? Why couldn't we go the way of
other expression DSLs in Haskell, where we settle with ``untyped'' terms being
expressible in Haskell, and validated using a separate \texttt{typeCheck}
function to validate terms at runtime?

I don't know. But really, maybe this is another way of taking the old
\href{https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/}{Parse,
Don't Validate} adage to the extreme. Why allow yourself to construct invalid
terms of your domain inside Haskell? Why use a ``validate'' function
(\texttt{isValid}) when you can just make invalid terms impossible to construct?

But\ldots no. There is no other choice. We CANNOT allow invalid domain terms to
be constructible. If we have the ability to do better, we MUST. With great power
comes great responsibility. And if we compromise here, how can we trust
ourselves not to compromise when it really matters?

One must imagine the stubborn typer happy.

In Part 2, we'll use our new EDSL to specify visualizable state machines and
programs within Haskell that are type-checked to be correct, and what it looks
like to actually \emph{use} these within Haskell. And in Part 3, we'll start
``compiling'' them to different language targets and different backends, with
the assurance that our generated programs are all synchronized and
self-consistent.

\subsection{A Note on AI Coding}\label{a-note-on-ai-coding}

I guess I'm going to have to start mentioning this in every post. \emph{But}, I
really do feel like this ``extreme type safety'' approach is more critical than
ever, in the age of agentic coding and LLM. I've been using LLMs in my daily
coding for many months now at this point, and one common pattern I've noticed:
when I start with a design with very clear, very strict types, LLMs excel. They
make much fewer errors, and the type system provides more immediate feedback on
their progress, without needing hundreds of defensive \texttt{x\ !=\ null}-style
guard pollution.

Once I can express what I want in the language of extreme ``invalid states
unrepresentable'' types, LLM agents no longer feel like agents of chaotic
spaghetti extruding unmaintainable code. Instead, it feels like\ldots seeding a
crystal and watching it grow into a beautiful, shimmering lattice. It feels like
the language they yearn to speak. And the more expressive your types, the more
beautiful the crystalline structure in the end.

Honestly, humans might have problems writing and using this code, but LLMs
definitely don't, if properly scaffolded! Since early 2026, at least, for me.
We'll explore a bit more about this once we have more to work with in Part 2.

\section{Special Thanks}\label{special-thanks}

I am very humbled to be supported by an amazing community, who make it possible
for me to devote time to researching and writing these posts. Very special
thanks to my supporter at the ``Amazing'' level on
\href{https://www.patreon.com/justinle/overview}{patreon}, Josh Vera! :)

\section{Signoff}\label{signoff}

Hi, thanks for reading! You can reach me via email at
\href{mailto:justin@jle.im}{\nolinkurl{justin@jle.im}}, or at twitter at
\href{https://twitter.com/mstk}{@mstk}! This post and all others are published
under the \href{https://creativecommons.org/licenses/by-nc-nd/3.0/}{CC-BY-NC-ND
3.0} license. Corrections and edits via pull request are welcome and encouraged
at \href{https://github.com/mstksg/inCode}{the source repository}.

If you feel inclined, or this post was particularly helpful for you, why not
consider \href{https://www.patreon.com/justinle/overview}{supporting me on
Patreon}, or a \href{bitcoin:3D7rmAYgbDnp4gp4rf22THsGt74fNucPDU}{BTC donation}?
:)

\textbackslash end\{document\}

\end{document}
