type=? handles binding types by default

- closes #32

macrotypes/examples/exist.rkt

@@ -1,6 +1,5 @@
 #lang s-exp macrotypes/typecheck
 (extends "stlc+reco+var.rkt")
-(reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=?
 
 ;; existential types
 ;; Types:
@@ -9,8 +8,6 @@
 ;; Terms:
 ;; - terms from stlc+reco+var.rkt
 ;; - pack and open
-;; Other: type=? from stlc+rec-iso.rkt
-
 
 (define-type-constructor ∃ #:bvs = 1)
 

macrotypes/examples/mlish.rkt

@@ -8,7 +8,7 @@
 (require (only-in "ext-stlc.rkt" → →?))
 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
-(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
+(require (only-in "stlc+rec-iso.rkt" ~× ×?))
 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))

macrotypes/examples/stlc+rec-iso.rkt

@@ -11,51 +11,9 @@
 ;; - terms from stlc+tup.rkt
 ;; - also var and case from stlc+reco+var
 ;; - fld, unfld
-;; Other:
-;; - extend type=? to handle lambdas
 
 (define-type-constructor μ #:bvs = 1)
 
-(begin-for-syntax
-  (define stlc:type=? (current-type=?))
-  ;; extend to handle μ, ie lambdas
-  (define (type=? τ1 τ2)
-;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
-;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
-    (syntax-parse (list τ1 τ2)
-      ;; alternative #4: use old type=? for everything except lambda
-      [(((~literal #%plain-lambda) (x:id ...) t1 ...)
-        ((~literal #%plain-lambda) (y:id ...) t2 ...))
-       (and (stx-length=? #'(x ...) #'(y ...))
-            (stx-length=? #'(t1 ...) #'(t2 ...))
-            (stx-andmap
-             (λ (t1 t2)
-               ((current-type=?) (substs #'(y ...) #'(x ...) t1) t2))
-             #'(t1 ...) #'(t2 ...)))]
-      #;[(((~literal #%plain-app) tycon1 ((~literal #%plain-lambda) (x:id ...) k1 ... t1))
-        ((~literal #%plain-app) tycon2 ((~literal #%plain-lambda) (y:id ...) k2 ... t2)))
-       #:when ((current-type=?) #'tycon1 #'tycon2)
-       #:when (types=? #'(k1 ...) #'(k2 ...))
-       #:when (stx-length=? #'(x ...) #'(y ...))
-       #:with (z ...) (generate-temporaries #'(x ...))
-       ;; alternative #1: install wrappers that checks for x and y and return true
-       #;(define old-type=? (current-type=?))
-       #;(define (new-type=? ty1 ty2)
-         (or (and (identifier? ty1) (identifier? ty2)
-                  (stx-ormap (λ (x y)
-                               (and (bound-identifier=? ty1 x) (bound-identifier=? ty2 y)))
-                             #'(x ...) #'(y ...)))
-             (old-type=? ty1 ty2)))
-       #;(parameterize ([current-type=? new-type=?]) ((current-type=?) #'t1 #'t2))
-       ;; alternative #2: subst fresh identifier for both x and y
-       #;((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
-                           (substs #'(z ...) #'(y ...) #'t2))
-       ;; alternative #3: subst y for x in t1
-       ((current-type=?) (substs #'(y ...) #'(x ...) #'t1) #'t2)]
-      [_ (stlc:type=? τ1 τ2)]))
-  (current-type=? type=?)
-  (current-typecheck-relation type=?))
-
 (define-typed-syntax unfld
   [(unfld τ:type-ann e)
    #:with (~μ* (tv) τ_body) #'τ.norm

macrotypes/examples/stlc+reco+sub.rkt

@@ -1,14 +1,12 @@
 #lang s-exp macrotypes/typecheck
-(extends "stlc+sub.rkt" #:except #%app #%datum)
+(extends "stlc+sub.rkt" #:except #%datum)
 (extends "stlc+reco+var.rkt" #:except #%datum +)
-;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
-;; but extend sub? from stlc+sub.rkt
 
 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records
 ;; Types:
 ;; - types from stlc+sub.rkt
 ;; Type relations:
-;; - sub? extended to records
+;; - sub? (from stlc+sub.rkt) extended to records
 ;; Terms:
 ;; - terms from stlc+sub.rkt
 ;; - records and variants from stlc+reco+var

macrotypes/examples/sysf.rkt

@@ -1,10 +1,7 @@
 #lang s-exp macrotypes/typecheck
 (extends "stlc+lit.rkt")
-(reuse #:from "stlc+rec-iso.rkt") ; want this type=?
 
 ;; System F
-;; Type relation:
-;; - extend type=? with ∀
 ;; Types:
 ;; - types from stlc+lit.rkt
 ;; - ∀

macrotypes/typecheck.rkt

@@ -818,8 +818,17 @@
              ;(printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum t2))
              (or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2))
                  (and (stx-null? t1) (stx-null? t2))
-                 (and (stx-pair? t1) (stx-pair? t2)
-                      (names=? t1 t2))))
+                 (syntax-parse (list t1 t2)
+                   [(((~literal #%plain-lambda) (~and (_:id (... ...)) xs) . ts1)
+                     ((~literal #%plain-lambda) (~and (_:id (... ...)) ys) . ts2))
+                    (and (stx-length=? #'xs #'ys) 
+                         (stx-length=? #'ts1 #'ts2)
+                         (stx-andmap
+                          (λ (ty1 ty2)
+                            ((current-name=?) (substs #'ys #'xs ty1) ty2))
+                          #'ts1 #'ts2))]
+                   [_ (and (stx-pair? t1) (stx-pair? t2)
+                           (names=? t1 t2))])))
            (define current-name=? (make-parameter name=?))
            (current-typecheck-relation name=?)
            (define (names=? τs1 τs2)

turnstile/examples/exist.rkt

@@ -1,6 +1,5 @@
 #lang turnstile/lang
 (extends "stlc+reco+var.rkt")
-(reuse #:from "stlc+rec-iso.rkt") ; want type=?, but only need to load current-type=?
 
 ;; existential types
 ;; Types:
@@ -9,8 +8,6 @@
 ;; Terms:
 ;; - terms from stlc+reco+var.rkt
 ;; - pack and open
-;; Other: type=? from stlc+rec-iso.rkt
-
 
 (define-type-constructor ∃ #:bvs = 1)
 

turnstile/examples/fomega.rkt

@@ -88,7 +88,7 @@
   [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
 
 (define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
+  [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
   [⊢ τ ≫ τ- ⇐ k] ...
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------

turnstile/examples/mlish.rkt

@@ -8,7 +8,7 @@
 (require (only-in "ext-stlc.rkt" → →?))
 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
-(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
+(require (only-in "stlc+rec-iso.rkt" ~× ×?))
 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))

turnstile/examples/stlc+rec-iso.rkt

@@ -11,31 +11,9 @@
 ;; - terms from stlc+tup.rkt
 ;; - also var and case from stlc+reco+var
 ;; - fld, unfld
-;; Other:
-;; - extend type=? to handle lambdas
 
 (define-type-constructor μ #:bvs = 1)
 
-(begin-for-syntax
-  (define stlc:type=? (current-type=?))
-  ;; extend to handle μ, ie lambdas
-  (define (type=? τ1 τ2)
-;    (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1))
-;    (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2))
-    (syntax-parse (list τ1 τ2)
-      ;; alternative #4: use old type=? for everything except lambda
-      [(((~literal #%plain-lambda) (x:id ...) t1 ...)
-        ((~literal #%plain-lambda) (y:id ...) t2 ...))
-       (and (stx-length=? #'(x ...) #'(y ...))
-            (stx-length=? #'(t1 ...) #'(t2 ...))
-            (stx-andmap
-             (λ (t1 t2)
-               ((current-type=?) (substs #'(y ...) #'(x ...) t1) t2))
-             #'(t1 ...) #'(t2 ...)))]
-      [_ (stlc:type=? τ1 τ2)]))
-  (current-type=? type=?)
-  (current-typecheck-relation type=?))
-
 (define-typed-syntax (unfld τ:type-ann e) ≫
   #:with (~μ* (tv) τ_body) #'τ.norm
   [⊢ e ≫ e- ⇐ τ.norm]

turnstile/examples/stlc+reco+sub.rkt

@@ -1,14 +1,12 @@
 #lang turnstile/lang
-(extends "stlc+sub.rkt" #:except #%app #%datum)
+(extends "stlc+sub.rkt" #:except #%datum)
 (extends "stlc+reco+var.rkt" #:except #%datum + *)
-;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
-;; but extend sub? from stlc+sub.rkt
 
 ;; Simply-Typed Lambda Calculus, plus subtyping, plus records
 ;; Types:
 ;; - types from stlc+sub.rkt
 ;; Type relations:
-;; - sub? extended to records
+;; - sub? (from stlc+sub.rkt) extended to records
 ;; Terms:
 ;; - terms from stlc+sub.rkt
 ;; - records and variants from stlc+reco+var

turnstile/examples/sysf.rkt

@@ -1,10 +1,7 @@
 #lang turnstile/lang
 (extends "stlc+lit.rkt")
-(reuse #:from "stlc+rec-iso.rkt") ; want this type=?
 
 ;; System F
-;; Type relation:
-;; - extend type=? with ∀
 ;; Types:
 ;; - types from stlc+lit.rkt
 ;; - ∀