commit b6c8bb5880bf8e801dac6d02326241724ff4a5b0
parent aa930c1180f13b6fdba2b378fc1f8e7675f53f95
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 21 Dec 2015 18:55:42 -0500
infer some lambda param types from body
Diffstat:
4 files changed, 107 insertions(+), 20 deletions(-)
diff --git a/tapl/infer.rkt b/tapl/infer.rkt
@@ -64,13 +64,13 @@
(define y e-))]
[(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
#:when (brace? #'Xs)
- #:with g (generate-temporary)
+ #:with g (generate-temporary #'f)
#:with e_ann #'(add-expected e τ_out)
#'(begin
(define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
(define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
[(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
- #:with g (generate-temporary)
+ #:with g (generate-temporary #'f)
#:with e_ann #'(add-expected e τ_out)
#'(begin
(define-syntax f (make-rename-transformer (⊢ g : (→ τ ... τ_out))))
@@ -78,7 +78,7 @@
; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
(define-typed-syntax λ #:datum-literals (:)
- [(~and fn (_ (x:id ...) e) ~!) ; no annotations
+ [(~and fn (_ (x:id ...) e)) ; no annotations, try to infer from outer ctx, ie an application
#:with given-τ-args (syntax-property #'fn 'given-τ-args)
#:fail-unless (syntax-e #'given-τ-args) ; no inferred types or annotations, so error
(format "input types for ~a could not be inferred; add annotations"
@@ -86,12 +86,28 @@
#:with (τ_arg ...) #'given-τ-args
#:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
(⊢ λ- : (∀ () τ_λ))]
+ [(~and fn (_ (x:id ...) e) ~!) ; no annotations, couldnt infer from ctx (eg, unapplied lam), try to infer from body
+ #:with (xs- e- τ_res) (infer/ctx+erase #'([x : x] ...) #'e)
+ #:with env (get-env #'e-)
+ #:fail-unless (syntax-e #'env)
+ (format "input types for ~a could not be inferred; add annotations"
+ (syntax->datum #'fn))
+ #:with (τ_arg ...) (stx-map (λ (y) (lookup y #'env)) #'xs-)
+ #:fail-unless (stx-andmap syntax-e #'(τ_arg ...))
+ (format "some input types for ~a could not be inferred; add annotations"
+ (syntax->datum #'fn))
+ ;; propagate up inferred types of variables
+ #:with res (add-env #'(λ xs- e-) #'env)
+; #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : x] ...) e))
+ (⊢ res : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
+ ;(⊢ (λ xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
[(_ . rst)
#:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ . rst))
(⊢ λ- : (∀ () τ_λ))])
(define-typed-syntax #%app
[(_ e_fn e_arg ...) ; infer args first
+ ; #:when (printf "args first ~a\n" (syntax->datum stx))
#:with maybe-inferred-τs (with-handlers ([exn:fail:type:infer? (λ _ #f)])
(infers+erase #'(e_arg ...)))
#:when (syntax-e #'maybe-inferred-τs)
@@ -131,8 +147,13 @@
(format "Expected: ~a arguments with type(s): "
(stx-length #'(τ_in ...)))
(string-join (stx-map type->str #'(τ_in ...)) ", "))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)]
+ ; propagate inferred types for variables up
+ #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e_arg- ...))))
+ #:with result-app (add-env #'(#%app e_fn- e_arg- ...) #'env)
+ ;(⊢ (#%app e_fn- e_arg- ...) : τ_out)]
+ (⊢ result-app : τ_out)]
[(_ e_fn e_arg ...) ; infer fn first ------------------------- ; TODO: remove code dup
+; #:when (printf "fn first ~a\n" (syntax->datum stx))
#:with [e_fn- ((X ...) ((~ext-stlc:→ τ_inX ... τ_outX)))] (⇑ e_fn as ∀)
#:fail-unless (stx-length=? #'(τ_inX ...) #'(e_arg ...)) ; check arity
(string-append
@@ -153,15 +174,20 @@
(define/with-syntax τs_solved (stx-map (λ (y) (lookup y cs)) #'(X ...)))
(cond
[(andmap syntax-e (syntax->list #'τs_solved)) ; all tyvars X have mapping
+ ; TODO: substs is not properly transferring #%type property
+; (stx-map displayln #'τs_solved)
(define e+τ (infer+erase #`(add-expected #,e_arg #,(substs #'τs_solved #'(X ...) τ_inX))))
+ ; (displayln e+τ)
(values cs (cons e+τ e+τs))]
[else
(define/with-syntax [e τ] (infer+erase e_arg))
+ ; (displayln #'(e τ))
(define/with-syntax (c ...) cs)
(define/with-syntax (new-c ...) (compute-constraint #`(#,τ_inX τ)))
(values #'(new-c ... c ...) (cons #'[e τ] e+τs))]))])
(define/with-syntax e+τs/stx e+τs)
(list cs (reverse (syntax->list #'e+τs/stx))))
+ #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e_arg- ...))))
#:with (τ_solved ...) (stx-map (λ (y) (lookup y #'cs)) #'(X ...))
#:with (τ_in ... τ_out) (stx-map (λ (t) (substs #'(τ_solved ...) #'(X ...) t)) #'(τ_inX ... τ_outX))
; some code duplication
@@ -179,4 +205,6 @@
(format "Expected: ~a arguments with type(s): "
(stx-length #'(τ_in ...)))
(string-join (stx-map type->str #'(τ_in ...)) ", "))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+ #:with result-app (add-env #'(#%app e_fn- e_arg- ...) #'env)
+ ;(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+ (⊢ result-app : τ_out)])
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -35,7 +35,10 @@
(format "trying to cons expression ~a with type ~a to list ~a with type ~a\n"
(syntax->datum #'e1) (type->str #'τ1)
(syntax->datum #'e2) (type->str #'(List τ2)))
- (⊢ (cons e1- e2-) : (List τ1))])
+ ;; propagate up inferred types of variables
+ #:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
+ #:with result-cons (add-env #'(cons e1- e2-) #'env)
+ (⊢ result-cons : (List τ1))])
(define-typed-syntax isnil
[(_ e)
#:with (e- _) (⇑ e as List)
diff --git a/tapl/tests/infer-tests.rkt b/tapl/tests/infer-tests.rkt
@@ -1,13 +1,15 @@
#lang s-exp "../infer.rkt"
(require "rackunit-typechecking.rkt")
-(typecheck-fail (λ (x) x) #:with-msg "add annotations")
+(typecheck-fail (λ (x) x) #:with-msg "could not infer type of x; add annotation\\(s\\)")
; should bidirectional checking work for this case?
; I think no, since TR doesnt handle it either
-(typecheck-fail (λ (x) (+ x 1)) #:with-msg "add annotations")
+;(typecheck-fail (λ (x) (+ x 1)) #:with-msg "add annotations")
+; 2015-12-18: can infer this type now
+(check-type (λ (x) (+ x 1)) : (→ Int Int))
; can't check this case either
-(typecheck-fail ((λ (f) (f 10)) (λ (x) x)) #:with-msg "add annotations")
+(typecheck-fail ((λ (f) (f 10)) (λ (x) x)) #:with-msg "add annotation\\(s\\)")
; stlc+lit tests with app, but infer types (no annotations)
(check-type ((λ (x) x) 1) : Int ⇒ 1)
@@ -89,7 +91,8 @@
(typecheck-fail (map add1 (list "1")) #:with-msg "Arguments.+have wrong type")
(check-type (map (λ ([x : Int]) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
; doesnt work yet
-;(map (λ (x) (+ x 2)) (list 1 2 3))
+;; 2015-12-18: dont need annotations on lambdas with concrete type
+(check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5))
(define {X} (filter [p? : (→ X Bool)] [lst : (List X)] → (List X))
(if (nil? lst)
@@ -107,6 +110,8 @@
(check-type (filter zero? (list 1 2 3)) : (List Int) ⇒ (nil {Int}))
(check-type (filter zero? (list 0 1 2)) : (List Int) ⇒ (list 0))
(check-type (filter (λ ([x : Int]) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
+;; 2015-12-18: dont need annotations on lambdas with concrete type
+(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2))
(define {X Y} (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y)
(if (nil? lst)
@@ -161,12 +166,16 @@
(define (nqueens [n : Int] → (List Queen))
(let* ([process-row
- (λ ([r : Int] [all-possible-so-far : (List (List Queen))])
+ (λ ;([r : Int] [all-possible-so-far : (List (List Queen))])
+ (r all-possible-so-far)
(foldr
- (λ ([qs : (List Queen)] [new-qss : (List (List Queen))])
+ ;; 2015-12-18: dont need annotations on lambdas with concrete type
+ (λ ;([qs : (List Queen)] [new-qss : (List (List Queen))])
+ (qs new-qss)
(append
(map
- (λ ([c : Int]) (cons (Q r c) qs))
+ ;; 2015-12-18: dont need annotations on lambdas with concrete type
+ (λ (c) (cons (Q r c) qs))
(build-list n add1))
new-qss))
nil
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -54,7 +54,7 @@
(syntax-parameterize ([stx (syntax-id-rules () [_ syntx])])
(syntax-parse syntx #:context #'out-name stx-parse-clause ...))))]
[(_ name:id stx-parse-clause ...)
- #`(define-typed-syntax #,(generate-temporary) #:export-as name
+ #`(define-typed-syntax #,(generate-temporary #'name) #:export-as name
stx-parse-clause ...)]))
;; need options for
@@ -118,7 +118,11 @@
(all-from-out base-lang))))]))
(define-syntax add-expected
- (syntax-parser [(_ e τ) (syntax-property #'e 'expected-type #'τ)]))
+ (syntax-parser
+ [(_ e τ)
+; #:when (printf "adding expected type ~a to expression ~a\n"
+; (syntax->datum #'τ) (syntax->datum #'e))
+ (syntax-property #'e 'expected-type #'τ)]))
;; type assignment
(begin-for-syntax
@@ -141,6 +145,8 @@
(syntax-property e 'expected-type τ)) ; dont type-eval?, ie expand?
(define (get-expected-type e)
(syntax-property e 'expected-type))
+ (define (add-env e env) (syntax-property e 'env env))
+ (define (get-env e) (syntax-property e 'env))
;; typeof : Syntax -> Type or #f
;; Retrieves type of given stx, or #f if input has not been assigned a type.
@@ -249,17 +255,45 @@
(assign-type #'tv #'k)
#'ok #:tag '#,tag))] ...)
(λ (x ...)
- (let-syntax ([x (syntax-parser [_:id (assign-type #'x #'τ)]
+ (let-syntax ([x (syntax-parser [i:id
+; #:when (or (not (and (identifier? #'τ) (free-identifier=? #'x #'τ)))
+; (printf "~a has type = itself\n" #'i))
+; #:when (or (not (get-expected-type #'i))
+; (printf "expected type of ~a: ~a\n"
+; #'i (and (get-expected-type #'i)
+; (syntax->datum (get-expected-type #'i)))))
+; #:when (or (not (get-expected-type #'i))
+; (printf "assigned type of ~a: ~a\n"
+; (syntax->datum #'i) (syntax->datum #'τ)))
+ (if (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+ (if (get-expected-type #'i)
+ (add-env (assign-type #'x (get-expected-type #'i)) #`((x #,(get-expected-type #'i))))
+ (raise (exn:fail:type:infer
+ (format "~a (~a:~a): could not infer type of ~a; add annotation(s)"
+ (syntax-source #'x) (syntax-line #'x) (syntax-column #'x)
+ (syntax->datum #'x))
+ (current-continuation-marks))))
+ (assign-type #'x #'τ))]
[(o . rst) ; handle if x used in fn position
+ #:fail-when (and (identifier? #'τ) (free-identifier=? #'x #'τ))
+ (raise (exn:fail:type:infer
+ (format "~a (~a:~a): could not infer type of function ~a; add annotation(s)"
+ (syntax-source #'o) (syntax-line #'o) (syntax-column #'o)
+ (syntax->datum #'o))
+ (current-continuation-marks)))
#:with app (datum->syntax #'o '#%app)
#`(app #,(assign-type #'x #'τ) . rst)]
#;[(_ . rst) #`(#,(assign-type #'x #'τ) . rst)])
- #;(make-rename-transformer
- (assign-type #'x #'τ))] ...)
+ #;(make-rename-transformer (assign-type #'x #'τ))] ...)
(#%expression e) ... void)))))
(list #'tvs+ #'xs+ #'(e+ ...)
(stx-map ; need this check when combining #%type and kinds
- (λ (t) (or (false? t) (syntax-local-introduce t)))
+ (λ (t) (or (false? t)
+ ; TODO: why does this happen?
+ ; happens when propagating 'env up in λ
+ #;(and (pair? t)
+ (syntax-local-introduce (car t)))
+ (syntax-local-introduce t)))
(stx-map typeof #'(e+ ...))))]
[([x τ] ...) (infer es #:ctx #'([x : τ] ...) #:tvctx tvctx)]))
@@ -578,10 +612,23 @@
; substitution
(begin-for-syntax
+ (define (merge-type-tags stx)
+ (define t (syntax-property stx 'type))
+ (or (and (pair? t)
+ (identifier? (car t)) (identifier? (cdr t))
+ (free-identifier=? (car t) (cdr t))
+ (syntax-property stx 'type (car t)))
+ stx))
; subst τ for y in e, if (bound-id=? x y)
(define (subst τ x e)
(syntax-parse e
- [y:id #:when (bound-identifier=? e x) (syntax-track-origin τ #'y #'y)]
+ [y:id #:when (bound-identifier=? e x)
+; #:when
+; (displayln (syntax-property (syntax-track-origin τ #'y #'y) 'type))
+; #:when (displayln (syntax-property (syntax-property (syntax-track-origin τ #'y #'y) 'type #'#%type) 'type))
+ ; use syntax-track-origin to transfer 'orig
+ ; but may transfer multiple #%type tags, so merge
+ (merge-type-tags (syntax-track-origin τ #'y #'y))]
[(esub ...)
#:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
(syntax-track-origin #'(esub_subst ...) e x)]
