commit 51e6e1b3ae750e8a8df7dc058b010bb5661c0b7e
parent e038d220f10841c795300455b23e33748949f733
Author: Ben Greenman <types@ccs.neu.edu>
Date: Thu, 22 Oct 2015 17:07:05 -0400
[overload] remove design/ folder
Diffstat:
4 files changed, 0 insertions(+), 158 deletions(-)
diff --git a/tapl/design/.gitignore b/tapl/design/.gitignore
@@ -1,6 +0,0 @@
-*\.aux
-*\.bbl
-*\.log
-*\.out
-*\.pdf
-mathpartir\.sty
diff --git a/tapl/design/Makefile b/tapl/design/Makefile
@@ -1,2 +0,0 @@
-coconut-creme-pie:
- xelatex overload
diff --git a/tapl/design/def.tex b/tapl/design/def.tex
@@ -1,8 +0,0 @@
-\usepackage{mathpartir}
-\usepackage{palatino}
-
-\newcommand{\fmt}[1]{\mathsf{#1}}
-\newcommand{\ksig}{\fmt{signature}}
-\newcommand{\kinst}{\fmt{instance}}
-\newcommand{\kres}{\fmt{resolve}}
-\newcommand{\kpsi}[3]{\psi~(#1)~#2~#3}
diff --git a/tapl/design/overload.tex b/tapl/design/overload.tex
@@ -1,142 +0,0 @@
-\documentclass{article}
-\input{def}
-\begin{document}
-
-\section*{Parametric Overloading}
-
-\subsection*{Definition}
-\begin{itemize}
-\item Identifiers may be parametrically overloaded.
-\item Overloaded identifiers have no implementation and a type containing holes.
-\item Implementations may be \emph{later} associated with the identifier by filling the type holes.
-\item On use, the identifier infers from its context which instance to use.
- Instances are keyed by type: the type filling the hole.
-\end{itemize}
-
-Goal: provide a clean implementation.
-
-\subsection*{Old Ideas}
-\subsubsection*{Global Table}
-\begin{itemize}
-\item Keep a global mapping $\Sigma$ from identifiers to types to implementations.
-\item Query and extend this map during typechecking.
-\end{itemize}
-
-Problem: global state like this is anti-modular.
-Unclear how to extend to a multi-module or sub-module world.
-There's only a global scope.
-
-\subsubsection*{Dynamic Binding \& Parameters}
-\begin{itemize}
-\item Each overloaded identifier represented as a new \emph{parameter}
-\item The parameter is a lookup procedure; using the ID should trigger a type-directed lookup.
- Somehow.
-\item New instances extend the lookup procedure in the parameter.
-\end{itemize}
-
-Parameters are a nice mix of lexical scope and imperatives.
-Also they are reasonable to share across modules.
-
-The lookup is a little troublesome, but the compile-time elaboration should be able to call the parameter with the right type arguments.
-
-
-\newpage
-\subsection*{Current Idea: first class overloadables}
-We'll represent overloadable signatures with a new type constructor, $\psi$, which makes the updating explicit.
-
-The $\psi$ types have the form
-$$\kpsi{\alpha}{\Sigma}{\tau}$$
-where:
-\begin{itemize}
-\item $\alpha$ is a type variable
-\item $\Sigma$ is a partial map from types to expressions.
- It is a lookup table: given a concrete type $\tau'$ to swap for the variable $\alpha$, the map $\Sigma$ returns an expression with type $\tau[\alpha/\tau']$.
-\item $\tau$ is a type where $\alpha$ is definitely free
-\end{itemize}
-
-For now, we constrain $\tau$ to be a function $\alpha \rightarrow \tau'$ for some base type $\tau'$.
-
-In the following rules, we identify $\Sigma$ with its set of keys.
-These keys are the carrier set for the algebra of types at which we can instantiate the $\psi$ type.
-%% TODO explain the carrier a little better
-
-At runtime, all values of $\psi$ type are dictionaries that perform type dispatch.
-Applying a $\psi$-value triggers a series of predicate checks on its argument; if successful, this leads to a function application.
-
-\begin{mathpar}
- \inferrule*[left=O-Sig]{
- \alpha\ \mbox{free in}\ \tau
- \\\\
- \mbox{(for now, $\tau = \alpha \rightarrow \tau'$)}
- \\\\
- \Sigma = \emptyset
- }{
- \vdash \ksig\ \alpha\ \tau : \kpsi{\alpha}{\Sigma}{\tau} \Rightarrow \Sigma
- }
-
- \inferrule*[left=O-Inst]{
- \vdash x : \kpsi{\alpha}{\Sigma}{\tau'}
- \\\\
- \tau \not\in \Sigma
- \\\\
- \vdash e : \tau'[\alpha/\tau]
- }{
- \vdash \kinst\ x\ \tau\ e : \kpsi{\alpha}{(\Sigma \cup \{\tau\})}{\tau'}
- \Rightarrow (\mathsf{set!}\ \Sigma\ ???)
- }
-
- \inferrule*[left=O-App]{
- \vdash e : \tau
- \\
- \vdash (\kres\ x\ \tau)~e : \tau'' \Rightarrow v
- }{
- \vdash x~e : \tau''
- \Rightarrow v
- }
-
- \inferrule*[left=O-Res]{
- \vdash x : \kpsi{\alpha}{\Sigma}{(\alpha \rightarrow \tau'')}
- \\
- (\tau, e) \in \Sigma
- \\
- \vdash e : \tau \rightarrow \tau'' \Rightarrow v
- }{
- \vdash \kres\ x\ \tau : \tau \rightarrow \tau'
- \Rightarrow v
- }
-
-\end{mathpar}
-We could also do $\kres$ as a metafunction, but this was language users can specify exactly how to resolve their overloaded functions.
-
-\subsection*{Problem!}
-Oh wow, I didn't think about $\lambda$ being a problem.
-We have types-depending-on-values, but I didn't see any issue because we know everything about these values statically.
-Not quite!
-$$(\lambda\,(x : \kpsi{\alpha}{\Sigma}{\tau})\,.\,(x~1))~(\kinst~(\ksig~(\alpha)~\tau)~\tau'~e)$$
-What's the type of $x$ inside the body?
-We know from ``$\Sigma$'' what keys it has, but the overloading-resolver is OUTSIDE the $\lambda$.
-
-Ideas to fix:
-\begin{itemize}
-\item Give up. Only do run-time instance resolution. HAH.
-\item Give up. Fall back to parameter-style or global-table-style. HM.
-\item Do some best-effort static analysis to push the type outside the lambda inside it.
- This could be combined with type inference on the $\lambda$ signature\textemdash we really don't care the exact type of $x$ (i.e. its entire carrier), only that it can be applied to integers.
-\end{itemize}
-
-
-
-\subsection*{Next Steps}
-\begin{itemize}
-\item Implement with simple types
-\item Implement with recursive types like nested products and lists
-\item Combine with occurrence typing
-\item Extend to multiple variables, $(\alpha^* \ldots)$
-\item Extend to overloaded codomains
-\item Extend to other overloadables, not just functions
-\item Allow bound polymorphism over signatures with at least some instances
-\item Work out interactions with $<:$ and $\forall$
-\end{itemize}
-
-
-\end{document}
