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? On Mon, Aug 8, 2016 at 7:55 PM, Alex Knauth <[email protected]> wrote: > >> On Aug 8, 2016, at 6:01 PM, Stephen Chang <[email protected]> wrote: >> >> 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? > > 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 > > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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. -- 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 [email protected]. To post to this group, send email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-dev/CAFfiA1J_UnfxTxsARCbAtXsDaW3gN1htb6P6BdoyvFyL6CZ83g%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
