<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body>
    Sigh, floating point.  Yes, this is the most difficult corner of
    this work.  <br>
    <br>
    Bear in mind that you're really asking questions about cast
    conversion.  Additionally, we have to define which of these casts
    are "lossy" vs which are "information preserving" (exact), which for
    most numbers is straightforward but for weird floating point values
    might be harder.   So let's first see what happens when we cast your
    examples:<br>
    <br>
    jshell> (int) 2.0f<br>
    $1 ==> 2<br>
    <br>
    jshell> (int) 2.5f<br>
    $2 ==> 2<br>
    <br>
    jshell> (float) Double.MAX_VALUE<br>
    Infinity<br>
    <br>
    jshell> (float) Math.PI<br>
    $4 ==> 3.1415927<br>
    <br>
    jshell> (float) Double.NaN<br>
    $5 ==> NaN<br>
    <br>
    jshell> (double) Double.NaN<br>
    $6 ==> NaN<br>
    <br>
    Clearly #2 (casting 2.5 to int) is lossy, and therefore would not be
    exact, so we can cross that one off the list.  Similar for
    Double.MAX_VALUE to float.  It's also pretty clear that Math.PI --
    which is merely an alias for 3.14159265358979323846 -- is also not
    representable in the range of float.  <br>
    <br>
    So that leaves:<br>
    <br>
        2.0 instanceof int<br>
        Double.NaN instanceof float<br>
        Double.NaN instanceof double<br>
    <br>
    The first one is an exact cast; this can be specified in a number of
    ways, including "sufficient number of low order bits are zero", or
    "representable in the range of the target type", or others.  The
    binary representation of 2.0f is 01000000000000000000000000000000,
    which exactly encodes an integer.  Again, this is not a rule about
    `instanceof`; this is derived from casting (though we do have to
    define what exactness means.)  <br>
    <br>
    For NaN, negative zero, and infinity, whether various conversions
    are exact or not may require a somewhat ad-hoc decision, but I think
    the intuitive answers for NaN is that Float.NaN <-->
    Double.NaN is exact, and similar for Float.Inf <-->
    Double.Inf.  There will be an argument about -0.0 and 0.0.  <br>
    <br>
    <blockquote type="cite">Intuitively, I think I would expect that if
      t is an expression of primitive type T, and U is also a primitive
      type, then <font face="monospace">t instanceof U</font><font face="arial, sans-serif"> is true iff</font> t == (T) (U) t.
      (Perhaps with a variant of == that is reflexive even for NaN, or
      perhaps not.) That would make (1) true, (2,3,4) false, and (5,6)
      who knows.</blockquote>
    <br>
    This is a good intuition, and is true for some types, and almost
    true for others, but it falls into some holes.  In particular, with
    some conversions, `(U) t` is lossy but `(T) (U) t` is also lossy in
    an exactly compensating way.  <br>
    <br>
    <blockquote type="cite" cite="mid:CAChqX89jk3v10B2q4kA6xHJE9uf2Y7ZBYEgb_859YXxzzx4HNQ@mail.gmail.com">
      
      <div dir="ltr">This makes a lot of sense. I'm wondering, though,
        how it works with float and double. I don't see the answer by
        looking at JLS Ch5. Are the following expressions legal, and if
        so which ones are true?
        <div>
          <ol>
            <li>2.0 instanceof int</li>
            <li>2.5 instanceof int</li>
            <li>Double.MAX_VALUE instanceof float</li>
            <li>Math.PI instanceof float</li>
            <li>Double.NaN instanceof float</li>
            <li>Double.NaN instanceof double</li>
          </ol>
          <div>Intuitively, I think I would expect that if t is an
            expression of primitive type T, and U is also a primitive
            type, then <font face="monospace">t instanceof U</font><font face="arial, sans-serif"> is true iff</font> t == (T) (U)
            t. (Perhaps with a variant of == that is reflexive even for
            NaN, or perhaps not.) That would make (1) true, (2,3,4)
            false, and (5,6) who knows.</div>
        </div>
      </div>
      <br>
      <div class="gmail_quote">
        <div dir="ltr" class="gmail_attr">On Thu, 8 Sept 2022 at 09:53,
          Brian Goetz <<a href="mailto:brian.goetz@oracle.com" moz-do-not-send="true" class="moz-txt-link-freetext">brian.goetz@oracle.com</a>>
          wrote:<br>
        </div>
        <blockquote class="gmail_quote" style="margin:0px 0px 0px
          0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
          <div> <font size="4"><font face="monospace">Earlier in the
                year we talked about primitive type patterns.  Let me
                summarize<br>
                the past discussion, what I think the right direction
                is, and why this is (yet<br>
                another) "finishing up the job" task for basic patterns
                that, if left undone,<br>
                will be a sharp edge.<br>
                <br>
                Prior to record patterns, we didn't support primitive
                type patterns at all. With<br>
                records, we now support primitive type patterns as
                nested patterns, but they are<br>
                very limited; they are only applicable to exactly their
                own type.  <br>
                <br>
                The motivation for "finishing" primitive type patterns
                is the same as discussed<br>
                earlier this week with array patterns -- if pattern
                matching is the dual of<br>
                aggregation, we want to avoid gratuitous asymmetries
                that let you put things<br>
                together but not take them apart.  <br>
                <br>
                Currently, we can assign a `String` to an `Object`, and
                recover the `String`<br>
                with a pattern match:<br>
                <br>
                    Object o = "Bob";<br>
                    if (o instanceof String s) { println("Hi Bob"); }<br>
                <br>
                Analogously, we can assign an `int` to a `long`:<br>
                <br>
                    long n = 0;<br>
                <br>
                but we cannot yet recover the int with a pattern match:<br>
                <br>
                    if (n instanceof int i) { ... } // error, pattern
                `int i` not applicable to `long`<br>
                <br>
                To fill out some more of the asymmetries around records
                if we don't finish the job: given <br>
                <br>
                    record R(int i) { }<br>
                <br>
                we can construct it with<br>
                <br>
                    new R(anInt)     // no adaptation<br>
                    new R(aShort)    // widening<br>
                    new R(anInteger) // unboxing<br>
                <br>
                but yet cannot deconstruct it the same way:<br>
                <br>
                    case R(int i)     // OK<br>
                    case R(short s)   // nope<br>
                    case R(Integer i) // nope<br>
                <br>
                It would be a gratuitous asymmetry that we can use
                pattern matching to recover from<br>
                reference widening, but not from primitive widening. 
                While many of the<br>
                arguments against doing primitive type patterns now were
                of the form "let's keep<br>
                things simple", I believe that the simpler solution is
                actually to _finish the<br>
                job_, because this minimizes asymmetries and potholes
                that users would otherwise<br>
                have to maintain a mental catalog of.  <br>
                <br>
                Our earlier explorations started (incorrectly, as it
                turned out), with<br>
                assignment context.  This direction gave us a good push
                in the right direction,<br>
                but turned out to not be the right answer.  A more
                careful reading of JLS Ch5<br>
                convinced me that the answer lies not in assignment
                conversion, but _cast<br>
                conversion_.  <br>
                <br>
                #### Stepping back: instanceof<br>
                <br>
                The right place to start is actually not patterns, but
                `instanceof`.  If we<br>
                start here, and listen carefully to the specification,
                it leads us to the<br>
                correct answer.  <br>
                <br>
                Today, `instanceof` works only for reference types. 
                Accordingly, most people<br>
                view `instanceof` as "the subtyping operator" -- because
                that's the only<br>
                question we can currently ask it.  We almost never see
                `instanceof` on its own;<br>
                it is nearly always followed by a cast to the same
                type.  Similarly, we rarely<br>
                see a cast on its own; it is nearly always preceded by
                an `instanceof` for the<br>
                same type.  <br>
                <br>
                There's a reason these two operations travel together:
                casting is, in general,<br>
                unsafe; we can try to cast an `Object` reference to a
                `String`, but if the<br>
                reference refers to another type, the cast will fail. 
                So to make casting safe,<br>
                we precede it with an `instanceof` test.  The semantics
                of `instanceof` and<br>
                casting align such that `instanceof` is the precondition
                test for safe casting.<br>
                <br>
                > instanceof is the precondition for safe casting<br>
                <br>
                Asking `instanceof T` means "if I cast this to T, would
                I like the answer."<br>
                Obviously CCE is an unlikable answer; `instanceof`
                further adopts the opinion<br>
                that casting `null` would also be an unlikable answer,
                because while the cast<br>
                would succeed, you can't do anything useful with the
                result.<br>
                <br>
                Currently, `instanceof` is only defined on reference
                types, and on this domain<br>
                coincides with subtyping.  On the other hand, casting is
                defined between<br>
                primitive types (widening, narrowing), and between
                primitive and reference types<br>
                (boxing, unboxing).  Some casts involving primitives
                yield "better" results than<br>
                others; casting `0` to `byte` results in no loss of
                information, since `0` is<br>
                representable as a byte, but casting `500` to `byte`
                succeeds but loses<br>
                information because the higher order bits are discarded.
                 <br>
                <br>
                If we characterize some casts as "lossy" and others as
                "exact" -- where lossy<br>
                means discarding useful information -- we can extend the
                "safe casting<br>
                precondition" meaning of `instanceof` to primitive
                operands and types in the<br>
                obvious way -- "would casting this expression to this
                type succeed without error<br>
                and without information loss."  If the type of the
                expression is not castable to<br>
                the type we are asking about, we know the cast cannot
                succeed and reject the<br>
                `instanceof` test at compile time.<br>
                <br>
                Defining which casts are lossy and which are exact is
                fairly straightforward; we<br>
                can appeal to the concept already in the JLS of
                "representable in the range of a<br>
                type."  For some pairs of types, casting is always exact
                (e.g., casting `int` to<br>
                `long` is always exact); we call these "unconditionally
                exact".  For other pairs<br>
                of types, some values can be cast exactly and others
                cannot.  <br>
                <br>
                Defining which casts are exact gives us a simple and
                precise semantics for `x<br>
                instanceof T`: whether `x` can be cast exactly to `T`. 
                Similarly, if the static<br>
                type of `x` is not castable to `T`, then the
                corresponding `instanceof` question<br>
                is rejected statically.  The answers are not suprising:<br>
                <br>
                 - Boxing is always exact;<br>
                 - Unboxing is exact for all non-null values;<br>
                 - Reference widening is always exact;<br>
                 - Reference narrowing is exact if the type of the
                target expression is a<br>
                   subtype of the target type;<br>
                 - Primitive widening and narrowing are exact if the
                target expression can be<br>
                   represented in the range of the target type.<br>
                <br>
                #### Primitive type patterns<br>
                <br>
                It is a short hop from `instanceof` to patterns
                (including primitive type<br>
                patterns, and reference type patterns applied to
                primitive types), which can be<br>
                defined entirely in terms of cast conversion and
                exactness: <br>
                <br>
                 - A type pattern `T t` is applicable to a target of
                type `S` if `S` is<br>
                   cast-convertible to `T`;<br>
                 - A type pattern `T t` matches a target `x` if `x` can
                be cast exactly to `T`;<br>
                 - A type pattern `T t` is unconditional at type `S` if
                casting from `T` to `S`<br>
                   is unconditionally exact;<br>
                 - A type pattern `T t` dominates a type pattern `S s`
                (or a record pattern<br>
                   `S(...)`) if `T t` would be unconditional on `S`.<br>
                <br>
                While the rules for casting are complex, primitive
                patterns add no new<br>
                complexity; there are no new conversions or conversion
                contexts.  If we see:<br>
                <br>
                    switch (a) { <br>
                        case T t: ...<br>
                    }<br>
                <br>
                we know the case matches if `a` can be cast exactly to
                `T`, and the pattern is<br>
                unconditional if _all_ values of `a`'s type can be cast
                exactly to `T`.  Note<br>
                that none of this is specific to primitives; we derive
                the semantics of _all_<br>
                type patterns from the enhanced definition of casting.<br>
                <br>
                Now, our record deconstruction examples work
                symmetrically to construction: <br>
                <br>
                    case R(int i)     // OK<br>
                    case R(short s)   // test if `i` is in the range of
                `short`<br>
                    case R(Integer i) // box `i` to `Integer`<br>
                <br>
                <br>
              </font></font> </div>
        </blockquote>
      </div>
    </blockquote>
    <br>
  </body>
</html>