commit 1b0179d0663e832744e6d2f24a692e854c62146b
parent 5c058bffd600475db357596202a9b0e98bbb5740
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 28 May 2015 16:01:09 -0400
add sysf; fix begin splicing problem
Diffstat:
4 files changed, 91 insertions(+), 32 deletions(-)
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,25 @@
+2015-05-28
+Problem: how to represent \forall types
+1) (Racket) functions
+- this gets the most linguistic reuse (is this true?)
+- but this does not allow equality comparisons
+- unless perhaps compare two foralls for equality by applying to the same tvar
+ - but these type vars would be unbound so it still wouldnt work without
+ adding a new special case
+2) syntax
+- easier to compare
+- but still need to manually implement alpha equality
+- would still require a special case for comparing the bodies, which have
+ unbound typevars
+
+Problem: begin in lambda body gets spliced
+- results in combined syntax properties, eg types
+Solution:
+- wrap lambda body with #%expression to indicate expression, ie non-splicing,
+ begin
+
+Previous: -----------------
+
macro system requirements:
- depth-first expansion, i.e., localexpand, and stop-lists
- language form hooks, e.g., #%app, etc
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
@@ -21,6 +21,11 @@
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
+(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
;;ascription
(typecheck-fail (ann 1 : Bool))
diff --git a/tapl/tests/sysf-tests.rkt b/tapl/tests/sysf-tests.rkt
@@ -2,6 +2,34 @@
(require "rackunit-typechecking.rkt")
(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int))
+(check-type (inst (Λ (t) 1) Bool) : Int)
+; first inst should be discarded
+(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))
+
+;; 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))))
+(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
+ (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)
+ : 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)))
+ : Int ⇒ 10)
+
;; previous tests -------------------------------------------------------------
(check-type 1 : Int)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -78,6 +78,7 @@
;(printf "~a\n" τ)
(or (string? (syntax-e τ))
(and (identifier? τ) (identifier-binding τ))
+ (and (stx-pair? τ) (equal? '∀ (syntax->datum (stx-car τ))))
(and (stx-pair? τ) (stx-andmap is-type? τ))))
;; ⊢ : Syntax Type -> Syntax
;; Attaches type τ to (expanded) expression e.
@@ -89,26 +90,24 @@
[(b:typed-binding ...)
#:with (x ...) #'(b.x ...)
#:with (τ ...) #'(b.τ ...)
- #:with
- ;; if e is (begin e1 ...), (e1 ...) will be spliced into expanded λ
- ;; (and begin will be dropped), so must handle that
- (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e_body+ ... e+)))
- (expand/df
- #`(λ (x ...)
- (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
+ ;; wrap e with #%expression to prevent splicing begins into lambda body
+ #:with ((~literal #%plain-lambda) xs+
+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2
+ ((~literal #%expression) e+))))
+ (expand/df
+ #`(λ (x ...)
+ (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+ (#%expression #,e))))
+;; print intermediate expansion -- for debugging
; #:with tmp
; (expand/df
; #`(λ (x ...)
-; (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
-; #:when (printf "~a\n" (syntax->datum #'tmp))
-; #:with (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+))) #'tmp
-
- ;; if e is (begin ...), types (ie syntax properties) of all begins
- ;; will be accumulated on e+, so only get the first type
- #:with τ_e (if (null? (syntax->list #'(e_body+ ...)))
- (typeof #'e+)
- (stx-car (typeof #'e+)))
- (list #'xs+ #'(begin e_body+ ... e+) #'τ_e)]
+; (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...)
+; (#%expression #,e))))
+; #:with ((~literal #%plain-lambda) xs+
+; (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2
+; ((~literal #%expression) e+)))) #'tmp
+ (list #'xs+ #'e+ (typeof #'e+))]
[([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)]))
; all xs are bound in the same scope
(define (infers/type-ctxt+erase ctxt es)
@@ -124,12 +123,9 @@
(list #'xs+ #'(e+ ...) (stx-map typeof #'(e+ ...)))]
[([x τ] ...) (infers/type-ctxt+erase #'([x : τ] ...) es)]))
- (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+erase e)
+ (define e+ (expand/df e))
+ (list e+ (eval-τ (typeof e+))))
(define (infer/tvs+erase e [tvs #'()])
(define-values (tvs+ e+)
(syntax-parse (expand/df #`(λ #,tvs #,e)) #:literals (#%expression)
@@ -138,9 +134,9 @@
(list tvs+ e+ (eval-τ (typeof e+) tvs)))
(define (infers+erase es)
(stx-map infer+erase es))
- (define (types=? τs1 τs2)
+ (define (types=? τs1 τs2 #:eval? [eval? #t])
(and (= (stx-length τs1) (stx-length τs2))
- (stx-andmap type=? τs1 τs2)))
+ (stx-andmap (λ (t1 t2) (type=? t1 t2 #:eval? eval?)) τs1 τs2)))
(define (same-types? τs)
(define τs-lst (syntax->list τs))
(or (null? τs-lst)
@@ -185,21 +181,29 @@
;; type=? : Type Type -> Boolean
;; Indicates whether two types are equal
- (define (type=? τa τb)
+ (define (type=? τa τb #:eval? [eval? #t])
;; expansion, and thus eval-τ is idempotent,
;; so should be ok to expand even if τa or τb are already expanded
- (define τ1 (eval-τ τa))
- (define τ2 (eval-τ τb))
-; (printf "t1: ~a => ~a\n" (syntax->datum τa) (syntax->datum τ1))
-; (printf "t2: ~a => ~a\n" (syntax->datum τb) (syntax->datum τ2))
- (syntax-parse #`(#,τ1 #,τ2)
+; (printf "t1: ~a => " (syntax->datum τa))
+ (define τ1 (if eval? (eval-τ τa) τa))
+; (printf "~a\n" (syntax->datum τ1))
+; (printf "t2: ~a => " (syntax->datum τb))
+ (define τ2 (if eval? (eval-τ τb) τb))
+; (printf "~a\n" (syntax->datum τ2))
+ (syntax-parse #`(#,τ1 #,τ2) #:datum-literals (∀)
; → should not be datum literal;
; adding a type constructor should extend type equality
; #:datum-literals (→)
[(x:id y:id) (free-identifier=? τ1 τ2)]
[(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
+ [((∀ (x ...) t1) (∀ (y ...) t2))
+ #:when (= (stx-length #'(x ...)) (stx-length #'(y ...)))
+ #:with (z ...) (generate-temporaries #'(x ...))
+ (type=? (substs #'(z ...) #'(x ...) #'t1)
+ (substs #'(z ...) #'(y ...) #'t2)
+ #:eval? #f)]
[((τ1 ...) (τ2 ...))
- (types=? #'(τ1 ...) #'(τ2 ...))]
+ (types=? #'(τ1 ...) #'(τ2 ...) #:eval? eval?)]
#;[((x ... → x_out) (y ... → y_out))
(and (type=? #'x_out #'y_out)
(stx-andmap type=? #'(x ...) #'(y ...)))]
