commit 9920c5791d45a222f77af61d317c81fd7d286da5
parent 5b64b3b042ad2b76e8efba3fd1fb16f44b3df51f
Author: AlexKnauth <alexander@knauth.org>
Date: Wed, 4 May 2016 18:09:44 -0400
modify #%app to deal with under-constrained function applications
fixes #16
Diffstat:
3 files changed, 140 insertions(+), 28 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -71,23 +71,30 @@
#'τ]
[(_ . rst) (lookup x #'rst)]
[() #f]))
-
- ;; Returns list of types, for each X in Xs,
- ;; if it's possible to solve for such types from constraints cs
- ;; else returns #f
- (define (try-to-solve Xs cs)
- (define maybe-solved
- (filter (lambda (x) x) (stx-map (λ (X) (lookup X cs)) Xs)))
- (and (stx-length=? Xs maybe-solved)
- maybe-solved))
+
+ ;; find-unsolved-Xs : (Stx-Listof Id) Constraints -> (Listof Id)
+ ;; finds the free Xs that aren't constrained by cs
+ (define (find-unsolved-Xs Xs cs)
+ (for/list ([X (in-list (stx->list Xs))]
+ #:when (not (lookup X cs)))
+ X))
+
+ ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
+ ;; looks up each X in the constraints, returning the X if it's unconstrained
+ (define (lookup-Xs/keep-unsolved Xs cs)
+ (for/list ([X (in-list (stx->list Xs))])
+ (or (lookup X cs) X)))
;; 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)
- ;; returns list of types if success, else throws type error
- ;; - infers type of arguments from left-to-right
- ;; - short circuits if done early
+ ;; It infers the types of arguments from left-to-right,
+ ;; and it short circuits if it's done early.
+ ;; It returns list of 3 values if successful, else throws a type error
+ ;; - a list of the arguments that it expanded
+ ;; - a list of the the un-constrained type variables
+ ;; - a list of types to fill in for the Xs
(define (solve Xs tyXs stx)
(syntax-parse tyXs
[(τ_inX ... τ_outX)
@@ -103,20 +110,19 @@
(for/fold ([as- null] [cs initial-cs])
([a (in-list (syntax->list #'args))]
[tyXin (in-list (syntax->list #'(τ_inX ...)))]
- #:break (try-to-solve Xs cs))
+ #:break (empty? (find-unsolved-Xs Xs cs)))
(define/with-syntax [a- ty_a] (infer+erase a))
(values
(cons #'a- as-)
(stx-append cs (compute-constraint (list tyXin #'ty_a))))))
- (define maybe-solved-tys (try-to-solve Xs cs))
-
- (if maybe-solved-tys
- (list (reverse as-) maybe-solved-tys)
- (type-error #:src stx
- #:msg (mk-app-err-msg stx #:expected #'(τ_inX ...)
- #:given (stx-map stx-cadr (infers+erase #'args))
- #:note (format "Could not infer instantiation of polymorphic function ~a."
- (syntax->datum (get-orig #'e_fn))))))])]))
+
+ (list (reverse as-) (find-unsolved-Xs Xs cs) (lookup-Xs/keep-unsolved Xs cs))])]))
+
+ (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
+ (type-error #:src stx
+ #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
+ #:note (format "Could not infer instantiation of polymorphic function ~a."
+ (syntax->datum (get-orig e_fn))))))
;; instantiate polymorphic types
(define (inst-type tys-solved Xs ty)
@@ -705,7 +711,7 @@
#'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
[else
;; ) solve for type variables Xs
- (define/with-syntax ((e_arg1- ...) tys-solved) (solve #'Xs #'tyX_args stx))
+ (define/with-syntax ((e_arg1- ...) (unsolved-X ...) tys-solved) (solve #'Xs #'tyX_args stx))
;; ) instantiate polymorphic function type
(syntax-parse (inst-types #'tys-solved #'Xs #'tyX_args)
[(τ_in ... τ_out) ; concrete types
@@ -737,7 +743,14 @@
(equal? (syntax->datum x) (syntax->datum y))))))
(set-stx-prop/preserved tyin 'orig (list new-orig)))
#'(τ_in ...)))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)])])]
+ #: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))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))
+ (⊢ (#%app e_fn- e_arg- ...) : τ_out*)])])]
[(_ e_fn . e_args) ; err case; e_fn is not a function
#:with [e_fn- τ_fn] (infer+erase #'e_fn)
(type-error #:src stx
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -55,8 +55,7 @@
(check-type g2 : (→/test (List Y) (List Y)))
(typecheck-fail (g2 1)
#:with-msg
- (expected "(List Y)" #:given "Int"
- #:note "Could not infer instantiation of polymorphic function"))
+ (expected "(List Y)" #:given "Int"))
;; todo? allow polymorphic nil?
(check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int}))
@@ -353,6 +352,107 @@
(inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int))
: (→ Int (→ Int Int)))
+(check-type
+ ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1)
+ : (→/test {Y} Y (→/test {Z} Z Z)))
+
+(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)))
+
+(define (nn [x : X] -> (→ (× X (→ Y Y))))
+ (λ () (tup x (λ ([x : Y]) x))))
+(define nn-1 (nn 1))
+(check-type (nn-1) : (× Int (→ String String)))
+(check-type (nn-1) : (× Int (→ (List Int) (List Int))))
+
+(define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z))))
+ (λ () (tup x (λ ([x : Y]) x) Nil)))
+(define nn2-1 (nn2 1))
+(check-type (nn2-1) : (× Int (→ String String) (List (List Int))))
+(check-type (nn2-1) : (× Int (→ (List Int) (List Int)) (List String)))
+;; test inst order
+(check-type ((inst nn2-1 String (List Int))) : (× Int (→ String String) (List (List Int))))
+(check-type ((inst nn2-1 (List Int) String)) : (× Int (→ (List Int) (List Int)) (List String)))
+
+(define-type (Result A B)
+ (Ok A)
+ (Error B))
+
+(define (ok [a : A] → (Result A B))
+ (Ok a))
+(define (error [b : B] → (Result A B))
+ (Error b))
+
+(check-type (if (zero? (random 2))
+ (ok 0)
+ (error "didn't get a zero"))
+ : (Result Int String))
+
+(define result-if-0
+ (λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+ (match b with
+ [Ok a -> (succeed a)]
+ [Error b -> (fail b)])))
+(check-type result-if-0
+ : (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2)))
+
+(define (result-if-1 [b : (Result A1 B1)]
+ → (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2)))
+ (λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))])
+ (result-if-0 b succeed fail)))
+(check-type result-if-1
+ : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2))
+ (Result A2 B2))))
+(check-type (inst (result-if-1 (Ok {Int String} 1)) (List Int) (List String))
+ : (→ (→ Int (Result (List Int) (List String)))
+ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type (inst (result-if-1 (Error {Int String} "bad")) (List Int) (List String))
+ : (→ (→ Int (Result (List Int) (List String)))
+ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type ((result-if-1 (Ok {Int String} 1))
+ (λ ([a : Int]) (ok (Cons a Nil)))
+ (λ ([b : String]) (error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+;; same thing, but without the lambda annotations:
+(check-type ((result-if-1 (Ok {Int String} 1))
+ (λ (a) (ok (Cons a Nil)))
+ (λ (b) (error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+
+(define (result-if-2 [b : (Result A1 B1)]
+ → (→ (→ A1 (Result A2 B2))
+ (→ (→ B1 (Result A2 B2))
+ (Result A2 B2))))
+ (λ ([succeed : (→ A1 (Result A2 B2))])
+ (λ ([fail : (→ B1 (Result A2 B2))])
+ (result-if-0 b succeed fail))))
+(check-type result-if-2
+ : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2))
+ (→ (→ B1 (Result A2 B2))
+ (Result A2 B2)))))
+(check-type (inst (result-if-2 (Ok {Int String} 1)) (List Int) (List String))
+ : (→/test (→ Int (Result (List Int) (List String)))
+ (→ (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String)))))
+(check-type ((result-if-2 (Ok {Int String} 1))
+ (λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
+ : (→/test (→ String (Result (List Int) (List String)))
+ (Result (List Int) (List String))))
+(check-type (((result-if-2 (Ok {Int String} 1))
+ ; type annotations are necessary here:
+ (λ ([a : Int]) (Ok {(List Int) (List String)} (Cons a Nil))))
+ ; but not here:
+ (λ (b) (Error (Cons b Nil))))
+ : (Result (List Int) (List String)))
+
;; records and automatically-defined accessors and predicates
(define-type (RecoTest X Y)
(RT1 [x : X] [y : Y] [z : String])
diff --git a/tapl/tests/mlish/match2.mlish b/tapl/tests/mlish/match2.mlish
@@ -59,11 +59,10 @@
[A x -> x]
[_ -> -1]) : Int -> 1)
-;; TODO: better err msg, is actually a type err
(typecheck-fail
(match2 (B 1) with
[B x -> x])
- #:with-msg "Could not infer instantiation of polymorphic function B")
+ #:with-msg (expected "(× X X)" #:given "Int"))
(check-type
(match2 (B (tup 2 3)) with
