From 51e6e1b3ae750e8a8df7dc058b010bb5661c0b7e Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Thu, 22 Oct 2015 17:07:05 -0400 Subject: [PATCH] [overload] remove design/ folder --- tapl/design/.gitignore | 6 -- tapl/design/Makefile | 2 - tapl/design/def.tex | 8 --- tapl/design/overload.tex | 142 --------------------------------------- 4 files changed, 158 deletions(-) delete mode 100644 tapl/design/.gitignore delete mode 100644 tapl/design/Makefile delete mode 100644 tapl/design/def.tex delete mode 100644 tapl/design/overload.tex diff --git a/tapl/design/.gitignore b/tapl/design/.gitignore deleted file mode 100644 index d316dca..0000000 --- a/tapl/design/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -*\.aux -*\.bbl -*\.log -*\.out -*\.pdf -mathpartir\.sty diff --git a/tapl/design/Makefile b/tapl/design/Makefile deleted file mode 100644 index 4805261..0000000 --- a/tapl/design/Makefile +++ /dev/null @@ -1,2 +0,0 @@ -coconut-creme-pie: - xelatex overload diff --git a/tapl/design/def.tex b/tapl/design/def.tex deleted file mode 100644 index 2d24cba..0000000 --- a/tapl/design/def.tex +++ /dev/null @@ -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 deleted file mode 100644 index 2c85da5..0000000 --- a/tapl/design/overload.tex +++ /dev/null @@ -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}