diff --git a/tapl/notes.txt b/tapl/notes.txt index a838475..cb3b138 100644 --- a/tapl/notes.txt +++ b/tapl/notes.txt @@ -1,3 +1,21 @@ +2015-07-28 +Problem: How to handle mixed types, ie combining expanded and unexpanded types. +Problem: When to eval, ie expand, types into canonical form +Solution: +- use two tags, #%type and #%plain-type, representing surface type syntax and + fully expanded type representation, respectively +- #%type wrapper automatically added by the define-type- macros +- #%plain-type wrapper added by type-eval +- both are macros that expand into their (single) sub-form + - enables elegant mixing of expanded and unexpanded types + - mixed types still need to be eval'ed + - needed to construct other types, eg inferring type of lambda +- enables easy checking of is-type? + - only checks outer wrapper + - rely on each tycon to validate its own arguments +- eval-type only expands if not #%plain-type, ie not already expanded +- this solution thus far does not require any awkward "hacks" in implementations + 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 ? @@ -12,6 +30,8 @@ What to do about "valid" terms like \x:(void).x or \x:1.x ? - 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 ? + - this might work + - will this have extensibility problems later, ie with records and variants? 2015-07-24 When to canonicalize (ie, eval) types: diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt index 9e82685..c1fc335 100644 --- a/tapl/stlc+lit.rkt +++ b/tapl/stlc+lit.rkt @@ -19,7 +19,7 @@ (define-syntax (datum/tc stx) (syntax-parse stx - [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)] + [(_ . n:integer) (⊢ (#%datum . n) : Int)] [(_ . x) #:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x) #'(#%datum . x)])) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index cbea98b..1f4097d 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -1,30 +1,38 @@ #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=? current-type=? type-eval)) (provide #%module-begin #%top-interaction #%top require) ; from racket ;; Simply-Typed Lambda Calculus ;; - no base type so cannot write any terms -;; Types: → +;; Types: multi-arg → (1+) ;; Terms: ;; - var -;; - multi-arg lambda -;; - multi-arg app +;; - multi-arg lambda (0+) +;; - multi-arg app (0+) (begin-for-syntax ;; type eval - ;; - for now, type-eval = full expansion + ;; - for now, type-eval = full expansion = canonical type representation ;; - must expand because: ;; - checks for unbound identifiers (ie, undefined types) + ;; - later, expanding enables reuse of same mechanisms for kind checking + ;; - may require some caution when mixing expanded and unexpanded types to + ;; create other types (define (type-eval τ) - (add-orig (expand/df τ) τ)) - (current-type-eval type-eval)) + (if (plain-type? τ) ; don't expand if already expanded + τ + (add-orig #`(#%plain-type #,(expand/df τ)) τ))) + + (current-type-eval type-eval) -(begin-for-syntax ;; type=? : Type Type -> Boolean ;; Indicates whether two types are equal ;; type equality == structurally free-identifier=? + ;; does not assume any sort of representation (eg expanded/unexpanded) + ;; - caller (see typechecks? in typecheck.rkt) is responsible to + ;; convert if necessary (define (type=? τ1 τ2) ; (printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum τ1)) ; (printf "(τ=) t2 = ~a\n" #;τ2 (syntax->datum τ2)) @@ -32,43 +40,13 @@ [(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 (same-types? τs) - (define τs-lst (syntax->list τs)) - (or (null? τs-lst) - (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst))))) - -;(define-type-constructor →) - -;;; when defining a type constructor tycon, can't define tycon as both -;;; - an appliable constructor (ie a macro) -;;; - and a syntax class -;;; alternate solution: automatically define a tycon-match function -;(define-syntax define-tycon -; (syntax-parser -; [(_ (τ arg ...)) -; #:with pat (generate-temporary) ; syntax-class name -; #:with fn (generate-temporary) ; need a runtime id for expansion -; #'(begin -; (begin-for-syntax -; (define-syntax-class pat -; (pattern (arg ...)))) -; (define-syntax τ -; (syntax-parser -; [x:id #'pat] -; [(_ x ( ... ...)) #'(fn x (... ...))])))])) -;(define-tycon (→ τ ... τ_res)) -; -;(define-for-syntax match-type-as -; (syntax-parser -; [( τ pat) -; #:with + (current-typecheck-relation type=?)) (define-type-constructor (→ τ_in ... τ_out)) @@ -76,49 +54,25 @@ (syntax-parse stx [(_ (b:typed-binding ...) e) #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e) - (⊢ #'(λ xs- e-) #`(→ b.τ ... #,(syntax-track-origin #'(#%type τ_res) #'τ_res #'λ)))])) + (⊢ (λ xs- e-) : (→ b.τ ... τ_res))])) (define-syntax (app/tc stx) (syntax-parse stx [(_ e_fn e_arg ...) - #:with (e_fn- (τ_in ... τ_out)) (→-match+erase #'e_fn) - ;#:with (e_fn- τ_fn) (infer+erase #'e_fn) - ;#:with (e_fn- (τ_in ... τ_out)) (match+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 (τ_in ... τ_out) (→-match #'τ_fn) - #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...)) -; #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ ...)) -; (string-append -; (format -; "Wrong number of args given to function ~a:\ngiven: " -; (syntax->datum #'e_fn)) -; (string-join -; (map -; (λ (e t) (format "~a : ~a" e t)) -; (syntax->datum #'(e_arg ...)) -; (syntax->datum #`#,(stx-map get-orig #'(τ_arg ...)))) -; ", ") -; (format "\nexpected: ~a argument(s)." (stx-length #'(τ ...)))) + #:with [e_fn- (τ_in ... τ_out)] (→-match+erase #'e_fn) + #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...)) #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) (string-append - (format "Arguments to function ~a have wrong type(s), " + (format "~a (~a:~a) Arguments to function ~a have wrong type(s), " + (syntax-source stx) (syntax-line stx) (syntax-column stx) (syntax->datum #'e_fn)) - "or wrong number of arguments:\n" - "given:\n" + "or wrong number of arguments:\nGiven:\n" (string-join - (map - (λ (e t) (format " ~a : ~a" e t)) - (syntax->datum #'(e_arg ...)) - (stx-map type->str #'(τ_arg ...)) - #;(syntax->datum #`#,(stx-map get-orig #'(τ_arg ...)))) - "\n") - "\n" - (format "expected ~a arguments with type(s): " + (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line + (syntax->datum #'(e_arg ...)) + (stx-map type->str #'(τ_arg ...))) + "\n" #:after-last "\n") + (format "Expected: ~a arguments with type(s): " (stx-length #'(τ_in ...))) - (string-join - (stx-map type->str #'(τ_in ...)) - #;(map ~a (syntax->datum #`#,(stx-map get-orig #'(τ_in ...)))) - ", ")) - (⊢ #'(#%app e_fn- e_arg- ...) #'τ_out)])) + (string-join (stx-map type->str #'(τ_in ...)) ", ")) + (⊢ (#%app e_fn- e_arg- ...) : τ_out)])) diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt index b3be9f7..80976cc 100644 --- a/tapl/tests/stlc+lit-tests.rkt +++ b/tapl/tests/stlc+lit-tests.rkt @@ -41,11 +41,12 @@ (typecheck-fail (+ 1 (λ ([x : Int]) x)) #:with-msg - "Arguments to function \\+ have wrong type.+given:\n 1 : Int.+(→ Int 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:.+(→ Int Int).+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") diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index 03190b2..bf72f07 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -38,8 +38,8 @@ (syntax-parse stx [x:id (add-orig #'(#%type (τ-internal)) #'τ)])) (define-for-syntax (τ? t) - (syntax-parse t - [((~literal #%type) ((~literal #%plain-app) ty)) + (syntax-parse ((current-type-eval) t) + [((~literal #%plain-type) ((~literal #%plain-app) ty)) (typecheck? #'ty #'τ-internal)])))])) (struct exn:fail:type:runtime exn:fail:user ()) @@ -63,8 +63,8 @@ (define-syntax (match-type stx) (syntax-parse stx [(_ ty tycon cls) - #'(syntax-parse ty ;((current-type-eval) ty) - [((~literal #%plain-app) t . args) + #'(syntax-parse ((current-type-eval) ty) + [((~literal #%plain-type) ((~literal #%plain-app) t . args)) #:declare args cls #:fail-unless (typecheck? #'t #'tycon) (format "Type error: expected ~a type, got ~a" @@ -87,6 +87,8 @@ (provide τ) (begin-for-syntax (define-syntax-class pat-class + ;; dont check is-type? here; should already be types + ;; only need to check is-type? for user-entered types (pattern pat)) (define (τ-match ty) (or (match-type ty tycon pat-class) @@ -183,7 +185,12 @@ #:when (typecheck? #'tycon #'tmp) (stx-length #'(τ_arg (... ...)))])))])) -(define-syntax #%type (syntax-parser [(_ τ) #'τ])) +;; when combining #%type's with #%plain-type's, eg when inferring type for λ +;; (call this mixed type) we create a type that still needs expansion, ie type-eval +;; With the #%type and #%plain-type distinction, mixed types can simply be eval'ed +;; and the #%plain-type will wrappers will simply go away +(define-syntax #%type (syntax-parser [(_ τ) #'τ])) ; surface stx +(define-syntax #%plain-type (syntax-parser [(_ τ) #'τ])) ; expanded representation ;; syntax classes (begin-for-syntax @@ -192,7 +199,9 @@ ;; norm = canonical form for the type (pattern τ #:fail-unless (is-type? #'τ) - (format "not a valid type: ~a" (syntax->datum #'τ)) + (format "~a (~a:~a) not a valid type: ~a" + (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) + (syntax->datum #'τ)) #:attr norm (delay ((current-type-eval) #'τ))) #;(pattern tycon:id #:when (procedure? (syntax-local-value #'tycon (λ _ #f))) @@ -232,10 +241,15 @@ #:with norm #'τ.norm))) (begin-for-syntax + (define-syntax (⊢ stx) + (syntax-parse stx #:datum-literals (:) + [(_ e : τ) #'(assign-type #'e #'τ)] + [(_ e τ) #'(⊢ e : τ)])) + ;; ⊢ : Syntax Type -> Syntax ;; Attaches type τ to (expanded) expression e. ;; must eval here, to catch unbound types - (define (⊢ e τ #:tag [tag 'type]) + (define (assign-type e τ #:tag [tag 'type]) (syntax-property e tag (syntax-local-introduce ((current-type-eval) τ)))) ;(syntax-property e tag τ)) @@ -279,7 +293,7 @@ (expand/df #`(λ #,tvs (λ (x ...) - (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ #:tag '#,tag))] ...) + (let-syntax ([x (make-rename-transformer (assign-type #'x #'τ #:tag '#,tag))] ...) (#%expression e) ...)))) (list #'tvs+ #'xs+ #'(e+ ...) (stx-map syntax-local-introduce (stx-map typeof #'(e+ ...))))] @@ -304,7 +318,7 @@ (define current-typecheck-relation (make-parameter #f)) (define (typecheck? t1 t2) - ((current-typecheck-relation) t1 t2)) + ((current-typecheck-relation) ((current-type-eval) t1) ((current-type-eval) t2))) (define (typechecks? τs1 τs2) (and (= (stx-length τs1) (stx-length τs2)) (stx-andmap typecheck? τs1 τs2))) @@ -314,10 +328,14 @@ (define current-promote (make-parameter (λ (x) x))) + ;; only check top level; tycons are responsible for verifying their own args (define (is-type? τ) - (syntax-parse (local-expand τ 'expression (list #'#%type)) - [((~literal #%type) t) #t] - [_ #f])) + (or (plain-type? τ) + ; partial expand to reveal #%type wrapper + (syntax-parse (local-expand τ 'expression (list #'#%type)) + [((~literal #%type) _) #t] [_ #f]))) + (define (plain-type? τ) + (syntax-parse τ [((~literal #%plain-type) _) #t] [_ #f])) ;; term expansion ;; expand/df : Syntax -> Syntax @@ -352,11 +370,11 @@ (provide (rename-out [op/tc op])) (define-syntax (op/tc stx) (syntax-parse stx - [f:id (⊢ (syntax/loc stx op) #'τ)] ; HO case + [f:id (assign-type (syntax/loc stx op) #'τ)] ; HO case [(_ x (... ...)) #:with app (datum->syntax stx '#%app) #:with op (format-id stx "~a" #'op) - #'(app op x (... ...))])))])) + (syntax/loc stx (app op x (... ...)))])))])) (define-for-syntax (mk-pred x) (format-id x "~a?" x)) (define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))