commit ef74f682705c5155ee3e14365c7f1c873bc5736c
parent 7e9d8cd1e01491860517b6210601d58c19a80653
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 11 Jun 2015 16:46:50 -0400
fomega with kinds, no operator abstraction yet
Diffstat:
7 files changed, 160 insertions(+), 39 deletions(-)
diff --git a/tapl/README.md b/tapl/README.md
@@ -12,4 +12,4 @@ A file extends its immediate parent file.
- stlc+sub.rkt
- stlc+rec+sub.rkt (also pull in tup from stlc+var.rkt)
- sysf.rkt
- - Fomega.rkt
-\ No newline at end of file
+ - fomega.rkt
+\ No newline at end of file
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -1,13 +1,117 @@
#lang racket/base
(require "typecheck.rkt")
-(require (except-in "sysf.rkt" #%app)
- (prefix-in stlc: (only-in "sysf.rkt" #%app)))
-(provide (rename-out [stlc:#%app #%app]))
-(provide (except-out (all-from-out "sysf.rkt") stlc:#%app))
-
+(require (except-in "sysf.rkt" #%app λ + Λ inst Int → ∀ eval-τ type=?)
+ (prefix-in sysf: (only-in "sysf.rkt" Int → ∀ eval-τ type=?)))
+(provide (rename-out [app/tc #%app] [λ/tc λ]))
+(provide (except-out (all-from-out "sysf.rkt")
+ sysf:Int sysf:→ sysf:∀
+ (for-syntax sysf:type=? sysf:eval-τ)))
+(provide Int → ∀ inst Λ
+ (for-syntax eval-τ type=?))
+
;; System F_omega
;; Type relation:
;; Types:
;; - types from sysf.rkt
;; Terms:
;; - terms from sysf.rkt
+
+(begin-for-syntax
+ ;; Extend to handle ∀ with type annotations
+ (define (eval-τ τ [tvs #'()])
+ (syntax-parse τ
+ [((~literal ∀) (b:typed-binding ...) t-body)
+ #`(∀ (b ...) #,((current-τ-eval) #'t-body (stx-append tvs #'(b.x ...))))]
+ ;; need to manually handle type constructors now since they are macros
+ [((~literal →) t ...)
+ #`(→ #,@(stx-map (λ (ty) ((current-τ-eval) ty tvs)) #'(t ...)))]
+ [_ (sysf:eval-τ τ tvs)]))
+ (current-τ-eval eval-τ)
+
+ ;; extend to handle ∀ with kind annotations
+ (define (type=? τ1 τ2)
+ (syntax-parse (list τ1 τ2) #:literals (∀)
+ [((∀ (a:typed-binding ...) t1:type) (∀ (b:typed-binding ...) t2:type))
+ #:when (= (stx-length #'(a ...)) (stx-length #'(b ...)))
+ #:with (z ...) (generate-temporaries #'(a ...))
+ #:when (typechecks? #'(a.τ ...) #'(b.τ ...))
+ ((current-type=?) (substs #'(z ...) #'(a.x ...) #'t1)
+ (substs #'(z ...) #'(b.x ...) #'t2))]
+ [_ (sysf:type=? τ1 τ2)]))
+ (current-type=? type=?)
+ (current-typecheck-relation type=?))
+
+(define-base-type ★)
+(define-type-constructor ⇒)
+
+;; for now, handle kind checking in the types themselves
+;; TODO: move kind checking to a common place (like #%app)?
+;; when expanding: check and erase kinds
+
+(define-syntax Int (syntax-parser [x:id (⊢ #'sysf:Int #'★)]))
+
+;; → in Fω is not first-class, can't pass it around
+(define-syntax (→ stx)
+ (syntax-parse stx
+ [(_ τ ... τ_res)
+ #:with ([τ- k] ... [τ_res- k_res]) (infers+erase #'(τ ... τ_res))
+ #:when (typecheck? #'k_res #'★)
+ #:when (same-types? #'(k ... k_res))
+ (⊢ #'(sysf:→ τ- ... τ_res-) #'★)]))
+
+(define-syntax (∀ stx)
+ (syntax-parse stx
+ [(∀ (b:typed-binding ...) τ)
+ #:with (tvs- τ- k) (infer/type-ctxt+erase #'(b ...) #'τ)
+ #:when (typecheck? #'k #'★)
+ (⊢ #'(sysf:∀ tvs- τ-) #'★)]))
+
+(define-syntax (Λ stx)
+ (syntax-parse stx
+ [(_ (b:typed-binding ...) e)
+ #:with ((tv- ...) e- τ) (infer/type-ctxt+erase #'(b ...) #'e)
+ (⊢ #'e- #'(∀ ([tv- : b.τ] ...) τ))]))
+(define-syntax (inst stx)
+ (syntax-parse stx
+ [(_ e τ ...)
+ #:with ([τ- k] ...) (infers+erase #'(τ ...))
+ #:with (e- τ_e) (infer+erase #'e)
+ #:with ((~literal ∀) (b:typed-binding ...) τ_body) #'τ_e
+ #:when (typechecks? #'(k ...) #'(b.τ ...))
+ (⊢ #'e- (substs #'(τ ...) #'(b.x ...) #'τ_body))]))
+
+;; must override #%app and λ and primops to use new →
+;; TODO: parameterize →?
+
+(define-primop + : (→ Int Int Int))
+
+(define-syntax (λ/tc stx)
+ (syntax-parse stx
+ [(_ (b:typed-binding ...) e)
+ #:when (andmap ★? (stx-map (λ (t) (typeof (expand/df t))) #'(b.τ ...)))
+ #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
+ (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
+
+(define-syntax (app/tc stx)
+ (syntax-parse stx #:literals (→)
+ [(_ e_fn e_arg ...)
+ #:with (e_fn- ((~literal →) τ ... τ_res)) (infer+erase #'e_fn)
+; #:fail-unless (→? #'τ_fn)
+; (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
+; (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
+; #:with (→ τ ... τ_res) #'τ_fn
+ #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ ...))
+ (string-append
+ (format
+ "Wrong number of args given to function ~a, or args have wrong type:\ngiven: "
+ (syntax->datum #'e_fn))
+ (string-join
+ (map (λ (e+τ) (format "~a : ~a" (car e+τ) (cadr e+τ))) (syntax->datum #'([e_arg τ_arg] ...)))
+ ", ")
+ "\nexpected arguments with type: "
+ (string-join
+ (map (λ (x) (format "~a" x)) (syntax->datum #'(τ ...)))
+ ", "))
+ (⊢ #'(#%app e_fn- e_arg- ...) #'τ_res)]))
+
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -34,6 +34,8 @@
;; type equality = structurally recursive identifier equality
;; structurally checks for free-identifier=?
(define (type=? τ1 τ2)
+; (printf "t1 = ~a\n" (syntax->datum τ1))
+; (printf "t2 = ~a\n" (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(x:id y:id) (free-identifier=? τ1 τ2)]
[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))]
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -24,8 +24,6 @@
(begin-for-syntax
;; Extend to handle ∀, skip typevars
(define (eval-τ τ [tvs #'()])
-; (printf "~a\n" (syntax->datum τ))
-; (printf "tvs: ~a\n" tvs)
(syntax-parse τ
[x:id #:when (stx-member τ tvs) τ]
[((~literal ∀) ts t-body)
@@ -47,7 +45,7 @@
;; extend to handle ∀
(define (type=? τ1 τ2)
(syntax-parse (list τ1 τ2) #:literals (∀)
- [((∀ (x ...) t1) (∀ (y ...) t2))
+ [((∀ (x:id ...) t1) (∀ (y:id ...) t2))
#:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
#:with (z ...) (generate-temporaries #'(x ...))
((current-type=?) (substs #'(z ...) #'(x ...) #'t1)
@@ -59,11 +57,12 @@
(define-syntax (Λ stx)
(syntax-parse stx
[(_ (tv:id ...) e)
- #:with (tvs+ e- τ) (infer/tvs+erase #'e #'(tv ...))
- (⊢ #'e- #'(∀ tvs+ τ))]))
+ #: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))]))
-\ No newline at end of file
+ #:with (τ+ ...) (stx-map (current-τ-eval) #'(τ ...))
+ (⊢ #'e- (substs #'(τ+ ...) #'(tv ...) #'τ_body))]))
+\ No newline at end of file
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
@@ -1,42 +1,57 @@
#lang s-exp "../fomega.rkt"
(require "rackunit-typechecking.rkt")
-(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2)))))
+(check-type Int : ★)
+(check-type (→ Int Int) : ★)
+(typecheck-fail (→ →))
-(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4)))))
+(typecheck-fail (λ ([x : (→ →)]) x))
-(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y))))
- : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
+(typecheck-fail (∀ (t) t)) ; missing kind annotation
+(check-type (∀ ([t : ★]) t) : ★)
+(check-type (∀ ([→ : ★]) →) : ★) ; should be ok
+(check-type (∀ ([t : ★]) (∀ ([s : ★]) (→ t s))) : ★)
+(check-type (∀ ([t : ★] [s : ★]) (→ t s)) : ★)
+;(check-type (∀ ([t : (⇒ ★ ★)] [s : ★]) (t s)) : ★) ; doesnt work yet
+(typecheck-fail (∀ (t) (→ →)))
-(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ (t) 1) Bool) : Int)
+;; sysf tests wont work, must be augmented with kinds
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2)))))
+
+(check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y))))
+ : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4)))))
+
+(check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int)
; first inst should be discarded
-(check-type (inst (inst (Λ (t) (Λ (t) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
+(check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
; second inst is discarded
-(check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
+(check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int))
;; polymorphic arguments
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))
-(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s)))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s))))
-(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u))))
-(check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u))))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t)))
+(check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s)))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s))))
+(check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u))))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u))))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x)))
(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u)))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u)))
(check-type
- (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int))
+ (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int))
(check-type
- ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10)
+ ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10)
: Int ⇒ 10)
-(check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int)))
-(check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int))
-(check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10))
- (Λ (s) (λ ([y : s]) y)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)))
+(check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int))
+(check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10))
+ (Λ ([s : ★]) (λ ([y : s]) y)))
: Int ⇒ 10)
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
@@ -8,6 +8,7 @@
(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 (λ ([x : (→ →)]) x) : (→ (→ →) (→ →))) ; TODO: should this fail?
(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
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -11,7 +11,7 @@
: (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4)))))
(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
-(check-type (inst (Λ (t) 1) Bool) : Int)
+(check-type (inst (Λ (t) 1) (→ Int Int)) : Int)
; first inst should be discarded
(check-type (inst (inst (Λ (t) (Λ (t) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int))
; second inst is discarded
