From e9cefe3298be30c81faab1de5a209fdbc7623ad1 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Mon, 19 Oct 2015 20:44:39 -0400
Subject: [PATCH 1/9] [overload] design doc for \psi types

---
 tapl/design/.gitignore   |   6 ++
 tapl/design/def.tex      |   8 +++
 tapl/design/overload.tex | 116 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 130 insertions(+)
 create mode 100644 tapl/design/.gitignore
 create mode 100644 tapl/design/def.tex
 create mode 100644 tapl/design/overload.tex

diff --git a/tapl/design/.gitignore b/tapl/design/.gitignore
new file mode 100644
index 0000000..d316dca
--- /dev/null
+++ b/tapl/design/.gitignore
@@ -0,0 +1,6 @@
+*\.aux
+*\.bbl
+*\.log
+*\.out
+*\.pdf
+mathpartir\.sty
diff --git a/tapl/design/def.tex b/tapl/design/def.tex
new file mode 100644
index 0000000..2d24cba
--- /dev/null
+++ b/tapl/design/def.tex
@@ -0,0 +1,8 @@
+\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
new file mode 100644
index 0000000..c94faa2
--- /dev/null
+++ b/tapl/design/overload.tex
@@ -0,0 +1,116 @@
+\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
+
+\begin{mathpar}
+  \inferrule*[left=O-Sig]{
+    \alpha\ \mbox{free in}\ \tau
+    \\\\
+    \mbox{(for now, $\tau = \alpha \rightarrow \tau'$)}
+  }{
+    \vdash \ksig\ \alpha\ \tau : \kpsi{\alpha}{\emptyset}{\tau}
+  }
+
+  \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'}
+  }
+
+  \inferrule*[left=O-App]{
+    \vdash e : \tau
+    \\
+    \vdash (\kres\ x\ \tau)~e : \tau''
+  }{
+    \vdash x~e : \tau''
+  }
+
+  \inferrule*[left=O-Res]{
+    \vdash x : \kpsi{\alpha}{\Sigma}{(\alpha \rightarrow \tau'')}
+    \\
+    (\tau, e) \in \Sigma
+    \\
+    \vdash e : \tau \rightarrow \tau''
+  }{
+    \vdash \kres\ x\ \tau : \tau \rightarrow \tau'
+  }
+
+\end{mathpar}
+Maybe, $\kres$ should be a metafunction.
+
+
+\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}

From f228ace20f75d2bc52120bd405ccadc69cc03b6f Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 20 Oct 2015 00:49:23 -0400
Subject: [PATCH 2/9] [overload] outline tests

---
 tapl/tests/stlc+overloading-tests.rkt | 52 +++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 tapl/tests/stlc+overloading-tests.rkt

diff --git a/tapl/tests/stlc+overloading-tests.rkt b/tapl/tests/stlc+overloading-tests.rkt
new file mode 100644
index 0000000..217254c
--- /dev/null
+++ b/tapl/tests/stlc+overloading-tests.rkt
@@ -0,0 +1,52 @@
+#lang s-exp "../stlc+overloading.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; -----------------------------------------------------------------------------
+;; --- syntax for ψ types
+
+(typecheck-fail
+ (signature (α) (→ α Str Str))
+ #:with-msg "We only support single-argument functions")
+
+(typecheck-fail
+ (signature (α) (→ Str Str))
+ #:with-msg "Variable 'α' must be free")
+
+(check-type
+ (signature (α) (→ α Str))
+ : (ψ (α) (→ α Str)))
+
+;; -----------------------------------------------------------------------------
+;; --- basic overloading
+
+;; -- creating a signature does nothing, at first
+;; (signature (to-string α) (→ α Str))
+
+;; (typecheck-fail
+;;  (to-string 1)
+;;  #:with-msg "no instance")
+
+;; (typecheck-fail
+;;  (to-string "yolo")
+;;  #:with-msg "no instance")
+
+;; ;; -- can later add cases to an overloaded name
+;; (instance (to-string Num)
+;;   (λ ([x : Num]) "num"))
+
+;; (instance (to-string Str)
+;;   (λ ([x : Str]) "string"))
+
+;; (check-type-and-result
+;;  (to-string 43)
+;;  : Str ⇒ "num")
+
+;; (check-type-and-result
+;;  (to-string (+ 2 2))
+;;  : Str ⇒ "num")
+
+;; (check-type-and-result
+;;  (to-string "hi")
+;;  : Str ⇒ "string")
+
+;; ;; -- 

From 3cbafd377228c7995de9173d4434e9ce103176f2 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 20 Oct 2015 00:49:55 -0400
Subject: [PATCH 3/9] [overload] got \psi-types and signature init

---
 tapl/stlc+overloading.rkt | 123 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 tapl/stlc+overloading.rkt

diff --git a/tapl/stlc+overloading.rkt b/tapl/stlc+overloading.rkt
new file mode 100644
index 0000000..ec00b9e
--- /dev/null
+++ b/tapl/stlc+overloading.rkt
@@ -0,0 +1,123 @@
+#lang s-exp "typecheck.rkt"
+(extends "stlc+sub.rkt" #:except #%datum); #:rename [#%app stlc:#%app])
+(reuse #:from "stlc+rec-iso.rkt") ; load current-type=?
+;(extends "stlc+tup.rkt" #:except + #%datum and)
+;(extends "stlc+cons.rkt" #:except + #%datum and)
+
+;; Parametric overloading.
+;; - define overloadable functions with "template" types
+;; - later, add implementations
+;; -- typecheck the impl
+;; -- save in a table
+;; - for app, lookup the overloaded ID
+;; - allow higher-order positions
+
+;; Implementation strategy
+;; - make explicit type for overloadables
+;;   showing the __free variables__ and __instance carrier__
+;; - new instances update the carrier
+;; - lookups query the type; the type contains the lookup table
+
+;; =============================================================================
+
+(define-base-type Bot)
+(define-base-type Str)
+
+(define-typed-syntax #%datum
+  [(_ . n:str) (⊢ (#%datum . n) : Str)]
+  [(_ . x) #'(stlc+sub:#%datum . x)])
+
+;; =============================================================================
+;; === ψ types
+
+;; TODO make it arity 2
+(define-type-constructor ψ #:arity = 1 #:bvs = 1)
+
+(begin-for-syntax
+ (define ψ-eval
+   (let ([τ-eval (current-type-eval)])
+     (lambda (τ-stx)
+       (define τ+ (τ-eval τ-stx))
+       (syntax-parse τ+
+        [(~ψ (α) τ)
+         ;; TODO ?
+         τ+]
+        [_ τ+]))))
+ (current-type-eval ψ-eval)
+
+ ;; TODO my types are unequal. How does equality for ∀ types work?
+ ;; (define ψ=?
+)
+
+;; =============================================================================
+;; === Signature maps
+;; Covert a type to an implementation. Use current-type-eval to normalize keys
+
+(begin-for-syntax 
+
+ (define (Σ-print Σ port mode)
+   (define (print-k+v k+v)
+     (display (syntax->datum (car k+v)) port))
+   (display "{" port)
+   (define k+v* (Σ-map Σ))
+   (when (not (null? k+v*))
+     (print-k+v (car k+v*))
+     (for ([k+v (in-list k+v*)])
+       (display " " port)
+       (print-k+v k+v)))
+   (display "}" port))
+
+ (struct Σ (
+   map ;; (Listof (Pairof τ* expr)), maps types to implementations
+ ) #:property prop:procedure
+   (lambda (self arg)
+     (error 'Σ "Cannot apply struct, don't yet know how to turn types into predicates"))
+   #:methods gen:custom-write
+   [(define write-proc Σ-print)])
+ 
+ (define Σ-empty
+   (Σ '()))
+
+ (define (Σ-key* Σ)
+   (map car (Σ-map Σ)))
+)
+
+;; =============================================================================
+
+(begin-for-syntax
+ (define-syntax-rule (signature-error τ reason)
+   (error 'signature (format "Cannot define overloadable signature for at type '~a'. ~a"
+                             (syntax->datum τ) reason)))
+)
+
+(define-typed-syntax signature
+  [(_ (α:id) τ)
+   ;; Expand the type τ with α bound as a valid type
+   #:with ((α+) τ+ _) (infer/tyctx+erase #'([α : #%type]) #'τ)
+   ;; Make sure τ is (→ α τ') for some real type τ'
+   #:when (syntax-parse #'τ+
+           [(~→ τ-dom τ-cod)
+            ;; τ-dom MUST be the (expanded) identifier α+
+            (unless (and (identifier? #'τ-dom)
+                         (free-identifier=? #'τ-dom #'α+))
+              (signature-error #'τ
+                               (format "Variable '~a' must be free in the signature type." (syntax->datum #'α))))]
+           [_
+            (signature-error #'τ "We only support single-argument functions with overloaded domains.")])
+   ;; Using define to ensure top-level use
+   ;; (define k* (assign-type #'() #'#%type))
+   (⊢ #,Σ-empty
+      : (ψ (α) τ))]) ;; TODO add Σ-keys to the type?
+
+#;(define-typed-syntax #%app
+  [(_ e_fn e_arg)
+   #:with [e_fn+ τ_fn] (infers+erase #'e_fn)
+   #:when (ψ? #'τ_fn)
+   #:when (error 'APP (format "YOLO e = ~a arg = ~a τ = ~a"
+                              (syntax->datum #'e_fn)
+                              (syntax->datum #'e_arg)
+                              (syntax->datum #'τ_fn)))
+   #'(void)
+   ]
+  [(_ e* ...)
+   #'(stlc:#%app e* ...)])

From b3e5a1b5cf7f2da6a31e7b57333f20514179c59e Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 20 Oct 2015 16:42:13 -0400
Subject: [PATCH 4/9] [overload] add run-time desugar to design doc

---
 tapl/design/overload.tex | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/tapl/design/overload.tex b/tapl/design/overload.tex
index c94faa2..b481e5f 100644
--- a/tapl/design/overload.tex
+++ b/tapl/design/overload.tex
@@ -60,13 +60,18 @@ 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}{\emptyset}{\tau}
+    \vdash \ksig\ \alpha\ \tau : \kpsi{\alpha}{\Sigma}{\tau} \Rightarrow \Sigma
   }
 
   \inferrule*[left=O-Inst]{
@@ -77,14 +82,16 @@ These keys are the carrier set for the algebra of types at which we can instanti
     \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''
+    \vdash (\kres\ x\ \tau)~e : \tau'' \Rightarrow v
   }{
     \vdash x~e : \tau''
+    \Rightarrow v
   }
 
   \inferrule*[left=O-Res]{
@@ -92,13 +99,14 @@ These keys are the carrier set for the algebra of types at which we can instanti
     \\
     (\tau, e) \in \Sigma
     \\
-    \vdash e : \tau \rightarrow \tau''
+    \vdash e : \tau \rightarrow \tau'' \Rightarrow v
   }{
     \vdash \kres\ x\ \tau : \tau \rightarrow \tau'
+    \Rightarrow v
   }
 
 \end{mathpar}
-Maybe, $\kres$ should be a metafunction.
+We could also do $\kres$ as a metafunction, but this was language users can specify exactly how to resolve their overloaded functions.
 
 
 \subsection*{Next Steps}

From e6e538c3ed42512108d344dfc20d6c5998cbc5fd Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Tue, 20 Oct 2015 18:06:59 -0400
Subject: [PATCH 5/9] [overload] doc'd the problem with lambda, gosh I miss let

---
 tapl/design/Makefile     |  2 ++
 tapl/design/overload.tex | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 tapl/design/Makefile

diff --git a/tapl/design/Makefile b/tapl/design/Makefile
new file mode 100644
index 0000000..4805261
--- /dev/null
+++ 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
index b481e5f..2c85da5 100644
--- 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}

From 0b587697f4b943b3d485d3fd5de65b8190aaf871 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Wed, 21 Oct 2015 00:47:21 -0400
Subject: [PATCH 6/9] [overloading] initial revision, overloading via parameter

---
 tapl/stlc+overloading-param.rkt             | 163 ++++++++++++++++++++
 tapl/stlc+overloading.rkt                   | 123 ---------------
 tapl/tests/stlc+overloading-param-tests.rkt |  96 ++++++++++++
 tapl/tests/stlc+overloading-tests.rkt       |  52 -------
 4 files changed, 259 insertions(+), 175 deletions(-)
 create mode 100644 tapl/stlc+overloading-param.rkt
 delete mode 100644 tapl/stlc+overloading.rkt
 create mode 100644 tapl/tests/stlc+overloading-param-tests.rkt
 delete mode 100644 tapl/tests/stlc+overloading-tests.rkt

diff --git a/tapl/stlc+overloading-param.rkt b/tapl/stlc+overloading-param.rkt
new file mode 100644
index 0000000..15f3fb8
--- /dev/null
+++ b/tapl/stlc+overloading-param.rkt
@@ -0,0 +1,163 @@
+#lang s-exp "typecheck.rkt"
+(reuse List cons nil #:from "stlc+cons.rkt")
+(extends "stlc+sub.rkt" #:except #%datum #:rename [#%app stlc:#%app])
+(reuse #:from "stlc+rec-iso.rkt") ; load current-type=?
+
+;; Apparently cannot propogate type information across statements.
+;; Until the first-class ones work, let's do the big dumb parameter
+
+;; So here's what going to happen
+;; - current-Σ will be a map from identifiers to resolvers
+;; - resolvers will map overloaded signatures and types to concrete instances
+;; - extending a resolver (via instance) will add a new (τ, e) pair to a mutable list
+
+;; =============================================================================
+
+(define-base-type Bot)
+(define-base-type Str)
+
+(define-typed-syntax #%datum
+  [(_ . n:str) (⊢ (#%datum . n) : Str)]
+  [(_ . x) #'(stlc+sub:#%datum . x)])
+
+(define-for-syntax xerox syntax->datum)
+
+;; =============================================================================
+;; === Resolvers
+
+(begin-for-syntax
+ (struct ℜ (
+   name ;; Symbol
+   dom* ;; (Box (Listof (Pairof Type Expr)))
+   cod  ;; Type
+ ) #:transparent
+   #:property prop:procedure
+   (lambda (self τ-or-e)
+     (define r
+       (if (syntax? τ-or-e) ;; Can I ask "type?"
+           (ℜ-resolve-syntax self τ-or-e)
+           (ℜ-resolve-value  self τ-or-e)))
+     (or r
+         (error 'ℜ (format "Resolution for '~a' failed at type ~a"
+                           (syntax->datum (ℜ-name self))
+                           τ-or-e))))
+ )
+
+ ;; Rad!
+ (define (ℜ-add! ℜ τ e)
+   (define dom* (ℜ-dom* ℜ))
+   (set-box! dom* (cons (cons τ e) (unbox dom*))))
+
+ (define (ℜ-init name τ-cod)
+   (ℜ name (box '()) τ-cod))
+
+ (define (ℜ->type ℜ)
+   ((current-type-eval) #`(→ #,(assign-type #''α #'#%type) #,(ℜ-cod ℜ))))
+
+ (define (ℜ-find ℜ τ)
+   (define τ=?
+     (let ([type=? (current-type=?)])
+       (lambda (τ2)
+         (type=? τ τ2))))
+   (assf τ=? (unbox (ℜ-dom* ℜ))))
+
+ (define (ℜ-resolve-syntax ℜ τ)
+   (define result (ℜ-find ℜ τ))
+   (and (pair? result)
+        (cdr result)))
+
+ (define (ℜ-resolve-value ℜ e)
+   (error 'ℜ (format "Runtime resolution not implemented. Anyway your value was ~a" e)))
+
+ (define (ℜ-unbound? ℜ τ)
+   (not (ℜ-find ℜ τ)))
+ 
+)
+
+;; =============================================================================
+;; === Overloaded signature environment
+
+(begin-for-syntax
+ (define current-Σ (make-parameter (lambda (id) #f)))
+)
+
+(define-typed-syntax signature
+  [(_ (name:id α:id) τ)
+   #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ)
+   (let ([ℜ-old ((current-Σ) #'name)])
+     (when ℜ-old
+       (error 'signature (format "Identifier '~a' already bound to a type ~a"
+                                 (syntax->datum #'name) (syntax->datum (ℜ->type ℜ-old))))))
+   (define ℜ (ℜ-init #'name #'τ-cod))
+   (current-Σ 
+    (let ([old-Σ (current-Σ)])
+      (lambda (id)
+        (if (free-identifier=? id #'name)
+            ℜ
+            (old-Σ id)))))
+   (⊢ (define name #,ℜ)
+      : Bot)]
+  [(_ e* ...)
+   (error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))])
+
+;; TODO make this available to users
+(define-for-syntax (resolve stx)
+  (syntax-parse stx
+   [(name:id τ)
+    #:with [name+ τ_fn+] (infer+erase #'name)
+    #:with τ+ ((current-type-eval) #'τ)
+    (define ℜ ((current-Σ) #'name+))
+    (unless ℜ
+      (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum #'name+))))
+    (ℜ #'τ)]))
+
+(define-typed-syntax #%app
+  [(_ e_fn:id e_arg)
+   #:with [e_fn+ τ_fn+] (infer+erase #'e_fn)
+   ;; Beware 3D syntax
+   #:when ((current-Σ) #'e_fn+)
+   #:with [e_arg+ τ_arg+] (infer+erase #'e_arg)
+   (unless (syntax-e #'τ_arg+)
+     (error '#%app "No type for expression ~a\n" (syntax->datum #'e_arg)))
+   (define fn (resolve #'(e_fn+ τ_arg+)))
+   #`(#%app #,fn e_arg+)]
+  [(_ e* ...)
+   #'(stlc:#%app e* ...)])
+
+(begin-for-syntax
+(define-syntax-rule (instance-error id τ r)
+  (error 'instance (format "Cannot make instance for '~a' at type '~a'. ~a"
+                           (syntax->datum id) (syntax->datum τ) r)))
+)
+
+(define-typed-syntax instance
+  [(_ (name:id τ-stx) e)
+   #:with τ ((current-type-eval) #'τ-stx)
+   #:with [e+ τ+] (infer+erase #'e)
+   (define ℜ ((current-Σ) #'name))
+   (unless ℜ (instance-error #'name #'τ "Not an overloaded identifier."))
+   (unless (ℜ-unbound? ℜ #'τ) (instance-error #'name #'τ "Overlaps with existing instance."))
+   (define does-this-id-matter?
+     (syntax-parse #`(τ+ #,(ℜ->type ℜ))
+      [((~→ τ_dom1 τ_cod1)
+        (~→ _      τ_cod2))
+       ;; Really, need to unify this type with the template
+       ;; (unless ((current-type=?) τ_dom1 τ_dom2)
+       ;;   (instance-error #'name #'τ (format "Domain '~a' must unify with template domain '~a'."
+       ;;                                      (syntax->datum #'τ_dom1) (syntax->datum #'τ_dom2))))
+       (unless ((current-type=?) ((current-type-eval) #'τ) #'τ_dom1)
+         (instance-error #'name #'τ (format "Domain '~a' must be the instance type, for now (2015-10-20)." (syntax->datum #'τ_dom1))))
+       (unless ((current-type=?) #'τ_cod1 #'τ_cod2)
+         (instance-error #'name #'τ (format "Codomain '~a' must match template codomain '~a'"
+                                            (syntax->datum #'τ_cod1) (syntax->datum #'τ_cod2))))
+       (void)]
+      [(a b)
+       (instance-error #'name #'τ (format "May only overload single-argument functions. (Got ~a and ~a)"
+                                          (syntax->datum #'a) (syntax->datum #'b))
+                                          )]))
+   (ℜ-add! ℜ #'τ #'e+) ;; Should we use syntax instead of e+ ?
+   (⊢ (void) : Bot)]
+  [_
+   (error 'instance "Expected (instance (id τ) e).")])
+       
+   
diff --git a/tapl/stlc+overloading.rkt b/tapl/stlc+overloading.rkt
deleted file mode 100644
index ec00b9e..0000000
--- a/tapl/stlc+overloading.rkt
+++ /dev/null
@@ -1,123 +0,0 @@
-#lang s-exp "typecheck.rkt"
-(extends "stlc+sub.rkt" #:except #%datum); #:rename [#%app stlc:#%app])
-(reuse #:from "stlc+rec-iso.rkt") ; load current-type=?
-;(extends "stlc+tup.rkt" #:except + #%datum and)
-;(extends "stlc+cons.rkt" #:except + #%datum and)
-
-;; Parametric overloading.
-;; - define overloadable functions with "template" types
-;; - later, add implementations
-;; -- typecheck the impl
-;; -- save in a table
-;; - for app, lookup the overloaded ID
-;; - allow higher-order positions
-
-;; Implementation strategy
-;; - make explicit type for overloadables
-;;   showing the __free variables__ and __instance carrier__
-;; - new instances update the carrier
-;; - lookups query the type; the type contains the lookup table
-
-;; =============================================================================
-
-(define-base-type Bot)
-(define-base-type Str)
-
-(define-typed-syntax #%datum
-  [(_ . n:str) (⊢ (#%datum . n) : Str)]
-  [(_ . x) #'(stlc+sub:#%datum . x)])
-
-;; =============================================================================
-;; === ψ types
-
-;; TODO make it arity 2
-(define-type-constructor ψ #:arity = 1 #:bvs = 1)
-
-(begin-for-syntax
- (define ψ-eval
-   (let ([τ-eval (current-type-eval)])
-     (lambda (τ-stx)
-       (define τ+ (τ-eval τ-stx))
-       (syntax-parse τ+
-        [(~ψ (α) τ)
-         ;; TODO ?
-         τ+]
-        [_ τ+]))))
- (current-type-eval ψ-eval)
-
- ;; TODO my types are unequal. How does equality for ∀ types work?
- ;; (define ψ=?
-)
-
-;; =============================================================================
-;; === Signature maps
-;; Covert a type to an implementation. Use current-type-eval to normalize keys
-
-(begin-for-syntax 
-
- (define (Σ-print Σ port mode)
-   (define (print-k+v k+v)
-     (display (syntax->datum (car k+v)) port))
-   (display "{" port)
-   (define k+v* (Σ-map Σ))
-   (when (not (null? k+v*))
-     (print-k+v (car k+v*))
-     (for ([k+v (in-list k+v*)])
-       (display " " port)
-       (print-k+v k+v)))
-   (display "}" port))
-
- (struct Σ (
-   map ;; (Listof (Pairof τ* expr)), maps types to implementations
- ) #:property prop:procedure
-   (lambda (self arg)
-     (error 'Σ "Cannot apply struct, don't yet know how to turn types into predicates"))
-   #:methods gen:custom-write
-   [(define write-proc Σ-print)])
- 
- (define Σ-empty
-   (Σ '()))
-
- (define (Σ-key* Σ)
-   (map car (Σ-map Σ)))
-)
-
-;; =============================================================================
-
-(begin-for-syntax
- (define-syntax-rule (signature-error τ reason)
-   (error 'signature (format "Cannot define overloadable signature for at type '~a'. ~a"
-                             (syntax->datum τ) reason)))
-)
-
-(define-typed-syntax signature
-  [(_ (α:id) τ)
-   ;; Expand the type τ with α bound as a valid type
-   #:with ((α+) τ+ _) (infer/tyctx+erase #'([α : #%type]) #'τ)
-   ;; Make sure τ is (→ α τ') for some real type τ'
-   #:when (syntax-parse #'τ+
-           [(~→ τ-dom τ-cod)
-            ;; τ-dom MUST be the (expanded) identifier α+
-            (unless (and (identifier? #'τ-dom)
-                         (free-identifier=? #'τ-dom #'α+))
-              (signature-error #'τ
-                               (format "Variable '~a' must be free in the signature type." (syntax->datum #'α))))]
-           [_
-            (signature-error #'τ "We only support single-argument functions with overloaded domains.")])
-   ;; Using define to ensure top-level use
-   ;; (define k* (assign-type #'() #'#%type))
-   (⊢ #,Σ-empty
-      : (ψ (α) τ))]) ;; TODO add Σ-keys to the type?
-
-#;(define-typed-syntax #%app
-  [(_ e_fn e_arg)
-   #:with [e_fn+ τ_fn] (infers+erase #'e_fn)
-   #:when (ψ? #'τ_fn)
-   #:when (error 'APP (format "YOLO e = ~a arg = ~a τ = ~a"
-                              (syntax->datum #'e_fn)
-                              (syntax->datum #'e_arg)
-                              (syntax->datum #'τ_fn)))
-   #'(void)
-   ]
-  [(_ e* ...)
-   #'(stlc:#%app e* ...)])
diff --git a/tapl/tests/stlc+overloading-param-tests.rkt b/tapl/tests/stlc+overloading-param-tests.rkt
new file mode 100644
index 0000000..3b7408e
--- /dev/null
+++ b/tapl/tests/stlc+overloading-param-tests.rkt
@@ -0,0 +1,96 @@
+#lang s-exp "../stlc+overloading-param.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; -----------------------------------------------------------------------------
+;; --- syntax for ψ types
+
+(typecheck-fail
+ (signature (to-string0 α) (→ α Str Str))
+ #:with-msg "Expected")
+
+(typecheck-fail
+ (signature (to-string0 α) (→ Str Str))
+ #:with-msg "Expected")
+
+(typecheck-fail
+ (signature (to-string0 α) (→ α Str))
+ #:with-msg "not allowed in an expression context")
+
+;; -----------------------------------------------------------------------------
+;; --- basic overloading
+
+(signature (to-string α) (→ α Str))
+
+(typecheck-fail
+ (to-string 1)
+ #:with-msg "Resolution for 'to-string' failed")
+
+(typecheck-fail
+ (to-string "yolo")
+ #:with-msg "Resolution for 'to-string' failed")
+
+;; -- can later add cases to an overloaded name
+(instance (to-string Nat)
+  (λ ([x : Nat]) "num"))
+
+(instance (to-string Str)
+  (λ ([x : Str]) "string"))
+
+;; TODO can't use check-type for some reason. Literal #f is not allowed... missing type?
+;; (check-type-and-result
+ (to-string 3)
+ ;; : Str ⇒ "num")
+
+;; (check-type-and-result
+ ;; (to-string (+ 2 2))
+ ;; : Str ⇒ "num")
+
+;; (check-type-and-result
+ (to-string "hi")
+;;  : Str ⇒ "string")
+
+;; -- instances are type-checked. They must match
+(typecheck-fail
+ (instance (to-string Int)
+           (λ ([x : Num]) "num"))
+ #:with-msg "must be the instance type")
+
+(typecheck-fail
+ (instance (to-string Int)
+           (λ ([x : Int]) 0))
+ #:with-msg "must match template codomain")
+
+(typecheck-fail
+ (instance (to-string Int)
+           42)
+ #:with-msg "May only overload single-argument functions")
+
+;; -- no overlapping instances
+(typecheck-fail
+ (instance (to-string Nat)
+           (λ ([x : Nat]) "wrong"))
+ #:with-msg "Overlaps with existing instance")
+
+;; -- can't instantiate non-overloadeds
+(typecheck-fail
+ (λ ([x : (→ Int Int)])
+   (instance (x Int)
+             0))
+ #:with-msg "Not an overloaded identifier")
+           
+;; -- subtypes do not overlap
+(instance (to-string Int)
+          (λ ([x : Int]) "int"))
+
+;; -- explicit resolve
+
+;; -- recursive instances are fine [TODO really want (List α)]
+(instance (to-string (List Nat))
+          (λ ([x : (List Nat)]) "listnat"))
+
+;; (check-type-and-result
+(to-string (cons 1 (cons 2 (nil {Nat}))))
+;;  : Str ⇒ "listnat")
+
+;; -- higher-order use
+
diff --git a/tapl/tests/stlc+overloading-tests.rkt b/tapl/tests/stlc+overloading-tests.rkt
deleted file mode 100644
index 217254c..0000000
--- a/tapl/tests/stlc+overloading-tests.rkt
+++ /dev/null
@@ -1,52 +0,0 @@
-#lang s-exp "../stlc+overloading.rkt"
-(require "rackunit-typechecking.rkt")
-
-;; -----------------------------------------------------------------------------
-;; --- syntax for ψ types
-
-(typecheck-fail
- (signature (α) (→ α Str Str))
- #:with-msg "We only support single-argument functions")
-
-(typecheck-fail
- (signature (α) (→ Str Str))
- #:with-msg "Variable 'α' must be free")
-
-(check-type
- (signature (α) (→ α Str))
- : (ψ (α) (→ α Str)))
-
-;; -----------------------------------------------------------------------------
-;; --- basic overloading
-
-;; -- creating a signature does nothing, at first
-;; (signature (to-string α) (→ α Str))
-
-;; (typecheck-fail
-;;  (to-string 1)
-;;  #:with-msg "no instance")
-
-;; (typecheck-fail
-;;  (to-string "yolo")
-;;  #:with-msg "no instance")
-
-;; ;; -- can later add cases to an overloaded name
-;; (instance (to-string Num)
-;;   (λ ([x : Num]) "num"))
-
-;; (instance (to-string Str)
-;;   (λ ([x : Str]) "string"))
-
-;; (check-type-and-result
-;;  (to-string 43)
-;;  : Str ⇒ "num")
-
-;; (check-type-and-result
-;;  (to-string (+ 2 2))
-;;  : Str ⇒ "num")
-
-;; (check-type-and-result
-;;  (to-string "hi")
-;;  : Str ⇒ "string")
-
-;; ;; -- 

From c299e58a0438903adb78b71d89613558d7d1dd58 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Thu, 22 Oct 2015 05:44:17 -0400
Subject: [PATCH 7/9] [overload] fix export-as, export 'resolve', fix subtyping

---
 tapl/stlc+overloading-param.rkt             | 61 +++++++++++----------
 tapl/tests/stlc+overloading-param-tests.rkt | 56 +++++++++++++------
 2 files changed, 72 insertions(+), 45 deletions(-)

diff --git a/tapl/stlc+overloading-param.rkt b/tapl/stlc+overloading-param.rkt
index 15f3fb8..c4d14d8 100644
--- a/tapl/stlc+overloading-param.rkt
+++ b/tapl/stlc+overloading-param.rkt
@@ -1,7 +1,7 @@
 #lang s-exp "typecheck.rkt"
 (reuse List cons nil #:from "stlc+cons.rkt")
-(extends "stlc+sub.rkt" #:except #%datum #:rename [#%app stlc:#%app])
 (reuse #:from "stlc+rec-iso.rkt") ; load current-type=?
+(extends "stlc+sub.rkt" #:except #%datum #:rename [#%app stlc:#%app])
 
 ;; Apparently cannot propogate type information across statements.
 ;; Until the first-class ones work, let's do the big dumb parameter
@@ -32,11 +32,11 @@
    cod  ;; Type
  ) #:transparent
    #:property prop:procedure
-   (lambda (self τ-or-e)
+   (lambda (self τ-or-e #:exact? [exact? #f])
      (define r
        (if (syntax? τ-or-e) ;; Can I ask "type?"
-           (ℜ-resolve-syntax self τ-or-e)
-           (ℜ-resolve-value  self τ-or-e)))
+           (ℜ-resolve-syntax self τ-or-e #:exact? exact?)
+           (ℜ-resolve-value  self τ-or-e #:exact? exact?)))
      (or r
          (error 'ℜ (format "Resolution for '~a' failed at type ~a"
                            (syntax->datum (ℜ-name self))
@@ -54,23 +54,26 @@
  (define (ℜ->type ℜ)
    ((current-type-eval) #`(→ #,(assign-type #''α #'#%type) #,(ℜ-cod ℜ))))
 
- (define (ℜ-find ℜ τ)
-   (define τ=?
-     (let ([type=? (current-type=?)])
-       (lambda (τ2)
-         (type=? τ τ2))))
+ (define (ℜ-find ℜ τ #:=? =?)
+   (define (τ=? τ2)
+     (=? τ τ2))
    (assf τ=? (unbox (ℜ-dom* ℜ))))
 
- (define (ℜ-resolve-syntax ℜ τ)
-   (define result (ℜ-find ℜ τ))
+ (define (ℜ-resolve-syntax ℜ τ #:exact? [exact? #f])
+   ;; First try exact matches, then fall back to subtyping (unless 'exact?' is set).
+   ;; When subtyping, the __order instances were declared__ resolves ties.
+   (define result
+     (or (ℜ-find ℜ τ #:=? (current-type=?))
+         (and (not exact?)
+              (ℜ-find ℜ τ #:=? (current-typecheck-relation)))))
    (and (pair? result)
         (cdr result)))
 
- (define (ℜ-resolve-value ℜ e)
+ (define (ℜ-resolve-value ℜ e #:exact? [exact? #f])
    (error 'ℜ (format "Runtime resolution not implemented. Anyway your value was ~a" e)))
 
  (define (ℜ-unbound? ℜ τ)
-   (not (ℜ-find ℜ τ)))
+   (not (ℜ-resolve-syntax ℜ τ #:exact? #t)))
  
 )
 
@@ -100,27 +103,26 @@
   [(_ e* ...)
    (error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))])
 
-;; TODO make this available to users
-(define-for-syntax (resolve stx)
-  (syntax-parse stx
-   [(name:id τ)
-    #:with [name+ τ_fn+] (infer+erase #'name)
-    #:with τ+ ((current-type-eval) #'τ)
-    (define ℜ ((current-Σ) #'name+))
-    (unless ℜ
-      (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum #'name+))))
-    (ℜ #'τ)]))
+(define-for-syntax (resolve/internal id τ #:exact? [exact? #f])
+  (define ℜ ((current-Σ) id))
+  (unless ℜ (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum id))))
+  (ℜ τ #:exact? exact?))
 
-(define-typed-syntax #%app
+(define-typed-syntax resolve/tc #:export-as resolve
+  [(_ name:id τ)
+   #:with [name+ τ_fn+] (infer+erase #'name)
+   #:with τ+ ((current-type-eval) #'τ)
+   (resolve/internal #'name+ #'τ+ #:exact? #t)])
+
+(define-typed-syntax app/tc #:export-as #%app
   [(_ e_fn:id e_arg)
    #:with [e_fn+ τ_fn+] (infer+erase #'e_fn)
-   ;; Beware 3D syntax
    #:when ((current-Σ) #'e_fn+)
    #:with [e_arg+ τ_arg+] (infer+erase #'e_arg)
    (unless (syntax-e #'τ_arg+)
-     (error '#%app "No type for expression ~a\n" (syntax->datum #'e_arg)))
-   (define fn (resolve #'(e_fn+ τ_arg+)))
-   #`(#%app #,fn e_arg+)]
+     (error '#%app "(does this ever happen?) No type for expression ~a\n" (syntax->datum #'e_arg)))
+   (define fn (resolve/internal #'e_fn+ #'τ_arg+))
+   #`(app/tc #,fn e_arg+)]
   [(_ e* ...)
    #'(stlc:#%app e* ...)])
 
@@ -155,7 +157,8 @@
        (instance-error #'name #'τ (format "May only overload single-argument functions. (Got ~a and ~a)"
                                           (syntax->datum #'a) (syntax->datum #'b))
                                           )]))
-   (ℜ-add! ℜ #'τ #'e+) ;; Should we use syntax instead of e+ ?
+   (ℜ-add! ℜ #'τ #'e+)
+   ;; Should we use syntax instead of e+ ?
    (⊢ (void) : Bot)]
   [_
    (error 'instance "Expected (instance (id τ) e).")])
diff --git a/tapl/tests/stlc+overloading-param-tests.rkt b/tapl/tests/stlc+overloading-param-tests.rkt
index 3b7408e..9b79323 100644
--- a/tapl/tests/stlc+overloading-param-tests.rkt
+++ b/tapl/tests/stlc+overloading-param-tests.rkt
@@ -31,23 +31,51 @@
 
 ;; -- can later add cases to an overloaded name
 (instance (to-string Nat)
-  (λ ([x : Nat]) "num"))
+  (λ ([x : Nat]) "nat"))
 
 (instance (to-string Str)
   (λ ([x : Str]) "string"))
 
-;; TODO can't use check-type for some reason. Literal #f is not allowed... missing type?
-;; (check-type-and-result
+(check-type-and-result
  (to-string 3)
- ;; : Str ⇒ "num")
+ : Str ⇒ "nat")
 
-;; (check-type-and-result
- ;; (to-string (+ 2 2))
- ;; : Str ⇒ "num")
+(typecheck-fail
+ (to-string (+ 0 0))
+ #:with-msg "Resolution for 'to-string' failed")
 
-;; (check-type-and-result
+(instance (to-string Num)
+  (λ ([x : Num]) "num"))
+
+(check-type-and-result
+ (to-string (+ 2 2))
+ : Str ⇒ "num")
+
+(check-type-and-result
+ (to-string -1)
+ : Str ⇒ "num")
+
+(check-type-and-result
  (to-string "hi")
-;;  : Str ⇒ "string")
+ : Str ⇒ "string")
+
+;; -- use 'resolve' to get exact matches
+
+(check-type-and-result
+ ((resolve to-string Nat) 1)
+ : Str ⇒ "nat")
+
+(check-type-and-result
+ ((resolve to-string Num) 1)
+ : Str ⇒ "num")
+
+(typecheck-fail
+ (resolve to-string Int)
+ #:with-msg "Resolution for 'to-string' failed")
+
+(typecheck-fail
+ ((resolve to-string Num) "hello")
+ #:with-msg "have wrong type")
 
 ;; -- instances are type-checked. They must match
 (typecheck-fail
@@ -77,10 +105,6 @@
    (instance (x Int)
              0))
  #:with-msg "Not an overloaded identifier")
-           
-;; -- subtypes do not overlap
-(instance (to-string Int)
-          (λ ([x : Int]) "int"))
 
 ;; -- explicit resolve
 
@@ -88,9 +112,9 @@
 (instance (to-string (List Nat))
           (λ ([x : (List Nat)]) "listnat"))
 
-;; (check-type-and-result
-(to-string (cons 1 (cons 2 (nil {Nat}))))
-;;  : Str ⇒ "listnat")
+(check-type-and-result
+ (to-string (cons 1 (cons 2 (nil {Nat}))))
+ : Str ⇒ "listnat")
 
 ;; -- higher-order use
 

From e038d220f10841c795300455b23e33748949f733 Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Thu, 22 Oct 2015 15:20:16 -0400
Subject: [PATCH 8/9] [overload] now improved with identifier macros

---
 ...loading-param.rkt => stlc+overloading.rkt} | 114 +++++++++---------
 ...m-tests.rkt => stlc+overloading-tests.rkt} |   4 +-
 2 files changed, 58 insertions(+), 60 deletions(-)
 rename tapl/{stlc+overloading-param.rkt => stlc+overloading.rkt} (63%)
 rename tapl/tests/{stlc+overloading-param-tests.rkt => stlc+overloading-tests.rkt} (96%)

diff --git a/tapl/stlc+overloading-param.rkt b/tapl/stlc+overloading.rkt
similarity index 63%
rename from tapl/stlc+overloading-param.rkt
rename to tapl/stlc+overloading.rkt
index c4d14d8..ad7f076 100644
--- a/tapl/stlc+overloading-param.rkt
+++ b/tapl/stlc+overloading.rkt
@@ -1,15 +1,9 @@
 #lang s-exp "typecheck.rkt"
 (reuse List cons nil #:from "stlc+cons.rkt")
-(reuse #:from "stlc+rec-iso.rkt") ; load current-type=?
-(extends "stlc+sub.rkt" #:except #%datum #:rename [#%app stlc:#%app])
+(reuse #:from "stlc+rec-iso.rkt") ; to load current-type=?
+(extends "stlc+sub.rkt" #:except #%datum)
 
-;; Apparently cannot propogate type information across statements.
-;; Until the first-class ones work, let's do the big dumb parameter
-
-;; So here's what going to happen
-;; - current-Σ will be a map from identifiers to resolvers
-;; - resolvers will map overloaded signatures and types to concrete instances
-;; - extending a resolver (via instance) will add a new (τ, e) pair to a mutable list
+;; Revision of overloading, using identifier macros instead of overriding #%app
 
 ;; =============================================================================
 
@@ -30,7 +24,8 @@
    name ;; Symbol
    dom* ;; (Box (Listof (Pairof Type Expr)))
    cod  ;; Type
- ) #:transparent
+ ) #:constructor-name make-ℜ
+   #:transparent
    #:property prop:procedure
    (lambda (self τ-or-e #:exact? [exact? #f])
      (define r
@@ -49,10 +44,10 @@
    (set-box! dom* (cons (cons τ e) (unbox dom*))))
 
  (define (ℜ-init name τ-cod)
-   (ℜ name (box '()) τ-cod))
+   (make-ℜ name (box '()) τ-cod))
 
- (define (ℜ->type ℜ)
-   ((current-type-eval) #`(→ #,(assign-type #''α #'#%type) #,(ℜ-cod ℜ))))
+ (define (ℜ->type ℜ #:subst [τ-dom (assign-type #''α #'#%type)])
+   ((current-type-eval) #`(→ #,τ-dom #,(ℜ-cod ℜ))))
 
  (define (ℜ-find ℜ τ #:=? =?)
    (define (τ=? τ2)
@@ -74,72 +69,75 @@
 
  (define (ℜ-unbound? ℜ τ)
    (not (ℜ-resolve-syntax ℜ τ #:exact? #t)))
- 
+
+ (define (syntax->ℜ id)
+   ;; Don't care about the type
+   (define stx+τ (infer+erase id))
+   ;; Boy, I wish I had a monad
+   (define (fail)
+     (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum id))))
+   (unless (pair? stx+τ) (fail))
+   (define stx (car stx+τ))
+   (unless (syntax? stx) (fail))
+   (define ℜ-stx (syntax->datum (car stx+τ)))
+   (unless (and (list? ℜ-stx)
+                (not (null? ℜ-stx))
+                (not (null? (cdr ℜ-stx))))
+     (fail))
+   (define ℜ (cadr ℜ-stx))
+   (unless (ℜ? ℜ) (fail))
+   ℜ)
+
+ (define-syntax-rule (error-template sym id τ reason)
+   (error sym (format "Failure for '~a' at type '~a'. ~a"
+                      (syntax->datum id)
+                      (syntax->datum τ)
+                      reason)))
+
+ (define-syntax-rule (instance-error id τ reason)
+   (error-template 'instance id τ reason))
+
+ (define-syntax-rule (resolve-error id τ reason)
+   (error-template 'resolve id τ reason))
 )
 
 ;; =============================================================================
 ;; === Overloaded signature environment
 
-(begin-for-syntax
- (define current-Σ (make-parameter (lambda (id) #f)))
-)
-
 (define-typed-syntax signature
   [(_ (name:id α:id) τ)
    #:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ)
-   (let ([ℜ-old ((current-Σ) #'name)])
-     (when ℜ-old
-       (error 'signature (format "Identifier '~a' already bound to a type ~a"
-                                 (syntax->datum #'name) (syntax->datum (ℜ->type ℜ-old))))))
    (define ℜ (ℜ-init #'name #'τ-cod))
-   (current-Σ 
-    (let ([old-Σ (current-Σ)])
-      (lambda (id)
-        (if (free-identifier=? id #'name)
-            ℜ
-            (old-Σ id)))))
-   (⊢ (define name #,ℜ)
+   (⊢ (define-syntax name
+        (syntax-parser
+         [_:id
+          #'(quote #,ℜ)] ;; Is there a way to transmit ℜ directly?
+         [(n e)
+          #:with [e+ τ+] (infer+erase #'e)
+          #:with n+ (#,ℜ #'τ+)
+          (⊢ (#%app n+ e+)
+             : τ-cod)]
+         [(_ e* (... ...))
+          #'(raise-arity-error (syntax->datum name) 1 e* (... ...))]))
       : Bot)]
   [(_ e* ...)
    (error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))])
 
-(define-for-syntax (resolve/internal id τ #:exact? [exact? #f])
-  (define ℜ ((current-Σ) id))
-  (unless ℜ (error 'resolve (format "Identifier '~a' is not overloaded" (syntax->datum id))))
-  (ℜ τ #:exact? exact?))
-
 (define-typed-syntax resolve/tc #:export-as resolve
   [(_ name:id τ)
-   #:with [name+ τ_fn+] (infer+erase #'name)
    #:with τ+ ((current-type-eval) #'τ)
-   (resolve/internal #'name+ #'τ+ #:exact? #t)])
-
-(define-typed-syntax app/tc #:export-as #%app
-  [(_ e_fn:id e_arg)
-   #:with [e_fn+ τ_fn+] (infer+erase #'e_fn)
-   #:when ((current-Σ) #'e_fn+)
-   #:with [e_arg+ τ_arg+] (infer+erase #'e_arg)
-   (unless (syntax-e #'τ_arg+)
-     (error '#%app "(does this ever happen?) No type for expression ~a\n" (syntax->datum #'e_arg)))
-   (define fn (resolve/internal #'e_fn+ #'τ_arg+))
-   #`(app/tc #,fn e_arg+)]
-  [(_ e* ...)
-   #'(stlc:#%app e* ...)])
-
-(begin-for-syntax
-(define-syntax-rule (instance-error id τ r)
-  (error 'instance (format "Cannot make instance for '~a' at type '~a'. ~a"
-                           (syntax->datum id) (syntax->datum τ) r)))
-)
+   ;; Extract a resolver from the syntax object
+   (define ℜ (syntax->ℜ #'name))
+   ;; Apply the resolver to the argument type. woo-wee!
+   (⊢ #,(ℜ #'τ+ #:exact? #t) : #,(ℜ->type ℜ #:subst #'τ+))])
 
 (define-typed-syntax instance
   [(_ (name:id τ-stx) e)
    #:with τ ((current-type-eval) #'τ-stx)
    #:with [e+ τ+] (infer+erase #'e)
-   (define ℜ ((current-Σ) #'name))
-   (unless ℜ (instance-error #'name #'τ "Not an overloaded identifier."))
+   (define ℜ (syntax->ℜ #'name))
    (unless (ℜ-unbound? ℜ #'τ) (instance-error #'name #'τ "Overlaps with existing instance."))
-   (define does-this-id-matter?
+   (define _unify ;; Should be a helper function
      (syntax-parse #`(τ+ #,(ℜ->type ℜ))
       [((~→ τ_dom1 τ_cod1)
         (~→ _      τ_cod2))
@@ -157,8 +155,8 @@
        (instance-error #'name #'τ (format "May only overload single-argument functions. (Got ~a and ~a)"
                                           (syntax->datum #'a) (syntax->datum #'b))
                                           )]))
-   (ℜ-add! ℜ #'τ #'e+)
    ;; Should we use syntax instead of e+ ?
+   (ℜ-add! ℜ #'τ #'e+)
    (⊢ (void) : Bot)]
   [_
    (error 'instance "Expected (instance (id τ) e).")])
diff --git a/tapl/tests/stlc+overloading-param-tests.rkt b/tapl/tests/stlc+overloading-tests.rkt
similarity index 96%
rename from tapl/tests/stlc+overloading-param-tests.rkt
rename to tapl/tests/stlc+overloading-tests.rkt
index 9b79323..44754ea 100644
--- a/tapl/tests/stlc+overloading-param-tests.rkt
+++ b/tapl/tests/stlc+overloading-tests.rkt
@@ -1,4 +1,4 @@
-#lang s-exp "../stlc+overloading-param.rkt"
+#lang s-exp "../stlc+overloading.rkt"
 (require "rackunit-typechecking.rkt")
 
 ;; -----------------------------------------------------------------------------
@@ -104,7 +104,7 @@
  (λ ([x : (→ Int Int)])
    (instance (x Int)
              0))
- #:with-msg "Not an overloaded identifier")
+ #:with-msg "Identifier 'x' is not overloaded")
 
 ;; -- explicit resolve
 

From 51e6e1b3ae750e8a8df7dc058b010bb5661c0b7e Mon Sep 17 00:00:00 2001
From: Ben Greenman <types@ccs.neu.edu>
Date: Thu, 22 Oct 2015 17:07:05 -0400
Subject: [PATCH 9/9] [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}