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] [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")
-
-;; ;; --