commit e6e538c3ed42512108d344dfc20d6c5998cbc5fd
parent b3e5a1b5cf7f2da6a31e7b57333f20514179c59e
Author: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 20 Oct 2015 18:06:59 -0400
[overload] doc'd the problem with lambda, gosh I miss let
Diffstat:
2 files changed, 20 insertions(+), 0 deletions(-)
diff --git a/tapl/design/Makefile b/tapl/design/Makefile
@@ -0,0 +1,2 @@
+coconut-creme-pie:
+ xelatex overload
diff --git a/tapl/design/overload.tex b/tapl/design/overload.tex
@@ -108,6 +108,23 @@ Applying a $\psi$-value triggers a series of predicate checks on its argument; i
\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}
@@ -121,4 +138,5 @@ We could also do $\kres$ as a metafunction, but this was language users can spec
\item Work out interactions with $<:$ and $\forall$
\end{itemize}
+
\end{document}
