TR case-> inference

[Stephen Chang]

For this function:

(define (f [x : (U Integer Boolean)])
(if (integer? x) (add1 x) "1"))

Typed Racket infers the type:

(-> (U Boolean Integer) (U Integer String))

and also recognizes this equivalent case-> type:

(ann f : (case-> (-> Boolean (U Integer String))
(-> Integer (U Integer String))))

but does not recognize this correct type:

(ann f : (case-> (-> Boolean String)
(-> Integer Integer)))
=>
Type Checker: type mismatch
expected: (case-> (-> Boolean String) (-> Integer Integer))
given: (-> (U Boolean Integer) (U Integer String)) in: f

Is there a reason TR cannot compute the last type? Is it a performance issue?

[Alex Knauth]

The only reason it couldn't assign that type is because of the type annotation you put on x. If you take away the (U Integer Boolean) annotation an x this works:

#lang typed/racket
(: f : (case-> (-> Boolean String)
(-> Integer Integer)))
(define (f x)

(if (integer? x) (add1 x) "1"))

Once you put the (U Integer Boolean) annotation, it can treat f as having any super type of (-> (U Boolean Integer) (U Integer String)), but it won't infer anything more specific than what the annotations say.

P.S.

> (case-> (-> Boolean (U Integer String))
> (-> Integer (U Integer String)))

This is a super-type of (-> (U Boolean Integer) (U Integer String)). It's a super-type because both (-> Boolean (U Integer String)) and (-> Integer (U Integer String)) are super-types. It's not equivalent under the current sub-typing rules though, because you can't pass a value of type (U Integer Boolean) to it.

Alex Knauth

[Stephen Chang]

Thanks, that makes sense.

I guess I was wondering if it would be sound to treat U inputs
specially and convert the function type to a case-> first, and then
compute the return type of each case individually, to get the more
precise type.

As I'm typing this out, I realize that my suggestion would introduce
an ordering. But could intersection types help here?

> --
> You received this message because you are subscribed to the Google Groups "Racket Developers" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-dev+...@googlegroups.com.
> To post to this group, send email to racke...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/2DA1A499-A4D2-48EE-AAC6-CF92C34274F6%40knauth.org.
> For more options, visit https://groups.google.com/d/optout.