From b0a8d192effd90aefb5a6b6e5d1d4ddc5e172890 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 9 Jul 2015 14:00:36 -0400
Subject: [PATCH] finish exist.rkt

---
 tapl/exist.rkt               |  93 +++++++++++++++++++--
 tapl/tests/exist-tests.rkt   | 157 +++++++++++++++++++++++++++++++++++
 tapl/tests/run-all-tests.rkt |   9 +-
 tapl/typecheck.rkt           |  23 ++++-
 4 files changed, 275 insertions(+), 7 deletions(-)

diff --git a/tapl/exist.rkt b/tapl/exist.rkt
index 1f105f5..080edd0 100644
--- a/tapl/exist.rkt
+++ b/tapl/exist.rkt
@@ -1,12 +1,95 @@
 #lang racket/base
 (require "typecheck.rkt")
-(require (except-in "stlc+reco+var.rkt" #%app λ)
-         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ)))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
-(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ))
- 
+(require (except-in "stlc+reco+var.rkt" #%app λ let type=?)
+         (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let type=?))
+         (prefix-in sysf: (only-in "sysf.rkt" type=?)))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])
+         (for-syntax type=?))
+(provide (except-out (all-from-out "stlc+reco+var.rkt") stlc:#%app stlc:λ stlc:let
+                     (for-syntax stlc:type=?)))
+(provide ∃ pack open)
+
 ;; existential types
+;; combine type=? from sysf (for lam, ie ∃) and stlc+reco+var (for strings)
 ;; Types:
 ;; - types from stlc+reco+var.rkt
+;; - ∃
 ;; Terms:
 ;; - terms from stlc+reco+var.rkt
+;; - pack and open
+
+(begin-for-syntax
+  (define (type=? t1 t2)
+    (or (stlc:type=? t1 t2)
+        (sysf:type=? t1 t2)))
+  (current-type=? type=?)
+  (current-typecheck-relation type=?))
+
+;; TODO: disambiguate expanded representation of ∃, ok to use lambda in this calculus
+(provide ∃)
+(define-syntax (∃ stx)
+  (syntax-parse stx
+    [(_ (tv:id) body)
+     (syntax/loc stx (#%plain-lambda (tv) body))]))
+
+(define-syntax (pack stx)
+  (syntax-parse stx
+    [(_ (τ:type e) as ∃τ:type)
+     #:with (#%plain-lambda (τ_abstract:id) τ_body) #'∃τ.norm
+     #:with [e- τ_e] (infer+erase #'e)
+     #:when (typecheck? #'τ_e  (subst #'τ.norm #'τ_abstract #'τ_body))
+     (⊢ #'e- #'∃τ)]))
+
+; TODO: the colon syntax might be misleading, since tv is not the type of x
+(define-syntax (open stx)
+  (syntax-parse stx #:datum-literals (<=)
+    [(_ ([(tv:id x:id) <= e_packed]) e)
+     #:with [e_packed- τ_packed] (infer+erase #'e_packed)
+     #:with (#%plain-lambda (τ_abstract:id) τ_body) #'τ_packed ; existential
+     ;; The subst below appears to be a hack, but it's not really.
+     ;; It's the (TaPL) type rule itself that is fast and loose.
+     ;; Leveraging the macro system's management of binding reveals this.
+     ;; 
+     ;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366:
+     ;; Γ ⊢ t_1 : {∃X,T_12}
+     ;; Γ,X,x:T_12 ⊢ t_2 : T_2
+     ;; ------------------------------
+     ;; Γ ⊢ let {X,x}=t_1 in t_2 : T_2
+     ;;
+     ;; There's *two* separate binders, the ∃ and the let,
+     ;; which the rule conflates.
+     ;;
+     ;; Here's the rule rewritten to distinguish the two binding positions:
+     ;; Γ ⊢ t_1 : {∃X_1,T_12}
+     ;; Γ,X_???,x:T_12 ⊢ t_2 : T_2
+     ;; ------------------------------
+     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;;
+     ;; The X_1 binds references to X in T_12.
+     ;; The X_2 binds references to X in t_2.
+     ;; What should the X_??? be?
+     ;;
+     ;; A first guess might be to replace X_??? with both X_1 and X_2,
+     ;; so all the potentially referenced type vars are bound.
+     ;; Γ ⊢ t_1 : {∃X_1,T_12}
+     ;; Γ,X_1,X_2,x:T_12 ⊢ t_2 : T_2
+     ;; ------------------------------
+     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;;
+     ;; But this example demonstrates that the rule above doesnt work:
+     ;; (open ([x : X_2 (pack (Int 0) as (∃ (X_1) X_1))])
+     ;;   ((λ ([y : X_2]) y) x)
+     ;; Here, x has type X_1, y has type X_2, but they should be the same thing,
+     ;; so we need to replace all X_1's with X_2
+     ;;
+     ;; Here's the fixed rule, which is implemented here
+     ;;
+     ;; Γ ⊢ t_1 : {∃X_1,T_12}
+     ;; Γ,X_2,x:[X_2/X_1]T_12 ⊢ t_2 : T_2
+     ;; ------------------------------
+     ;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
+     ;;
+     #:with [tvs- (x-) (e-) (τ_e)]
+            (infer #'(e) #:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)])
+                         #:tvs #'(tv))
+     (⊢ #'(let ([x- e_packed-]) e-) #'τ_e)]))
\ No newline at end of file
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
index 6dfb462..b44d05c 100644
--- a/tapl/tests/exist-tests.rkt
+++ b/tapl/tests/exist-tests.rkt
@@ -1,6 +1,163 @@
 #lang s-exp "../exist.rkt"
 (require "rackunit-typechecking.rkt")
 
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
+(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
+(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
+(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
+(typecheck-fail (pack (Int #t) as (∃ (X) X)))
+
+; cant typecheck bc X has local scope, and no X elimination form
+;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X) 
+
+(check-type 0 : Int)
+(check-type (+ 0 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
+(typecheck-fail (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) (+ x 1))) ; can't use as Int
+
+(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ 0)
+(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
+            : (∃ (X) X) ⇒ #t)
+
+;; example where the two binding X's are conflated, see exist.rkt for explanation
+(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) ((λ ([y : X]) 1) x))
+            : Int ⇒ 1)
+            
+(check-type
+ (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
+ : (∃ (X) (× [: "a" X] [: "f" (→ X X)])))
+
+(define p4
+  (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
+        as (∃ (X) (× [: "a" X] [: "f" (→ X Int)]))))
+(check-type p4 : (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
+
+(check-not-type (open ([(X x) <= p4]) (proj x "a")) : Int) ; type is X, not Int
+; type is (→ X X), not (→ Int Int)
+(check-not-type (open ([(X x) <= p4]) (proj x "f")) : (→ Int Int))
+(typecheck-fail (open ([(X x) <= p4]) (+ 1 (proj x "a"))))
+(check-type (open ([(X x) <= p4]) ((proj x "f") (proj x "a"))) : Int ⇒ 6)
+(check-type (open ([(X x) <= p4]) ((λ ([y : X]) ((proj x "f") y)) (proj x "a"))) : Int ⇒ 6)
+
+(check-type
+ (open ([(X x) <= (pack (Int 0) as (∃ (Y) Y))])
+       ((λ ([y : X]) 1) x))
+ : Int ⇒ 1)
+
+(check-type
+ (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
+ : (∃ (X) (× [: "a" Int] [: "f" (→ Int Int)])))
+
+(typecheck-fail
+ (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [: "a" Int] [: "f" (→ Bool Int)]))))
+
+(typecheck-fail
+ (pack (Int (tup ["a" = 5] ["f" = (λ ([x : Int]) (+ x 1))]))
+       as (∃ (X) (× [: "a" X] [: "f" (→ X Bool)]))))
+
+(check-type
+ (pack (Bool (tup ["a" = #t] ["f" = (λ ([x : Bool]) (if x 1 2))]))
+       as (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
+ : (∃ (X) (× [: "a" X] [: "f" (→ X Int)])))
+
+(define counterADT
+  (pack (Int (tup ["new" = 1]
+                  ["get" = (λ ([i : Int]) i)]
+                  ["inc" = (λ ([i : Int]) (+ i 1))]))
+        as (∃ (Counter) (× [: "new" Counter]
+                           [: "get" (→ Counter Int)]
+                           [: "inc" (→ Counter Counter)]))))
+(check-type counterADT :
+            (∃ (Counter) (× [: "new" Counter]
+                            [: "get" (→ Counter Int)]
+                            [: "inc" (→ Counter Counter)])))
+(check-type
+ (open ([(Counter counter) <= counterADT])
+       ((proj counter "get") ((proj counter "inc") (proj counter "new"))))
+ : Int ⇒ 2)
+
+ (check-type
+  (open ([(Counter counter) <= counterADT])
+        (let ([inc (proj counter "inc")]
+              [get (proj counter "get")])
+          (let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
+            (get (add3 (proj counter "new"))))))
+  : Int ⇒ 4)
+
+(check-type
+ (open ([(Counter counter) <= counterADT])
+       (let ([get (proj counter "get")]
+             [inc (proj counter "inc")]
+             [new (λ () (proj counter "new"))])
+         (letrec ([(is-even? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (or (zero? n)
+                      (is-odd? (sub1 n))))]
+                  [(is-odd? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (and (not (zero? n))
+                          (is-even? (sub1 n))))])
+           (open ([(FlipFlop flipflop) <=
+                   (pack (Counter (tup ["new" = (new)]
+                                       ["read" = (λ ([c : Counter]) (is-even? (get c)))]
+                                       ["toggle" = (λ ([c : Counter]) (inc c))]
+                                       ["reset" = (λ ([c : Counter]) (new))]))
+                         as (∃ (FlipFlop) (× [: "new" FlipFlop]
+                                             [: "read" (→ FlipFlop Bool)]
+                                             [: "toggle" (→ FlipFlop FlipFlop)]
+                                             [: "reset" (→ FlipFlop FlipFlop)])))])
+                 (let ([read (proj flipflop "read")]
+                       [togg (proj flipflop "toggle")])
+                   (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+ : Bool ⇒ #f)
+
+(define counterADT2
+  (pack ((× [: "x" Int])
+         (tup ["new" = (tup ["x" = 1])]
+              ["get" = (λ ([i : (× [: "x" Int])]) (proj i "x"))]
+              ["inc" = (λ ([i : (× [: "x" Int])]) (tup ["x" = (+ 1 (proj i "x"))]))]))
+        as (∃ (Counter) (× [: "new" Counter]
+                           [: "get" (→ Counter Int)]
+                           [: "inc" (→ Counter Counter)]))))
+(check-type counterADT2 :
+            (∃ (Counter) (× [: "new" Counter]
+                            [: "get" (→ Counter Int)]
+                            [: "inc" (→ Counter Counter)])))
+
+;; same as above, but with different internal counter representation
+(check-type
+ (open ([(Counter counter) <= counterADT2])
+       (let ([get (proj counter "get")]
+             [inc (proj counter "inc")]
+             [new (λ () (proj counter "new"))])
+         (letrec ([(is-even? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (or (zero? n)
+                      (is-odd? (sub1 n))))]
+                  [(is-odd? : (→ Int Bool))
+                   (λ ([n : Int])
+                     (and (not (zero? n))
+                          (is-even? (sub1 n))))])
+           (open ([(FlipFlop flipflop) <=
+                   (pack (Counter (tup ["new" = (new)]
+                                       ["read" = (λ ([c : Counter]) (is-even? (get c)))]
+                                       ["toggle" = (λ ([c : Counter]) (inc c))]
+                                       ["reset" = (λ ([c : Counter]) (new))]))
+                         as (∃ (FlipFlop) (× [: "new" FlipFlop]
+                                             [: "read" (→ FlipFlop Bool)]
+                                             [: "toggle" (→ FlipFlop FlipFlop)]
+                                             [: "reset" (→ FlipFlop FlipFlop)])))])
+                 (let ([read (proj flipflop "read")]
+                       [togg (proj flipflop "toggle")])
+                   (read (togg (togg (togg (togg (proj flipflop "new")))))))))))
+ : Bool ⇒ #f)
+
+;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
 ;; define-type-alias
 (define-type-alias Integer Int)
 (define-type-alias ArithBinOp (→ Int Int Int))
diff --git a/tapl/tests/run-all-tests.rkt b/tapl/tests/run-all-tests.rkt
index 649eb03..aefec3b 100644
--- a/tapl/tests/run-all-tests.rkt
+++ b/tapl/tests/run-all-tests.rkt
@@ -1,4 +1,6 @@
 #lang racket
+
+;; stlc and extensions
 (require "stlc-tests.rkt")
 (require "stlc+lit-tests.rkt")
 (require "ext-stlc-tests.rkt")
@@ -9,10 +11,15 @@
 
 (require "stlc+rec-iso-tests.rkt")
 
+(require "exist-tests.rkt")
+
+;; subtyping
 (require "stlc+sub-tests.rkt")
 (require "stlc+reco+sub-tests.rkt")
 
+;; system F
 (require "sysf-tests.rkt")
-(require "exist-tests.rkt")
+
+;; F_omega
 (require "fomega-tests.rkt")
 (require "fomega2-tests.rkt")
\ No newline at end of file
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index e34b430..550d6d3 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -167,11 +167,32 @@
   (define (infers+erase es)
     (stx-map infer+erase es))
   ;; infers and erases types in an expression, in the context of given type vars
-  (define (infer/tvs+erase e [tvs #'()])
+  (define (infer/tvs+erase e tvs)
     (syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression)
       [(lam tvs+ (#%expression e+))
        (list #'tvs+ #'e+ (syntax-local-introduce (typeof #'e+)))]))
 
+  (define (infer es #:ctx [ctx null] #:tvs [tvs null])
+    (syntax-parse ctx #:datum-literals (:)
+      [([x : τ] ...) ; dont expand yet bc τ may have references to tvs
+;       #:with (x ...) #'(b.x ...)
+;       #:with (τ ...) #'(b.τ ...)
+       #:with (e ...) es
+       #:with
+       ((~literal #%plain-lambda) tvs+
+        ((~literal #%expression)
+         ((~literal #%plain-lambda) xs+
+          ((~literal letrec-syntaxes+values) stxs1 ()
+            ((~literal letrec-syntaxes+values) stxs2 ()
+              ((~literal #%expression) e+) ...)))))
+       (expand/df
+        #`(λ #,tvs
+            (λ (x ...)
+              (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+                (#%expression e) ...))))
+       (list #'tvs+ #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))]
+      [([x τ] ...) (infer+erase es #:ctx #'([x : τ] ...) #:tvs tvs)]))
+
   (define current-typecheck-relation (make-parameter #f))
   (define (typecheck? t1 t2) ((current-typecheck-relation) t1 t2))
   (define (typechecks? τs1 τs2)