paper.tex

% chktex-file 1
% chktex-file 26
% chktex-file 35
\documentclass[11pt]{article}
\usepackage[ligature,reserved]{semantic}
\usepackage[utf8]{inputenc}
\usepackage[american]{babel}
\usepackage{csquotes}
\usepackage[dvipsnames]{xcolor}
\usepackage{hyperref}
\usepackage{hyphenat}
\usepackage{amsfonts}
\usepackage{amsmath} \allowdisplaybreaks
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage[margin=1.25in,letterpaper]{geometry}
\usepackage{mathtools}
\usepackage{mathpartir}
\usepackage{scalerel}
\usepackage{stackengine}

\usepackage[
    backend=biber,
    style=apa,
]{biblatex}

\addbibresource{biblio.bib}

\hypersetup{
    colorlinks=true,
    linkcolor=blue,
    filecolor=magenta,
    urlcolor=cyan,
    citecolor=Green,
    pdfpagemode=FullScreen,
}


% thanks goes to einargs for creating this setup (BNF, \typerule, \typeaxiom)
% (rest is my hacky LaTeX)
% Syntax group
\newcommand{\syng}[2]{#1 \bnf& & \text{#2} \\}
% Line in a syntax group
\newcommand{\syn}[2]{& #1 & \text{#2} \\}
\newcommand{\bnf}{\mathrel{::=}\;}

\newcommand{\tchk}{\Leftarrow}
\newcommand{\tsyn}{\Rightarrow}
\newcommand{\rarr}{\rightarrow}

% found on tex.SE, tortured into compliance
\newlength\arrowheight
\newcommand\doubleRightarrow{
  \mathrel{\ThisStyle{
    \setlength{\arrowheight}{\heightof{$\SavedStyle\Downarrow$}}
    \scalerel*{\rotatebox{90}{\stackengine{.5\arrowheight}{$\SavedStyle\Downarrow$}
      {$\SavedStyle\Downarrow$}{O}{c}{F}{F}{L}}}{\rotatebox[origin=c]{90}{$\Downarrow$}}}
}}

% function & applicand type notation
% stolen from Dunfield 2013
\newcommand{\tapp}[3]{
    #1 \bullet #2 \doubleRightarrow #3
}

\newcommand{\alphahat}{\hat{\alpha}}
\newcommand{\betahat}{\hat{\beta}}

\newcommand{\tprod}[1]{\{#1\}}
\newcommand{\tsum}[1]{\langle#1\rangle}
\newcommand{\ttauibar}{\overline{\tau_i}}
\newcommand{\tall}[3]{\forall (#1 :: #2).#3}
\newcommand{\tlam}[3]{\lambda (#1 :: #2).#3}

\newcommand{\eeibar}{\overline{e_i}}
\newcommand{\ecase}[2]{\<case>\ #1\ \<of>\ #2}

\newcommand{\Nf}{^{\textsf{Nf}}}
\newcommand{\Ne}{^{\textsf{Ne}}}

\newcommand{\typerule}[3]{
    \inferrule{#2}{#3}\quad(\textsf{#1})
}

\newcommand{\typeaxiom}[2]{
    \inferrule{ }{#2}\quad(\textsf{#1})
}

\reservestyle{\literal}{\texttt}
\reservestyle{\keyword}{\textbf}
\literal{true, false, bool, int, cond, fix, mod, and, or, not, project, embed, eq, neq}
\keyword{case, of}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[theorem]
\newtheorem{lemma}[theorem]{Lemma}

\title{Tethys\\
    \large A Toy Functional Programming Language\\
    with a System F$\omega$-based Core Calculus\\
    \url{https://github.com/ThePuzzlemaker/tethys}}
\author{James [Redacted] (aka ThePuzzlemaker)}
\date{\today}

\begin{document}

\maketitle

\tableofcontents
\newpage

\section{Introduction}

This ``paper'' (which is really just a well-typeset, but somewhat informal
    write-up) introduces Tethys, a toy functional programming language based on
    a System F$\omega$-based core calculus. Hence the title.

There are two parts of Tethys: the surface language, and the core calculus. The
    core calculus is the intermediate representation of Tethys which is used
    for type checking and inference, and for interpretation. The surface
    language is the higher-level interface that is eventually desugared by the
    compiler/interpreter to the core calculus.

The reference implementation in Rust will not use any particular ``tricks'' in
    terms of interpretation, instead just using a simple tree-walk interpreter
    or similar.

This language was created in order to conduct informal research (i.e., not
    actually discovering anything interesting, probably) on type systems,
    especially bidirectional typechecking and polymorphism. Tethys is named as
    such as it is the name of the co-orbital moon to Calypso; as my work on
    this language is ``co-orbital'', so to speak, to my work on
    \href{https://calypso-lang.github.io}{Calypso}.

Please note that I am not an expert in pretty much any subject this writeup
    covers. If you notice something you don't understand, or that you think is
    a mistake, don't fret to point it out.

\subsection{Background}

\begin{quote}
    Note: This section is taken from
        \href{https://thepuzzlemaker.info/static/tethys-slides/}{some slides I
        prepared for a lightning talk} in the
        \href{https://discord.gg/26X6ChQQcG}{r/PL Discord server}. If it seems
        a bit un-prose-y, that's why.
\end{quote}

Originally, I thought I needed to use System F$\omega$, an extension of the
    polymorphic typed lambda calculus (System F), with the extension of type
    lambdas. However, it has some problems:

\begin{itemize}
    \item System F is already undecidable enough, with respect to inference.
        Adding \emph{more} types of types does \textbf{not} help.
    \item Theoretically, bidirectional typechecking (my chosen strategy)
        doesn't \emph{need} unification, but it sure makes it nice. And having
        type lambdas means you need higher order unfication, which is scary
        because anything including ``higher-order'' in its name is automatically
        scary. Also it's undecidable, so you have to restrict yourself to
        higher-order pattern unification, which is still quite scary.
    \item I just can't really find much good introductory literature on
        System F$\omega$ (at least, literature that I can understand).
\end{itemize}

As it turns out, System F$\omega$ is more expressive than F, but \textbf{way}
    much more of a pain. Not even Haskell, the paragon of kitchen sink type
    system features has it. (By default, because of course GHC's gonna have it
    as an extension).

Here are some of the key theoretical differences:

\begin{itemize}
    \item Within the type system, type constructors are opaque. Defining a type
        just creates opaque term-level and type-level constants, which don't
        normalize to the type or term they ``really'' mean. Of course, these
        are stripped out after typechecking, once they're no longer needed.
    \item Type constructors are injective, i.e. for some type constructor $C$
        and types $X$ and $Y$, if $C\;X$ and $C\;Y$ are the same type, then $X$
        and $Y$ are the same type.
    \item Differently named type constructors are never equal, even if they
        ``mean'' the same thing, i.e. for some type constructors $C1$ and $C2$,
        and type $T$, $C1\;T$ never equals $C2\;T$, no matter how they are
        defined.
\end{itemize}

Note that this is pretty much nominal typing! (If my understanding of nominal
    typing is correct.)


\section{The Surface Language}

This section has not been started yet.

\section{The Declarative Core Calculus}

This section is, unsurprisingly, work-in-progress.

\section{References}

\subsection{Acknowledements}

Thanks to Brendan Zabarauskas and András Kovács, who have helped with many type
    system details. Many thanks to Mark Barbone (aka MBones/mb64), who provided
    a code sample of their bidirectionally typed (with unification) algorithm
    for typechecking higher-rank System F (\cite{tychk-nbe}), and who also
    noted some issues they had with \citetitle{Dunfield13:bidir}
    (\cite{Dunfield13:bidir}).


\subsection{References}

\nocite{*}

\printbibliography[heading=none]

\end{document}