commit bec3be8b22bfe3982a64a1c19f68c847f9b6ccb1
parent f703520367cd1f66c5034be68de9668e24d1a7d4
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 3 Jun 2015 19:25:31 -0400
use parameters to implement extensible type relations (instead of eval)
Diffstat:
10 files changed, 103 insertions(+), 49 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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))
