<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
+1 on this suggestion. I believe it is the only approach that could make switch on floats at all useful, and it would be very useful, as Joe says, for expressing special cases in math libraries clearly.
<div class=""><br class="">
</div>
<div class="">—Guy<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Sep 13, 2022, at 1:07 PM, Joe Darcy <<a href="mailto:joe.darcy@oracle.com" class="">joe.darcy@oracle.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="">
<div class="moz-cite-prefix">On 9/13/2022 9:55 AM, Brian Goetz wrote:<br class="">
</div>
<blockquote type="cite" cite="mid:5bf2de36-4e56-cb68-2fe3-972d4cadebb8@oracle.com" class="">
<br class="">
<blockquote type="cite" class="">It is common for math library methods to have a preamble to screen out special values (infinities, NaN, 0.0, 1.0, etc.).
<br class="">
<br class="">
This would be a reasonable use of a switch on float/double switch. <br class="">
<br class="">
<br class="">
</blockquote>
<br class="">
Which raises some questions (again) of the semantics of constant patterns for exotic floating point values, especially (again) negative zero.
<br class="">
</blockquote>
<p class=""><br class="">
</p>
<p class="">In a switching context, I think there is a stronger case for distinguishing between +0.0 and -0.0. The operational semantics I'd recommend are to desugar, say a float switch, to an int switch on the Float.<span class="element-name">floatToIntBits
mapping of the float case labels. </span><span class="element-name">Float.<span class="element-name">floatToIntBits, as opposed to
</span></span><span class="element-name"><span class="element-name"><span class="element-name">Float.<span class="element-name">floatToRawIntBits, normalized all NaN representations to a single value.</span></span></span></span></p>
<p class="">-Joe<br class="">
</p>
</div>
</div>
</blockquote>
</div>
<br class="">
</div>
</body>
</html>