diff --git a/tapl/notes.txt b/tapl/notes.txt index faab94b..a838475 100644 --- a/tapl/notes.txt +++ b/tapl/notes.txt @@ -1,3 +1,18 @@ +2015-07-25 +Problem: types and terms occur in the same space +What to do about "valid" terms like \x:(void).x or \x:1.x ? +- adding an is-type? predicate that checks shape and other things will only + partially work because things like \x:(void).x will still pass +- define types in a different phase + - wont work because you need terms to do type checking so the terms have to be + in the same phase +- write a separate parser for types + - wont work because still cant tell with a valid binding is a term or type, + eg, \x:(void).x still passes + - unless you hard-code the type names, but then it's not extensible? + - can extend the reader but then you have code duplication? +- wrap types with a tag, like #%type ? + 2015-07-24 When to canonicalize (ie, eval) types: - calling eval before matching is too late diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index ee1219f..cbea98b 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -1,7 +1,7 @@ #lang racket/base (require "typecheck.rkt") (provide (rename-out [λ/tc λ] [app/tc #%app])) -(provide (for-syntax type=? types=? same-types? current-type=? type-eval)) +(provide (for-syntax type=? #;types=? #;same-types? current-type=? type-eval)) (provide #%module-begin #%top-interaction #%top require) ; from racket ;; Simply-Typed Lambda Calculus @@ -32,14 +32,14 @@ [(x:id y:id) (free-identifier=? τ1 τ2)] [((τa ...) (τb ...)) (types=? #'(τa ...) #'(τb ...))] [_ #f])) - + (define (types=? τs1 τs2) + (and (stx-length=? τs1 τs2) + (stx-andmap (current-type=?) τs1 τs2))) + (define current-type=? (make-parameter type=?)) (current-typecheck-relation type=?) - (define (types=? τs1 τs2) - (and (= (stx-length τs1) (stx-length τs2)) - (stx-andmap (current-type=?) τs1 τs2))) - (define (same-types? τs) + #;(define (same-types? τs) (define τs-lst (syntax->list τs)) (or (null? τs-lst) (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst))))) @@ -70,13 +70,13 @@ ; [( τ pat) ; #:with -(define-tycon (→ τ_in ... τ_out)) +(define-type-constructor (→ τ_in ... τ_out)) (define-syntax (λ/tc stx) (syntax-parse stx [(_ (b:typed-binding ...) e) #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e) - (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))])) + (⊢ #'(λ xs- e-) #`(→ b.τ ... #,(syntax-track-origin #'(#%type τ_res) #'τ_res #'λ)))])) (define-syntax (app/tc stx) (syntax-parse stx @@ -106,17 +106,19 @@ (format "Arguments to function ~a have wrong type(s), " (syntax->datum #'e_fn)) "or wrong number of arguments:\n" - "given: " + "given:\n" (string-join (map - (λ (e t) (format "~a : ~a" e t)) + (λ (e t) (format " ~a : ~a" e t)) (syntax->datum #'(e_arg ...)) - (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...)))) - ", ") + (stx-map type->str #'(τ_arg ...)) + #;(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...)))) + "\n") "\n" (format "expected ~a arguments with type(s): " (stx-length #'(τ_in ...))) (string-join - (map ~a (syntax->datum #`#,(stx-map get-orig #'(τ_in ...)))) + (stx-map type->str #'(τ_in ...)) + #;(map ~a (syntax->datum #`#,(stx-map get-orig #'(τ_in ...)))) ", ")) (⊢ #'(#%app e_fn- e_arg- ...) #'τ_out)])) diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index 8f7b9a2..33426ef 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -7,7 +7,7 @@ [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)] [(_ e : τ-expected:type) #:with τ (typeof (expand/df #'e)) - #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected)) + #:fail-unless (typecheck? #'τ #'τ-expected.norm) (format "Expression ~a [loc ~a:~a] has type ~a, expected ~a" (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e) @@ -18,7 +18,7 @@ (syntax-parse stx #:datum-literals (:) [(_ e : not-τ:type) #:with τ (typeof (expand/df #'e)) - #:fail-when (typecheck? #'τ ((current-type-eval) #'not-τ.norm)) + #:fail-when (typecheck? #'τ #'not-τ.norm) (format "(~a:~a) Expression ~a should not have type ~a" (syntax-line stx) (syntax-column stx) @@ -38,8 +38,8 @@ (unless (regexp-match? (syntax-e #'msg-pat) (exn-message ex)) (printf (string-append - "ERROR: wrong err msg produced by expression ~v:\n" - "expected msg matching pattern ~v, got:\n ~v") + "ERROR-MSG ERROR: wrong err msg produced by expression ~v:\n" + "EXPECTED:\nmsg matching pattern ~v,\nGOT:\n~v\n") (syntax->datum #'e) (syntax-e #'msg-pat) (exn-message ex))) (raise ex))]) (expand/df #'e))) diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt index fd86b3b..b3be9f7 100644 --- a/tapl/tests/stlc+lit-tests.rkt +++ b/tapl/tests/stlc+lit-tests.rkt @@ -25,14 +25,14 @@ (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) (typecheck-fail ((λ ([x : Bool]) x) 1) - #:with-msg "Bool: unbound identifier") + #:with-msg "not a valid type: Bool") (typecheck-fail (λ ([x : (→ Bool Bool)]) x) - #:with-msg "Bool: unbound identifier") + #:with-msg "not a valid type: Bool") (typecheck-fail (λ ([x : Bool]) x) - #:with-msg "Bool: unbound identifier") + #:with-msg "not a valid type: Bool") (typecheck-fail (λ ([f : Int]) (f 1 2)) #:with-msg - "didn't match expected type pattern: \\(→ τ_in ... τ_out\\)") + "Expected type with pattern: \\(→ τ_in ... τ_out\\), got: Int") (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) : (→ (→ Int Int Int) Int Int Int)) @@ -41,18 +41,18 @@ (typecheck-fail (+ 1 (λ ([x : Int]) x)) #:with-msg - "Arguments to function \\+ have wrong type.+given: 1 : Int.+→.+expected 2 arguments with type.+Int\\, Int") + "Arguments to function \\+ have wrong type.+given:\n 1 : Int.+(→ Int Int).+expected 2 arguments with type.+Int\\, Int") (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x)) #:with-msg - "Arguments to function \\+ have wrong type.+given: x.+→.+expected 2 arguments with type.+Int\\, Int") + "Arguments to function \\+ have wrong type.+given:.+(→ Int Int).+expected 2 arguments with type.+Int\\, Int") (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1) #:with-msg "Arguments to function.+have.+wrong number of arguments") (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) -(typecheck-fail (λ ([x : (→ 1 2)]) x) - #:with-msg "Improperly formatted type annotation") -(typecheck-fail (λ ([x : 1]) x) - #:with-msg "Improperly formatted type annotation") +(typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a valid type") +(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type") +(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type") +(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type") diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index e4aadbb..03190b2 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -27,10 +27,20 @@ (syntax-parse stx [(_ τ:id) #:with τ? (format-id #'τ "~a?" #'τ) + #:with τ-internal (generate-temporary #'τ) #'(begin (provide τ (for-syntax τ?)) - (define τ (void)) - (define-for-syntax (τ? τ1) (typecheck? τ1 #'τ)))])) + (define τ-internal + (λ () (raise (exn:fail:type:runtime + (format "~a: Cannot use type at run time" 'τ) + (current-continuation-marks))))) + (define-syntax (τ stx) + (syntax-parse stx + [x:id (add-orig #'(#%type (τ-internal)) #'τ)])) + (define-for-syntax (τ? t) + (syntax-parse t + [((~literal #%type) ((~literal #%plain-app) ty)) + (typecheck? #'ty #'τ-internal)])))])) (struct exn:fail:type:runtime exn:fail:user ()) @@ -39,8 +49,16 @@ (define origs (or (syntax-property orig 'orig) null)) (syntax-property stx 'orig (cons orig origs))) (define (get-orig τ) - (car (reverse (or (syntax-property τ 'orig) (list τ)))))) - + (car (reverse (or (syntax-property τ 'orig) (list τ))))) + (define (type->str ty) + (define τ (get-orig ty)) + (cond + [(identifier? τ) (symbol->string (syntax->datum τ))] + [(stx-pair? τ) (string-join (stx-map type->str τ) + #:before-first "(" + #:after-last ")")] + [else (format "~a" (syntax->datum τ))]))) + (begin-for-syntax (define-syntax (match-type stx) (syntax-parse stx @@ -57,7 +75,7 @@ #:msg "~a didn't match expected type pattern: ~a" ty pat)])]))) -(define-syntax define-tycon +(define-syntax define-type-constructor (syntax-parser [(_ (τ:id . pat)) #:with τ-match (format-id #'τ "~a-match" #'τ) @@ -73,8 +91,8 @@ (define (τ-match ty) (or (match-type ty tycon pat-class) (type-error #:src ty - #:msg "~a didn't match expected type pattern: ~a" - ty (quote-syntax (τ . pat)))) + #:msg "Expected type with pattern: ~a, got: ~a" + (quote-syntax (τ . pat)) ty)) #;(syntax-parse ty [((~literal #%plain-app) t . args) #:declare args pat-class @@ -98,7 +116,9 @@ (current-continuation-marks))))) (define-syntax (τ stx) (syntax-parse stx - [(_ . pat) #'(tycon . pat)] + [(_ . pat) ; first check shape + #:with (~! (~var t type) (... ...)) #'pat ; then check for valid types + #'(#%type (tycon . pat))] [_ (type-error #:src stx #:msg "Improper usage of type constructor ~a: ~a, expected pattern ~a" @@ -107,7 +127,7 @@ ;; TODO: refine this to enable specifying arity information ;; type constructors currently must have 1+ arguments -(define-syntax (define-type-constructor stx) +#;(define-syntax (define-type-constructor stx) (syntax-parse stx [(_ τ:id (~optional (~seq #:arity n:exact-positive-integer))) #:with τ? (format-id #'τ "~a?" #'τ) @@ -163,37 +183,44 @@ #:when (typecheck? #'tycon #'tmp) (stx-length #'(τ_arg (... ...)))])))])) +(define-syntax #%type (syntax-parser [(_ τ) #'τ])) + ;; syntax classes (begin-for-syntax (define-syntax-class type ;; stx = surface syntax, as written ;; norm = canonical form for the type - (pattern tycon:id + (pattern τ + #:fail-unless (is-type? #'τ) + (format "not a valid type: ~a" (syntax->datum #'τ)) + #:attr norm (delay ((current-type-eval) #'τ))) + #;(pattern tycon:id #:when (procedure? (syntax-local-value #'tycon (λ _ #f))) #:with norm #f ; should this be #f? #:with τ #f) - (pattern T:id + #;(pattern T:id #:with norm #'T ;((current-type-eval) #'T) #:with τ #'norm) ; backwards compat - (pattern (t:type ...) + #;(pattern (t:type ...) #:with norm #'(t ...) ;((current-type-eval) #'(t ...)) #:with τ #'norm) ; backwards compat - (pattern any + #;(pattern any #:with norm #f #:with τ #f #:fail-when #t (format "~a is not a valid type" (syntax->datum #'any)))) (define-syntax-class typed-binding #:datum-literals (:) - (pattern [x:id : stx:type] #:with τ #'stx.τ) - (pattern (~and any (~not [x:id : τ:type])) - #:with x #f - #:with τ #f + #:attributes (x τ norm) + (pattern [x:id : ~! τ:type] #:attr norm (delay #'τ.norm)) + (pattern any #:fail-when #t (format (string-append "Improperly formatted type annotation: ~a; should have shape [x : τ], " "where τ is a valid type.") - (syntax->datum #'any)))) + (syntax->datum #'any)) + #:attr x #f #:attr τ #f #:attr norm #f)) + (define (brace? stx) (define paren-shape/#f (syntax-property stx 'paren-shape)) (and paren-shape/#f (char=? paren-shape/#f #\{))) @@ -283,9 +310,15 @@ (stx-andmap typecheck? τs1 τs2))) (define current-type-eval (make-parameter #f)) + (define (type-evals τs) #`#,(stx-map (current-type-eval) τs)) (define current-promote (make-parameter (λ (x) x))) + (define (is-type? τ) + (syntax-parse (local-expand τ 'expression (list #'#%type)) + [((~literal #%type) t) #t] + [_ #f])) + ;; term expansion ;; expand/df : Syntax -> Syntax ;; Local expands the given syntax object. @@ -308,7 +341,7 @@ (exn:fail:type:check (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg) (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src) - (syntax->datum args) ...) + (type->str args) ...) (current-continuation-marks))))) (define-syntax (define-primop stx)