Skip to content

[WIP] Infer instantiations for polymorphic arguments to polymorphic functions [rebase of Alex Knauth's PR on bitbucket] #29

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
SuzanneSoy wants to merge 5 commits into
base: master
Choose a base branch
from
Open

[WIP] Infer instantiations for polymorphic arguments to polymorphic functions [rebase of Alex Knauth's PR on bitbucket] #29

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
dbafd4e
lift nested foralls from function result types
AlexKnauth May 4, 2016
2261861
infer instantiations for polymorphic arguments to polymorphic functions
AlexKnauth May 9, 2016
6247b62
Adjusted some tests for https://bitbucket.org/stchang/macrotypes/pull…
SuzanneSoy Sep 28, 2017
9d812c0
Hopefully not unsound fix for the (Cons (λ ([x : Y]) x) Nil) bug.
SuzanneSoy Sep 29, 2017
dea93ab
Fixed another test
SuzanneSoy Sep 29, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
133 changes: 88 additions & 45 deletions macrotypes/examples/mlish.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@
(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
(require (only-in "stlc+rec-iso.rkt" ~× ×?))
(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum])
?∀)
(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
(require (only-in "stlc+cons.rkt" ~List List? List))
Expand Down Expand Up @@ -110,22 +111,48 @@
(~and (~not (~∀ _ _))
(~parse vars-pat #'())
body-pat))]))))


;; matching possibly polymorphic types with renamings
(define-syntax ~?∀*
(pattern-expander
(lambda (stx)
(syntax-case stx ()
[(?∀* vars-pat body-pat)
#'(~and (~?∀ vars body)
(~parse vars* (generate-temporaries #'vars))
(~parse vars** (stx-map add-orig #'vars* #'vars))
(~parse body* (inst-type #'vars** #'vars #'body))
(~parse vars-pat #'vars**)
(~parse body-pat #'body*))]))))

;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
;; finds the free Xs in the type
(define (find-free-Xs Xs ty)
(for/list ([X (in-list (stx->list Xs))]
#:when (stx-contains-id? ty X))
X))


;; wrap-∀/free-Xs : (Syntax-Listof Id) Type -> Type
;; If the type has free Xs, this wraps the type in an forall with those free Xs.
(define (wrap-∀/free-Xs Xs ty)
(define free-Xs (find-free-Xs Xs ty))
(if (stx-null? free-Xs)
ty
(syntax-parse ty
[(~?∀ (Y ...) ty)
#:with [X ...] free-Xs
((current-type-eval)
(datum->syntax #'ty (list #'∀ #'(X ... Y ...) #'ty) #'ty #'ty))])))

;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
;; stx = the application stx = (#%app e_fn e_arg ...)
;; tyXs = input and output types from fn type
;; ie (typeof e_fn) = (-> . tyXs)
;; It infers the types of arguments from left-to-right,
;; and it expands and returns all of the arguments.
;; It returns list of 3 values if successful, else throws a type error
;; It returns list of 4 values if successful, else throws a type error
;; - a list of all the arguments, expanded
;; - a list of all the argument types
;; - a list of all the type variables
;; - the constraints for substituting the types
(define (solve Xs tyXs stx)
Expand All @@ -140,26 +167,29 @@
'()))
(syntax-parse stx
[(_ e_fn . args)
(define-values (as- cs)
(for/fold ([as- null] [cs initial-cs])
(define-values (Xs* as- a-tys cs)
(for/fold ([Xs Xs] [as- null] [a-tys null] [cs initial-cs])
([a (in-list (syntax->list #'args))]
[tyXin (in-list (syntax->list #'(τ_inX ...)))])
(define ty_in (inst-type/cs Xs cs tyXin))
(define/with-syntax [a- ty_a]
(define/syntax-parse [a- (~?∀* Ys ty_a)]
(infer+erase (if (empty? (find-free-Xs Xs ty_in))
(add-expected-ty a ty_in)
a)))
(values
(define XYs (stx-append Xs #'Ys))
(values
XYs
(cons #'a- as-)
(add-constraints Xs cs (list (list ty_in #'ty_a))
(cons #'ty_a a-tys)
(add-constraints XYs cs (list (list ty_in #'ty_a))
(list (list (inst-type/cs/orig
Xs cs ty_in
(λ (id1 id2)
(equal? (syntax->datum id1)
(syntax->datum id2))))
#'ty_a))))))

(list (reverse as-) Xs cs)])]))
(list (reverse as-) (reverse a-tys) (stx-append #'Vs Xs*) cs)])]))

(define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
(type-error #:src stx
Expand All @@ -172,6 +202,15 @@
(string-join (stx-map type->str expected-tys) ", ")
(string-join (stx-map type->str given-tys) ", "))))

;; inst-type/cs/∀ : (Stx-Listof Id) Constraints Type-Stx -> Type-Stx
;; Instantiates ty with the substitution, possibly wrapping it in a forall.
(define (inst-type/cs/∀ Xs cs ty)
(wrap-∀/free-Xs Xs (inst-type/cs Xs cs ty)))
;; inst-types/cs/∀ : (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) -> (Listof Type-Stx)
;; the plural version of inst-type/cs/∀
(define (inst-types/cs/∀ Xs cs tys)
(stx-map (lambda (t) (inst-type/cs/∀ Xs cs t)) tys))

;; covariant-Xs? : Type -> Bool
;; Takes a possibly polymorphic type, and returns true if all of the
;; type variables are in covariant positions within the type, false
Expand Down Expand Up @@ -352,7 +391,25 @@
[exn:fail:type:infer? (lambda (e) #t)])
(let ([X+ ((current-type-eval) X)])
(not (or (tyvar? X+) (type? X+))))))
(stx-remove-dups Xs))))
(stx-remove-dups Xs)))

(define old-join (current-join))

;; new-join : Type-Stx Type-Stx -> Type-Stx
;; Computes the join of two possibly polymorphic types, by solving the
;; constraint that they should be equal once instantiated.
(define (new-join t1 t2)
(syntax-parse (list t1 t2)
[[(~?∀ (X ...) t1) (~?∀ (Y ...) t2)]
#:with Xs #'(X ... Y ...)
#:with cs (add-constraints #'Xs '() #'([t1 t2]))
#:with [t1* t2*] (inst-types/cs #'Xs #'cs #'[t1 t2])
#:with t1** ((current-type-eval) #`(?∀ #,(find-free-Xs #'Xs #'t1*) t1*))
#:with t2** ((current-type-eval) #`(?∀ #,(find-free-Xs #'Xs #'t2*) t2*))
(old-join #'t1** #'t2**)]))

(current-join new-join)
)

;; define --------------------------------------------------
;; for function defs, define infers type variables
Expand Down Expand Up @@ -503,22 +560,9 @@
. rst)])) ...
(define-syntax (Cons stx)
(syntax-parse stx
; no args and not polymorphic
[C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
; no args but polymorphic, check inferred type
[C:id
#:when (stx-null? #'(τ ...))
#:with τ-expected (syntax-property #'C 'expected-type)
#:fail-unless (syntax-e #'τ-expected)
(raise
(exn:fail:type:infer
(format "~a (~a:~a): ~a: ~a"
(syntax-source stx) (syntax-line stx) (syntax-column stx)
(syntax-e #'C)
(no-expected-type-fail-msg))
(current-continuation-marks)))
#:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
#'(C {τ-expected-arg (... ...)})]
; no args expected, expand to value
[C:id #:when (stx-null? #'(τ ...)) #'(C)]
; no args given, expand to function
[_:id (⊢ StructName (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn
[(C τs e_arg ...)
#:when (brace? #'τs) ; commit to this clause
Expand Down Expand Up @@ -729,7 +773,8 @@
(syntax-parse stx #:datum-literals (with)
[(_ e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with [e- τ_e] (infer+erase #'e)
#:with [e- (~?∀ Xs τ_e)] (infer+erase #'e)
#:fail-unless (stx-null? #'Xs) "add annotations"
(syntax-parse #'clauses #:datum-literals (->)
[([(~seq p ...) -> e_body] ...)
#:with (pat ...) (stx-map ; use brace to indicate root pattern
Expand All @@ -748,7 +793,8 @@
(define-typed-syntax match #:datum-literals (with)
[(_ e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with [e- τ_e] (infer+erase #'e)
#:with [e- (~?∀ Xs τ_e)] (infer+erase #'e)
#:fail-unless (stx-null? #'Xs) "add annotations"
#:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
(cond
[(×? #'τ_e) ;; e is tuple
Expand Down Expand Up @@ -874,7 +920,9 @@
[(_ (~and x+tys ([_ (~datum :) ty] ...)) . body)
#:with Xs (compute-tyvars #'(ty ...))
;; TODO is there a way to have λs that refer to ids defined after them?
#'(?Λ Xs (ext-stlc:λ x+tys . body))])
#:with [f (~?∀ (X ...) (~ext-stlc:→ arg-ty ... (~?∀ (Y ...) body-ty)))]
(infer+erase #'(?Λ Xs (ext-stlc:λ x+tys . body)))
(⊢ f : (?∀ (X ... Y ...) (→ arg-ty ... body-ty)))])


;; #%app --------------------------------------------------
Expand All @@ -883,31 +931,26 @@
;; compute fn type (ie ∀ and →)
#:with [e_fn- (~?∀ Xs (~ext-stlc:→ . tyX_args))] (infer+erase #'e_fn)
;; solve for type variables Xs
#:with [(e_arg- ...) Xs* cs] (solve #'Xs #'tyX_args stx)
#:with [(e_arg- ...) (τ_arg- ...) Xs* cs] (solve #'Xs #'tyX_args stx)
;; instantiate polymorphic function type
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
#:with [τ_in ... τ_out] (inst-types/cs/∀ #'Xs* #'cs #'tyX_args)
;; arity check
#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
(num-args-fail-msg #'e_fn #'(τ_in ...) #'e_args)
;; compute argument types
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
#:with (τ_arg ...) (inst-types/cs/∀ #'Xs* #'cs #'(τ_arg- ...))
;; typecheck args
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'e_args)
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
#'τ_out
(syntax-parse #'τ_out
[(~?∀ (Y ...) τ_out)
(unless (→? #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
(for ([X (in-list (syntax->list #'(unsolved-X ...)))])
(unless (covariant-X? X #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
#'(∀ (unsolved-X ... Y ...) τ_out)]))
#:with τ_out* (syntax-parse #'τ_out
[(~?∀ (X ...) (~?∀ (Y ...) τ_out))
(for ([X (in-list (syntax->list #'(X ...)))]
#:when (stx-contains-id? #'Xs X)) ;; To cause an error, the X must be part of the original signature (I think?)
(unless (covariant-X? X #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
#'(?∀ (X ... Y ...) τ_out)])
(⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])


;; cond and other conditionals
(define-typed-syntax cond
[(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
Expand Down
33 changes: 20 additions & 13 deletions macrotypes/examples/tests/mlish-tests.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,7 +260,7 @@
(check-type (Leaf 10) : (Tree Int))
(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))

(typecheck-fail Nil #:with-msg "Nil: no expected type, add annotations")
(check-type (λ () Nil) : (→/test {X} (List X)))
(typecheck-fail (Cons 1 (Nil {Bool}))
#:with-msg
"expected: \\(List Int\\)\n *given: \\(List Bool\\)")
Expand All @@ -272,11 +272,11 @@
(typecheck-fail (Cons {Bool} 1 Nil)
#:with-msg
(string-append
"Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(List Bool\\)\n"
"Cons: type mismatch\n *expected: +Bool, \\(List Bool\\)\n *given: +Int, \\(\\?∀ \\(\\) \\(List X\\)\\)\n"
" *expressions: 1, Nil"))

(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
#:with-msg "Nil: no expected type, add annotations")
#:with-msg "match: add annotations")
(check-type
(match (Nil {Int}) with
[Cons x xs -> 2]
Expand Down Expand Up @@ -359,13 +359,16 @@
;; nested lambdas

(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 : X]) y)) : (→/test X (→ Y Y)))
(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test X (→ Y Y)))
(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))

(check-type
((λ ([x : X]) (λ ([y : Y]) y)) 1)
: (→/test Y Y))
Copy link
Owner

@stchang stchang Oct 10, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would the original test still pass?

Copy link
Contributor Author

@SuzanneSoy SuzanneSoy Oct 10, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, that's one of the remaining issues.

With @AlexKnauth's change which lifts nested ∀ from the function's return type, the outer lambda has type (∀ (X Y) (→ X (→ Y Y))), but then the value restriction kicks in, and prevents Y from appearing in covariant positions (in case the body was a let-over-lambda capturing the Y type).

If I revert that commit, then the outer lambda's type is (∀ (X) (→ X (∀ (Y) (→ Y Y)))) (which sounds good to me as I used Typed Racket a lot, but @AlexKnauth I'm not sure if it is okay to revert that commit). The problem then becomes that (∀ (Y) (→ Y Y)) cannot be annotated as (→ Int Int), because the former is not a subtype of the former (an explicit instantiation is needed instead).

So I'm trying to see if I can find some combination of changes to solve + add-constraints + subtyping which makes everything work.

Copy link
Owner

@stchang stchang Oct 10, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, yes I'm playing around a bit more and see the behavior you mention. I'm starting to remember now and I think that was one of the original holdups because it means programs like (((λ ([x : X]) (λ ([y : Y]) y)) 1) 1) will be rejected which is not ideal.

Thanks for the update and thanks for work on this!

Copy link
Collaborator

@AlexKnauth AlexKnauth Oct 11, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The type of the outer lambda should be (∀ (X Y) (→ X (→ Y Y))) so that type inference can instantiate either X or Y if it needs to. Here it needs to instantiate X as Int, but Y isn't constrained. So why is Y also solved to Int here?

Copy link
Contributor Author

@SuzanneSoy SuzanneSoy Oct 11, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@AlexKnauth I'm not sure what you mean by "why is Y also solved to Int here?", could you clarify? Thanks!

Tentative answer: In that test, the (check-type … : (→ Int Int)) places an expected-type on the outer lambda's return value, which allows the Y to be instantiated to Int (but then the return type cannot be left as (→ Y Y), as the value restriction forces it to be monomorphic, IIUC).

Copy link
Collaborator

@AlexKnauth AlexKnauth Oct 11, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, right. So the test could just as easily be (check-type … : (→ String String)) and it would still pass. The Y in the answer we want should a non-generalizable type variable, like the ones notated '_a in the "Relaxing the Value Restriction" paper.

: (→ Int Int))
(check-type
((λ ([x : X]) (λ ([y : Y]) y)) 1)
: (→ String String))

;; TODO?
;; - this fails if polymorphic functions are allowed as HO args
Expand All @@ -378,14 +381,15 @@

(check-type
((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
: (→/test {Y} Y (→/test {Z} Z Z)))

: (→/test Int (→ String String)))
(check-type
((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
: (→/test String (→ Int Int)))
(check-type (inst Cons (→/test X X))
: (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
(check-type map : (→/test (→ X Y) (List X) (List Y)))

(check-type (Cons (λ ([x : X]) x) Nil)
: (List (→/test {X} X X)))
: (?∀ {X} (List (→ X X))))

(define (nn [x : X] -> (→ (× X (→ Y Y))))
(λ () (tup x (λ ([x : Y]) x))))
Expand Down Expand Up @@ -419,6 +423,8 @@
(check-type (let ([x (nn4)])
x)
: (→/test (Option X)))
(check-type (λ () (nn4)) : (→/test (→ (Option X))))


(define (nn5 -> (→ (Ref (Option X))))
(λ () (ref (None {X}))))
Expand All @@ -430,6 +436,7 @@
(let ([r (((inst nn5 X)))])
(λ () (deref r))))
(check-type (nn6) : (→/test (Option X)))
(check-type (λ () (nn6)) : (→/test (→ (Option X))))

;; A is covariant, B is invariant.
(define-type (Cps A B)
Expand All @@ -449,6 +456,7 @@
(check-type (let ([x (nn8)])
x)
: (→/test (Cps (Option A) Int)))
(check-type (λ () (nn8)) : (→/test (→ (Cps (Option A) Int))))

(define-type (Result A B)
(Ok A)
Expand Down Expand Up @@ -748,7 +756,7 @@
(typecheck-fail
(if #t 1 "2")
#:with-msg
"branches have incompatible types: Int and String")
"couldn't unify Int and String")

;; tests from stlc+lit-tests.rkt --------------------------
; most should pass, some failing may now pass due to added types/forms
Expand Down Expand Up @@ -778,7 +786,7 @@

(typecheck-fail
(+ 1 (λ ([x : Int]) x))
#:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
#:with-msg "couldn't unify Int and \\(\\?∀ \\(\\) \\(→ Int Int\\)\\)")
(typecheck-fail
(λ ([x : (→ Int Int)]) (+ x x))
#:with-msg "expected: Int\n *given: \\(→ Int Int\\)")
Expand All @@ -787,4 +795,3 @@
#:with-msg "wrong number of arguments: expected 2, given 1\n *expected: +Int, Int\n *arguments: 1")

(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)

6 changes: 3 additions & 3 deletions macrotypes/examples/tests/mlish/match2.mlish
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,14 @@
(match2 (B (tup 2 3)) with
[A x -> x]
[C (x,y) -> y]
[B x -> x]) #:with-msg "branches have incompatible types: Int and \\(× Int Int\\)")
[B x -> x]) #:with-msg "couldn't unify Int and \\(× Int Int\\)")

(typecheck-fail
(match2 (B (tup 2 3)) with
[A x -> (tup x x)]
[C x -> x]
[B x -> x])
#:with-msg "branches have incompatible types: \\(× Int Int\\) and \\(× Int \\(× Int Int\\)\\)")
#:with-msg "couldn't unify Int and \\(× Int Int\\)")

(check-type
(match2 (B (tup 2 3)) with
Expand Down Expand Up @@ -52,7 +52,7 @@
(match2 (A (tup 2 3)) with
[B (x,y) -> y]
[A x -> x]
[C x -> x]) #:with-msg "branches have incompatible types")
[C x -> x]) #:with-msg "couldn't unify Int and \\(× Int Int\\)")

(check-type
(match2 (A 1) with
Expand Down
Loading