commit a44d946ffb0a78c132cb455d8701e8a5a0d54128
parent daecc5c62402bbd290ba9d336fc0b38897b378ed
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 28 Jul 2015 15:25:34 -0400
add #%type annotation; add type->str; type constructor pattern match
- #%type annotation distinguishes types from terms
- is-type? checks #%type
- type->str fixes type printing
- wasnt recursively calling get-orig
- use delay in "type" syntax-class norm attribute
- fixes eager eval problem from before
- add more invalid type tests
- only tested up to stlc+lit.rkt
- nicer type constructors
- more concise, intuitive pat matching language
- use for-meta 2 macros
Diffstat:
5 files changed, 96 insertions(+), 46 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)
