diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index 576c4e7..4ce7943 100644 --- a/tapl/ext-stlc.rkt +++ b/tapl/ext-stlc.rkt @@ -68,7 +68,7 @@ #:fail-unless (Bool? #'τ_tst) (format "given non-Bool test: ~a\n" (syntax->datum #'e_tst)) #:with (e1- τ1) (infer+erase #'e1) #:with (e2- τ2) (infer+erase #'e2) - #:when (type=? #'τ1 #'τ2) + #:when ((current-type=?) #'τ1 #'τ2) (⊢ #'(if e_tst- e1- e2-) #'τ1)])) (define-base-type Unit) @@ -94,7 +94,7 @@ (syntax-parse stx #:datum-literals (:) [(_ e : ascribed-τ) #:with (e- τ) (infer+erase #'e) - #:fail-unless (type=? #'τ #'ascribed-τ) + #:fail-unless ((current-type=?) #'τ #'ascribed-τ) (format "~a does not have type ~a\n" (syntax->datum #'e) (syntax->datum #'ascribed-τ)) (⊢ #'e- #'ascribed-τ)])) diff --git a/tapl/notes.txt b/tapl/notes.txt index 674829d..9241b36 100644 --- a/tapl/notes.txt +++ b/tapl/notes.txt @@ -18,6 +18,30 @@ Solution: - wrap lambda body with #%expression to indicate expression, ie non-splicing, begin +2015-05-29 +Notes: locally-nameless representation of lambdas (and other binding terms) +- syntactically distinguishes bound names vs free vars +- combination of debruijn (nameless) for bound vars and names +- simplifies implementation of capture avoiding substitution + - I already get around by using Racket's identifiers and free-identifier= + to easily implement capture-avoiding subst +- debruijn indices for boundvars avoids having to convert to canonical form + to compare for alpha-equal +- using names for free vars avoids "shifting" of indices when adding or + removing binders, ie free vars dont rely on context +- two main operations: + - open: converts some bound vars to free vars + - eg subst into lambda body + - conversion and subst can be done in one pass? + - close: converts some free vars to bound vars + - eg wrapping a term in a lambda + - similar to subst + - both operations involve traversing the term + - but can do straight-subst (instead of renaming subst) because + shadowing is not possible +- multiple binders are more complicated + - require both depth and offset index + Previous: ----------------- macro system requirements: diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index b5d9547..4534286 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -45,7 +45,7 @@ [(_ e1 e2) #:with (e1- τ1) (infer+erase #'e1) #:with (e2- ((~literal List) τ2)) (infer+erase #'e2) - #:when (type=? #'τ1 #'τ2) + #:when ((current-type=?) #'τ1 #'τ2) (⊢ #'(cons e1- e2-) #'(List τ1))])) (define-syntax (isnil stx) (syntax-parse stx diff --git a/tapl/stlc+rec+sub.rkt b/tapl/stlc+rec+sub.rkt index b17c732..57183ef 100644 --- a/tapl/stlc+rec+sub.rkt +++ b/tapl/stlc+rec+sub.rkt @@ -2,15 +2,15 @@ (require (for-syntax racket/base syntax/parse racket/string syntax/stx racket/set "stx-utils.rkt") "typecheck.rkt") -(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=? types=? same-types?) +(require (except-in "stlc+sub.rkt" #%app #%datum sub? type=?) (prefix-in stlc: (only-in "stlc+sub.rkt" #%app #%datum sub?)) (except-in "stlc+var.rkt" #%app #%datum +) - (prefix-in var: (only-in "stlc+var.rkt" #%datum))) + (prefix-in var: (only-in "stlc+var.rkt" #%datum type=?))) (provide (rename-out [stlc:#%app #%app] [datum/tc #%datum])) (provide (except-out (all-from-out "stlc+sub.rkt") stlc:#%app stlc:#%datum (for-syntax stlc:sub?)) - (except-out (all-from-out "stlc+var.rkt") var:#%datum)) + (except-out (all-from-out "stlc+var.rkt") var:#%datum (for-syntax var:type=?))) (provide (for-syntax sub?)) ;; Simply-Typed Lambda Calculus, plus subtyping, plus records @@ -36,7 +36,7 @@ (syntax-parser [(l:str τl) #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) - (sub? #'τk_match #'τl)]) + ((current-sub?) #'τk_match #'τl)]) #'([l τl] ...))] [((∨ [k:str τk] ...) (∨ [l:str τl] ...)) #:when (subset? (stx-map syntax-e (syntax->list #'(l ...))) @@ -45,7 +45,8 @@ (syntax-parser [(l:str τl) #:with (k_match τk_match) (str-stx-assoc #'l #'([k τk] ...)) - (sub? #'τk_match #'τl)]) + ((current-sub?) #'τk_match #'τl)]) #'([l τl] ...))] [_ #f]) - (stlc:sub? τ1 τ2)))) \ No newline at end of file + (stlc:sub? τ1 τ2))) + (current-sub? sub?)) \ No newline at end of file diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt index d27bab0..543431f 100644 --- a/tapl/stlc+sub.rkt +++ b/tapl/stlc+sub.rkt @@ -2,7 +2,7 @@ (require (for-syntax racket/base syntax/parse racket/string "stx-utils.rkt") "typecheck.rkt") -(require (except-in "stlc+lit.rkt" #%app #%datum +) +(require (except-in "stlc+lit.rkt" #%datum + #%app) (prefix-in stlc: (only-in "stlc+lit.rkt" #%datum))) (provide (rename-out [app/tc #%app] [datum/tc #%datum])) (provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%datum)) @@ -40,19 +40,29 @@ (begin-for-syntax (define (sub? τ1 τ2) - (or (type=? τ1 τ2) - (type=? #'Top τ2) - (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num) - [(Nat τ) (sub? #'Int #'τ)] - [(Int τ) (sub? #'Num #'τ)] - [(τ Num) (sub? #'τ #'Int)] - [(τ Int) (sub? #'τ #'Nat)] + (or ((current-type=?) τ1 τ2) + #;(and (identifier? τ2) (free-identifier=? τ2 #'Top)) + (syntax-parse (list τ1 τ2) #:literals (→ Nat Int Num Top) + [(_ Top) #t] + #;[(t1:id t2:id) (free-identifier=? #'t1 #'t2)] + [(Nat τ) ((current-sub?) #'Int #'τ)] + [(Int τ) ((current-sub?) #'Num #'τ)] + [(τ Num) ((current-sub?) #'τ #'Int)] + [(τ Int) ((current-sub?) #'τ #'Nat)] [((→ s1 ... s2) (→ t1 ... t2)) (and (subs? #'(t1 ...) #'(s1 ...)) - (sub? #'s2 #'t2))] + ((current-sub?) #'s2 #'t2))] [_ #f]))) - (define (subs? τs1 τs2) (stx-andmap (eval-syntax (datum->syntax τs1 'sub?)) τs1 τs2))) - ;(define (subs? ts1 ts2) (stx-andmap (λ (t1 t2) (printf "~a <: ~a: ~a\n" (syntax->datum t1) (syntax->datum t2) (sub? t1 t2)) (sub? t1 t2)) ts1 ts2))) + (current-sub? sub?) + (define (subs? τs1 τs2) (stx-andmap (current-sub?) τs1 τs2))) + +#;(define-syntax (app/tc stx) + (syntax-parse stx + [(_ x ...) + #:with res + (parameterize ([current-type=? (current-sub?)]) + (local-expand #'(stlc:#%app x ...) 'expression null)) + #'res])) (define-syntax (app/tc stx) (syntax-parse stx #:literals (→) diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt index 0fd6a05..ca74ced 100644 --- a/tapl/stlc+var.rkt +++ b/tapl/stlc+var.rkt @@ -4,14 +4,15 @@ "stx-utils.rkt" "typecheck.rkt") (for-meta 2 racket/base syntax/parse racket/syntax) "typecheck.rkt") -(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let)) - (except-in "stlc+tup.rkt" #%app λ tup proj let type=? types=? same-types?)) +(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let type=?)) + (except-in "stlc+tup.rkt" #%app λ tup proj let type=?)) (provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let])) (provide (except-out (all-from-out "stlc+tup.rkt") - stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj)) + stlc:#%app stlc:λ stlc:let stlc:tup stlc:proj + (for-syntax stlc:type=?))) ;(provide define-type-alias define-variant module quote submod) (provide tup proj var case) -(provide (for-syntax type=? types=? same-types?)) +(provide (for-syntax type=?)) ;; Simply-Typed Lambda Calculus, plus variants @@ -34,19 +35,21 @@ (define (type=? τ1 τ2) (syntax-parse (list τ1 τ2) [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] - [(x:id y:id) (free-identifier=? τ1 τ2)] - [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] - [_ #f])) + [_ (stlc:type=? τ1 τ2)] + #;[(x:id y:id) (free-identifier=? τ1 τ2)] + #;[((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] + #;[_ #f])) + (current-type=? type=?) ;; redefine these to use the new type=? ;; type equality = structurally recursive identifier equality ;; uses the type=? in the context of τs1 instead of here - (define (types=? τs1 τs2) + #;(define (types=? τs1 τs2) (and (= (stx-length τs1) (stx-length τs2)) (stx-andmap type=? τs1 τs2))) ;; uses the type=? in the context of τs instead of here - (define (same-types? τs) + #;(define (same-types? τs) (define τs-lst (syntax->list τs)) (or (null? τs-lst) (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))) @@ -94,7 +97,7 @@ #:with (∨ (l_τ τ_l) ...) #'τ+ #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...)) #:with (e- τ_e) (infer+erase #'e) - #:when (type=? #'τ_match #'τ_e) + #:when ((current-type=?) #'τ_match #'τ_e) (⊢ #'(list l e) #'τ+)])) (define-syntax (case stx) (syntax-parse stx #:datum-literals (of =>) @@ -104,7 +107,8 @@ #:with (∨ (l_x τ_x) ...) #'τ_e #:fail-when (null? (syntax->list #'(l ...))) "no clauses" #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses" - #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses is not exhaustive" +; #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" + #:fail-unless (types=? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" #:with (((x-) e_l- τ_el) ...) (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...)) #:fail-unless (same-types? #'(τ_el ...)) "branches have different types" diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index 4e0c906..368a493 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -27,17 +27,19 @@ [(x:id y:id) (free-identifier=? τ1 τ2)] [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] [_ #f])) - + + (current-type=? type=?) + ;; type equality = structurally recursive identifier equality ;; uses the type=? in the context of τs1 instead of here (define (types=? τs1 τs2) (and (= (stx-length τs1) (stx-length τs2)) - (stx-andmap type=? τs1 τs2))) + (stx-andmap (current-type=?) τs1 τs2))) ;; uses the type=? in the context of τs instead of here (define (same-types? τs) (define τs-lst (syntax->list τs)) (or (null? τs-lst) - (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))) + (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst))))) (define-syntax (λ/tc stx) (syntax-parse stx @@ -54,7 +56,8 @@ (syntax->datum #'e_fn) (syntax->datum #'τ_fn)) #:with (→ τ ... τ_res) #'τ_fn #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) - #:fail-unless ((eval-syntax (datum->syntax #'e_fn 'types=?)) #'(τ ...) #'(τ_arg ...)) +; #:fail-unless ((eval-syntax (datum->syntax #'e_fn 'types=?)) #'(τ ...) #'(τ_arg ...)) + #:fail-unless (types=? #'(τ_arg ...) #'(τ ...)) (string-append (format "Wrong number of args given to function ~a, or args have wrong type:\ngiven: " diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt index fe0dc8a..0235ce6 100644 --- a/tapl/sysf.rkt +++ b/tapl/sysf.rkt @@ -2,12 +2,12 @@ (require (for-syntax racket/base syntax/parse "stx-utils.rkt") "typecheck.rkt") -(require (except-in "stlc+lit.rkt" #%app type=? types=? same-types?) - (prefix-in stlc: (only-in "stlc+lit.rkt" #%app))) +(require (except-in "stlc+lit.rkt" #%app type=?) + (prefix-in stlc: (only-in "stlc+lit.rkt" #%app type=?))) (provide (rename-out [stlc:#%app #%app])) -(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app)) +(provide (except-out (all-from-out "stlc+lit.rkt") stlc:#%app (for-syntax stlc:type=?))) (provide Λ inst) -(provide (for-syntax type=? types=? same-types?)) +(provide (for-syntax type=?)) ;; System F @@ -34,20 +34,22 @@ #:with (z ...) (generate-temporaries #'(x ...)) (type=? (substs #'(z ...) #'(x ...) #'t1) (substs #'(z ...) #'(y ...) #'t2))] - [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] - [(x:id y:id) (free-identifier=? τ1 τ2)] - [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] - [_ #f])) + [_ (stlc:type=? τ1 τ2)])) + (current-type=? type=?) +; [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))] +; [(x:id y:id) (free-identifier=? τ1 τ2)] +; [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] +; [_ #f])) ;; redefine these to use the new type=? ;; type equality = structurally recursive identifier equality ;; uses the type=? in the context of τs1 instead of here - (define (types=? τs1 τs2) + #;(define (types=? τs1 τs2) (and (= (stx-length τs1) (stx-length τs2)) (stx-andmap type=? τs1 τs2))) ;; uses the type=? in the context of τs instead of here - (define (same-types? τs) + #;(define (same-types? τs) (define τs-lst (syntax->list τs)) (or (null? τs-lst) (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))) diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index a6accf1..bf12d0d 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -4,6 +4,11 @@ "../typecheck.rkt") (provide (all-defined-out)) +(define-for-syntax (type=? t1 t2) + (if (current-sub?) + ((current-sub?) t1 t2) + ((current-type=?) t1 t2))) + (define-syntax (check-type stx) (syntax-parse stx #:datum-literals (:) [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)] @@ -12,8 +17,9 @@ #:with τ-expected+ (eval-τ #'τ-expected) #:fail-unless ;; use subtyping if it's bound in the context of #'e - (with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'τ-expected+))]) - ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected+)) + #;(with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'τ-expected+))]) + ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'τ-expected+)) + (type=? #'τ #'τ-expected+) (format "Expression ~a [loc ~a:~a] has type ~a, expected ~a" (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e) @@ -26,8 +32,9 @@ #:with τ (typeof (expand/df #'e)) #:with not-τ+ (eval-τ #'not-τ) #:fail-when - (with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'not-τ+))]) + #;(with-handlers ([exn:fail? (λ _ ((eval-syntax (datum->syntax #'e 'type=?)) #'τ #'not-τ+))]) ((eval-syntax (datum->syntax #'e 'sub?)) #'τ #'not-τ+)) + (type=? #'τ #'not-τ+) (format "(~a:~a) Expression ~a should not have type ~a" (syntax-line stx) (syntax-column stx) diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 4e44aea..d0b59c3 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -108,6 +108,9 @@ (syntax-parse (expand/df #`(λ #,tvs (#%expression #,e))) #:literals (#%expression) [(lam tvs+ (#%expression e+)) (list #'tvs+ #'e+ (typeof #'e+))])) + (define current-type=? (make-parameter #f)) + (define current-sub? (make-parameter #f)) + ; ;; type equality = structurally recursive identifier equality ; (define (types=? τs1 τs2) ; (and (= (stx-length τs1) (stx-length τs2))