commit c64251cac0e8d09dcc935f873ce11093ece0bc84
parent 29be57dffea1b2730bf21de451d6774570546eac
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 19 Apr 2016 15:10:07 -0400
infer quantified type variables in the order that they occur (L-to-R)
- backwards incompatible change: quantified type variables no longer sorted lex
- fix and add tests, remove some annotations in tests
- small speed improvement due to eliminating some extra expansions
- closes #9, closes #11
Diffstat:
6 files changed, 123 insertions(+), 72 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -114,21 +114,23 @@
(define (inst-types tys-solved Xs tys)
(stx-map (lambda (t) (inst-type tys-solved Xs t)) tys))
- ;; computes unbound ids in tys, to be used as tyvars
+ ;; compute unbound tyvars in one unexpanded type ty
+ (define (compute-tyvar1 ty)
+ (syntax-parse ty
+ [X:id #'(X)]
+ [() #'()]
+ [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))]))
+ ;; computes unbound ids in (unexpanded) tys, to be used as tyvars
(define (compute-tyvars tys)
- (if (stx-null? tys)
- #'()
- (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
- (define ctx (stx-car tys))
- (with-handlers
- ([exn:fail:syntax:unbound?
- (λ (e)
- (define X (stx-car (exn:fail:syntax-exprs e)))
- ;; X is tainted, so need to launder it
- (define Y (datum->syntax ctx (syntax->datum X)))
- (L (cons Y Xs)))])
- ((current-type-eval) #`(∀ #,Xs (ext-stlc:→ . #,tys)))
- (stx-sort Xs))))))
+ (define Xs (stx-appendmap compute-tyvar1 tys))
+ (filter
+ (lambda (X)
+ (with-handlers
+ ([exn:fail:syntax:unbound? (lambda (e) #t)]
+ [exn:fail:type:infer? (lambda (e) #t)])
+ (let ([X+ ((current-type-eval) X)])
+ (not (or (tyvar? X+) (type? X+))))))
+ (stx-remove-dups Xs))))
;; define --------------------------------------------------
;; for function defs, define infers type variables
@@ -267,16 +269,20 @@
[_:id
#:when (and (not (stx-null? #'(X ...)))
(not (stx-null? #'(τ ...))))
- (type-error
- #:src stx
- #:msg
- (string-append
- (format "constructor ~a must instantiate ~a type argument(s): "
- 'Cons (stx-length #'(X ...)))
- (string-join (stx-map type->str #'(X ...)) ", ")
- "\n"
- (format "and be applied to ~a arguments with type(s): "(stx-length #'(τ ...)))
- (string-join (stx-map type->str #'(τ ...)) ", ")))]
+ (raise
+ (exn:fail:type:infer
+ (string-append
+ (format "TYPE-ERROR: ~a (~a:~a):"
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ "\n"
+ (format "Constructor ~a must be applied to ~a argument(s) with type(s): "
+ 'Cons (stx-length #'(τ ...)))
+ (string-join (stx-map type->str #'(τ ...)) ", ")
+ "\n"
+ (format "The arguments should instantiate ~a type argument(s): "
+ (stx-length #'(X ...)))
+ (string-join (stx-map type->str #'(X ...)) ", "))
+ (current-continuation-marks)))]
[(C τs e_arg ...)
#:when (brace? #'τs) ; commit to this clause
#:with {~! τ_X:type (... ...)} #'τs
@@ -905,7 +911,7 @@
(⊢ (for*/list ([x- e-] ...) body-) : (List ty_body))])
(define-typed-syntax for/fold
[(_ ([acc init]) ([x:id e] ...) body)
- #:with [init- ty_init] (infer+erase #'init)
+ #:with [init- ty_init] (infer+erase #`(pass-expected init #,stx))
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(acc- x- ...) body- ty_body]
(infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -57,6 +57,9 @@
(define (stx-appendmap f stx)
(stx-flatten (stx-map f stx)))
+(define (stx-remove-dups Xs)
+ (remove-duplicates (stx->list Xs) free-identifier=?))
+
(define (stx-drop stx n)
(drop (stx->list stx) n))
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -52,7 +52,7 @@
(check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool}))
(check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)}))
(check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))}))
-;; same as tests above, but without annotations
+;; annotations unneeded: same as tests above, but without annotations
(check-type (g2 Nil) : (List Int) ⇒ Nil)
(check-type (g2 Nil) : (List Bool) ⇒ Nil)
(check-type (g2 Nil) : (List (List Int)) ⇒ Nil)
@@ -278,6 +278,39 @@
(define-type (Pairof A B) (C A B))
(check-type (match (C 1 2) with [C a b -> None]) : (Option Int) -> None)
+;; type variable inference
+
+; F should remain valid tyvar, even though it's bound
+(define (F [x : X] -> X) x)
+(define (tvf1 [x : F] -> F) x)
+(check-type tvf1 : (→/test X X))
+
+; G should remain valid tyvar
+(define-type (Type1 X) (G X))
+(define (tvf5 [x : G] -> G) x)
+(check-type tvf5 : (→/test X X))
+
+; TY should not be tyvar, bc it's a valid type
+(define-type-alias TY (Pairof Int Int))
+(define (tvf2 [x : TY] -> TY) x)
+(check-not-type tvf2 : (→/test X X))
+
+; same with Bool
+(define (tvf3 [x : Bool] -> Bool) x)
+(check-not-type tvf3 : (→/test X X))
+
+;; X in lam should not be a new tyvar
+(define (tvf4 [x : X] -> (→ X X))
+ (λ ([y : X]) x))
+(check-type tvf4 : (→/test X (→ X X)))
+(check-not-type tvf4 : (→/test X (→ Y X)))
+
+(check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X)))
+(check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
+(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
+
+
; ext-stlc tests --------------------------------------------------
; tests for stlc extensions
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
@@ -79,7 +79,7 @@
[Leaf x -> (list x)]
[Node x rst ->
(cons x
- (for/fold ([acc (nil {X})]) ([p (in-list (flatten rst))])
+ (for/fold ([acc nil]) ([p (in-list (flatten rst))])
(match p with
[x y -> (cons x (cons y acc))])))]))
diff --git a/tapl/tests/mlish/result.mlish b/tapl/tests/mlish/result.mlish
@@ -14,13 +14,15 @@
(provide ok)
(provide error)
+(check-type ok : (→/test A (Result A B)))
+(check-type error : (→/test B (Result A B)))
(check-type (inst ok Int String) : (→ Int (Result Int String)))
-(check-type (inst error Int String) : (→ String (Result Int String)))
+(check-type (inst error String Int) : (→ String (Result Int String)))
(check-type
- (list (Ok {Int String} 3) (Error "abject failure") (Ok 4))
+ (list (Ok 3) (Error "abject failure") (Ok 4))
: (List (Result Int String))
- -> (list (Ok {Int String} 3) (Error "abject failure") (Ok 4)))
+ -> (list (Ok 3) (Error "abject failure") (Ok 4)))
(define (result-bind [a : (Result A Er)] [f : (→ A (Result B Er))]
→ (Result B Er))
@@ -74,59 +76,58 @@
(define (read-tree [str : (List Char)] → (Read-Result (Tree Int)))
(cond
- [(isnil str)
- (error "expected a tree of integers, given nothing")]
- [(equal? (head str) #\( )
- (do result-bind
- [tree1+str : (× (Tree Int) (List Char))
- <- (read-tree (tail str))]
- [(cond [(equal? (head (proj tree1+str 1)) #\space)
- ((inst ok Unit String) (void))]
- [else
- ((inst error Unit String) "expected a space")])]
- [int+str : (× Int (List Char))
- <- (read-int (tail (proj tree1+str 1)) nil)]
- [(cond [(equal? (head (proj int+str 1)) #\space)
- ((inst ok Unit String) (void))]
- [else
- ((inst error Unit String) "expected a space")])]
- [tree2+str : (× (Tree Int) (List Char))
- <- (read-tree (tail (proj int+str 1)))]
- [(cond [(equal? (head (proj tree2+str 1)) #\) )
- ((inst ok Unit String) (void))]
- [else
- ((inst error Unit String) "expected a `)`")])]
- ((inst ok (× (Tree Int) (List Char)) String)
- (tup (Node (proj tree1+str 0)
- (proj int+str 0)
- (proj tree2+str 0))
- (tail (proj tree2+str 1)))))]
- [(digit? (head str))
- (do result-bind
- [int+str : (× Int (List Char))
- <- (read-int str nil)]
- ((inst ok (× (Tree Int) (List Char)) String)
- (tup (Leaf (proj int+str 0))
- (proj int+str 1))))]
- [else
- (error "expected either a `(` or a digit")]))
+ [(isnil str)
+ (error "expected a tree of integers, given nothing")]
+ [(equal? (head str) #\( )
+ (let ([do-ok (inst ok Unit String)]
+ [do-error (inst error String Unit)])
+ (do result-bind
+ [tree1+str : (× (Tree Int) (List Char))
+ <- (read-tree (tail str))]
+ [(cond [(equal? (head (proj tree1+str 1)) #\space)
+ (do-ok (void))]
+ [else (do-error "expected a space")])]
+ [int+str : (× Int (List Char))
+ <- (read-int (tail (proj tree1+str 1)) nil)]
+ [(cond [(equal? (head (proj int+str 1)) #\space)
+ (do-ok (void))]
+ [else (do-error "expected a space")])]
+ [tree2+str : (× (Tree Int) (List Char))
+ <- (read-tree (tail (proj int+str 1)))]
+ [(cond [(equal? (head (proj tree2+str 1)) #\) )
+ (do-ok (void))]
+ [else (do-error "expected a `)`")])]
+ (ok
+ (tup (Node (proj tree1+str 0)
+ (proj int+str 0)
+ (proj tree2+str 0))
+ (tail (proj tree2+str 1))))))]
+ [(digit? (head str))
+ (do result-bind
+ [int+str : (× Int (List Char))
+ <- (read-int str nil)]
+ (ok
+ (tup (Leaf (proj int+str 0))
+ (proj int+str 1))))]
+ [else
+ (error "expected either a `(` or a digit")]))
(check-type
(read-tree (string->list "42"))
: (Read-Result (Tree Int))
- -> ((inst ok (× (Tree Int) (List Char)) String)
+ -> (ok
(tup (Leaf 42) nil)))
(check-type
(read-tree (string->list "x"))
: (Read-Result (Tree Int))
- -> ((inst error (× (Tree Int) (List Char)) String)
+ -> (error
"expected either a `(` or a digit"))
(check-type
(read-tree (string->list "(42 43 (44 45 46))"))
: (Read-Result (Tree Int))
- -> ((inst ok (× (Tree Int) (List Char)) String)
+ -> (ok
(tup (Node (Leaf 42) 43 (Node (Leaf 44) 45 (Leaf 46))) nil)))
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -135,6 +135,10 @@
(define-syntax add-expected
(syntax-parser
[(_ e τ) (syntax-property #'e 'expected-type #'τ)]))
+(define-syntax pass-expected
+ (syntax-parser
+ [(_ e stx) (syntax-property #'e 'expected-type
+ (syntax-property #'stx 'expected-type))]))
(define-for-syntax (add-expected-ty e ty)
(or (and (syntax-e ty)
(syntax-property e 'expected-type ((current-type-eval) ty)))
@@ -170,6 +174,8 @@
(define ty (syntax-property stx tag))
(if (cons? ty) (car ty) ty))
+ (define (tyvar? X) (syntax-property X 'tyvar))
+
(define type-pat "[A-Za-z]+")
;; - infers type of e
@@ -284,9 +290,11 @@
(expand/df
#`(λ (tv ...)
(let-syntax ([tv (make-rename-transformer
- (assign-type
- (assign-type #'tv #'k)
- #'ok #:tag '#,tag))] ...)
+ (syntax-property
+ (assign-type
+ (assign-type #'tv #'k)
+ #'ok #:tag '#,tag)
+ 'tyvar #t))] ...)
(λ (x ...)
(let-syntax
([x
