start sysf

tapl/README.md

@@ -10,4 +10,5 @@ A file extends its immediate parent file.
            - stlc+cons.rkt
              - stlc+box.rkt
      - stlc+sub.rkt
-       - stlc+rec+var+sub.rkt
+       - stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt)
+     - sysf.rkt

tapl/stx-utils.rkt

@@ -31,4 +31,6 @@
   (string=? (syntax-e s1) (syntax-e s2)))
 
 (define (stx-sort stx cmp)
-  (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
+  (sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
+(define (stx-fold f base . lsts)
+  (apply foldl f base (map syntax->list lsts)))

tapl/sysf.rkt

@@ -0,0 +1,31 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse)
+;  (for-meta 2 racket/base)
+  "typecheck.rkt")
+(require (except-in "stlc+lit.rkt" λ #%app)
+         (prefix-in stlc: (only-in "stlc+lit.rkt" λ #%app)))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ]))
+(provide (except-out (all-from-out "stlc+lit.rkt") stlc:λ stlc:#%app))
+(provide Λ inst)
+
+ 
+;; System F
+;; Types:
+;; - types from stlc+lit.rkt
+;; Terms:
+;; - terms from stlc+lit.rkt
+
+(define-type-constructor ∀)
+
+(define-syntax (Λ stx)
+  (syntax-parse stx
+    [(_ (tv:id ...) e)
+     #:with (tvs+ e- τ) (infer/tvs+erase #'e #'(tv ...))
+     (⊢ #'e- #'(∀ tvs+ τ))]))
+(define-syntax (inst stx)
+  (syntax-parse stx
+    [(_ e τ ...)
+     #:with (e- τ_e) (infer+erase #'e)
+     #:with ((~literal ∀) (tv ...) τ_body) #'τ_e
+     (⊢ #'e- (substs #'(τ ...) #'(tv ...) #'τ_body))]))

tapl/tests/sysf-tests.rkt

@@ -0,0 +1,25 @@
+#lang s-exp "../sysf.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
+
+;; previous tests -------------------------------------------------------------
+(check-type 1 : Int)
+(check-not-type 1 : (→ Int Int))
+(typecheck-fail "one") ; unsupported literal
+(typecheck-fail #f) ; unsupported literal
+(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
+            : (→ (→ Int Int Int) Int Int Int))
+(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)

tapl/typecheck.rkt

@@ -124,9 +124,18 @@
        (list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
       [([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)]))
 
-  (define (infer+erase e)
-    (define e+ (expand/df e))
-    (list e+ (eval-τ (typeof e+))))
+  (define (infer+erase e [tvs #'()])
+    (define e+
+      (syntax-parse (expand/df #`(λ #,tvs #,e)) #:literals (#%expression)
+        [(lam tvs+ (#%expression e+)) #'e+]
+        [(lam tvs+ e+) #'e+]))
+    (list e+ (eval-τ (typeof e+) tvs)))
+  (define (infer/tvs+erase e [tvs #'()])
+    (define-values (tvs+ e+)
+      (syntax-parse (expand/df #`(λ #,tvs #,e)) #:literals (#%expression)
+        [(lam tvs+ (#%expression e+)) (values #'tvs+ #'e+)]
+        [(lam tvs+ e+) (values #'tvs+ #'e+)]))
+    (list tvs+ e+ (eval-τ (typeof e+) tvs)))
   (define (infers+erase es)
     (stx-map infer+erase es))
   (define (types=? τs1 τs2)
@@ -155,7 +164,9 @@
   #;(define (assert-types es τs)
     (stx-andmap assert-type es τs))
 
-  (define (eval-τ τ)
+  (define (eval-τ τ [tvs #'()])
+    (if (and (identifier? τ) (stx-member τ tvs))
+        τ
     (syntax-parse τ
       [s:str τ] ; record field
       [_
@@ -169,8 +180,8 @@
            maybe-app-τ
            (syntax-parse maybe-app-τ
              [(τ ...)
-              #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
-              #'(τ-exp ...)]))]))
+              #:with (τ-exp ...) (stx-map (λ (t) (eval-τ t tvs)) #'(τ ...))
+              #'(τ-exp ...)]))])))
 
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
@@ -267,7 +278,18 @@
 (define-for-syntax (mk-pred x) (format-id x "~a?" x))
 (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
 
-       
+(define-for-syntax (subst τ x e)
+  (syntax-parse e
+    [y:id
+     #:when (free-identifier=? e x)
+     τ]
+    [y:id #'y]
+    [(esub ...)
+     #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
+     #'(esub_subst ...)]))
+(define-for-syntax (substs τs xs e)
+  (stx-fold subst e τs xs))
+  
 ;; type environment -----------------------------------------------------------
 #;(begin-for-syntax