more-complete-application RFC

[pnwamk]

TL;DR for case-> types, we're proposing to apply all
possible ->'s to compute the return type instead of
just the first applicable arrow.

Longer:

Some functions use a case-> type, which indicates that
multiple simpler function types work together to describe
the function's behavior.

For example, a simple addition function designed to add
integers with the same sign could be written as follows:

(: plus (case->
         [Nonnegative-Integer Nonnegative-Integer -> Nonnegative-Integer]
         [Nonpositive-Integer Nonpositive-Integer -> Nonpositive-Integer]))
(define (plus x y)
  (+ x y))

Old behavior: up until now, when type checking the application of a case->,
Typed Racket searches for the first applicable arrow and then uses that
return type. E.g.,

(ann (plus 42 42) Nonnegative-Integer) ;; first arrow
(ann (plus -42 -42) Nonpositive-Integer) ;; second arrow
(ann (plus 0 0) Nonnegative-Integer) ;; first arrow

New proposed behavior: when calculating the resulting type for specific
use cases, each applicable -> type in the case-> contributes
to determining the result type:

(ann (plus 42 42) Nonnegative-Integer) ;; first arrow
(ann (plus -42 -42) Nonpositive-Integer) ;; second arrow
(ann (plus 0 0) Zero) ;; first _and_ second arrow!

In other words, the first two examples correspond to the
first and second arrows respectively, but the third example
fits both descriptions, and so the resulting type is the
intersection of both result types, i.e. the type which
describes values that are both nonnegative and nonpositive
integers (namely Zero).

[stamourv]

That sounds great!
And, as your example shows, that should make it possible to simplify the types of numeric operations tremendously.

[pnwamk]

TL;DR To fully benefit from these proposed changes, improvements
to subtyping and inference are needed as well. I'm not sure what the
change to inference would look like at the moment...

Longer:

After looking at an initial implementation of this feature and then
attempting to reduce the size of some numeric tower types (i.e. #757),
it seems to me that to fully benefit from this added feature, we need
all three of the following:

1. Function application that can apply all applicable arrows
   w.r.t. the given argument types.

2. Subtyping needs to be extended to reason more completely about
   the meaning of function types.

3. Type inference also needs to be extended to reason more
   completely about the meaning of function types.

An example:

With the improve function application (1), we can simplify
the type of add1 from this:

[add1 (from-cases
       (-> -Zero -One)
       (-> -One -PosByte)
       (-> -Byte -PosIndex)
       (-> -Index -PosFixnum)
       (-> -NegFixnum -NonPosFixnum)
       (-> -NonPosFixnum -Fixnum)
       (-> -Nat -Pos)
       (-> -NegInt -NonPosInt)
       (-> -Int -Int)
       (-> -NonNegRat -PosRat)
       (-> -Rat)
       (-> -NonNegFlonum -PosFlonum)
       (-> -Flonum)
       (-> -NonNegSingleFlonum -PosSingleFlonum)
       (-> -SingleFlonum)
       (-> -NonNegInexactReal -PosInexactReal)
       (-> -InexactReal)
       (-> -NonNegReal -PosReal)
       (-> -Real -Real)
       (-> -FloatComplex -FloatComplex)
       (-> -SingleFlonumComplex -SingleFlonumComplex)
       (-> -InexactComplex -InexactComplex)
       (-> N N))]

to this:

[add1 (from-cases
       (-> -Zero -One)
       (-> -One -Byte)
       (-> -Byte -Index)
       (-> -Index -Fixnum)
       (-> -NonPosFixnum -Fixnum)
       (-> -NegInt -NonPosInt)
       (-> -NonNegReal -PosReal)
       (-> -InexactReal -InexactReal)
       (-> -Int -Int)
       (-> -Rat -Rat)
       (-> -Flonum -Flonum)
       (-> -SingleFlonum -SingleFlonum)
       (-> -FloatComplex -FloatComplex)
       (-> -SingleFlonumComplex -SingleFlonumComplex)
       (-> -Real -Real)
       (-> -InexactReal -InexactReal)
       (-> -InexactComplex -InexactComplex)
       (-> N N))]

This seems nice... but we see someproblems if we consider a few
short examples.

First, in Typed Racket today:

#lang typed/racket

(define x : Index 42)

(add1 x) ;; type checks at Positive-Fixnum

(ann add1 (-> Index Positive-Fixnum)) ;; type checks fine

(build-list x add1) ;; type checks at (Listof Positive-Fixnum)

All three terms using add1 type check. All of these cases in
Typed Racket today rely on the explicit (-> Index Positive-Fixnum)
in add1's case->.

If we improve only function application (so it uses all
applicable arrows) but leave subtyping and inference alone, only
the first usage of add1 retains its behavior:

#lang typed/racket

(define x : Index 42)

(add1 x) ;; type checks at Positive-Fixnum

(ann add1 (-> Index Positive-Fixnum)) ;; fails to type check

(build-list x add1) ;; type checks at (Listof Fixnum)

The first still type checks at Positive-Fixnumbecause, although
add1 does not explicitly contain a case for (-> Index Positive-Fixnum), the return type Positive-Fixnum is derivable
given the new, simpler type and our improved function
application.

The second fails to type check because subtyping is not reasoning
more than one arrow at a time (it would need to act similar to
function application -- this improvement I think would be very doable).

The third type checks at a less precise type because inference does not
now how to leverage multiple arrows in add1's type to derive
Positive-Fixnum---instead it simply uses the first that satisfies
the set of generated constraints, which is Fixnum. This last issue
I'm not sure what the "right" fix would be. I need to go do some
reading on type inference =\