Abs Puzzle
Contents
If someone asked you to implement abs function (say, for ints), how would you do that? A simple experiment shows that almost everyone comes up with something like that, whether it’s F#, C#, Scala or anything else:


The obvious question  do the answers match your expectations? That depends…
It’s quite obvious when you think about the corner cases  here it’s the minimal integer value:


So, in Java/Scala the absolute value can be negative:
Note that if the argument is equal to the value of Integer.MIN_VALUE, the most negative representable int value, the result is that same value, which is negative.
In .NET you’ll get an exception  personally, I think that’s a better behaviour for this function:
OverflowException  value equals Int32.MinValue
When I started to think about different examples for our future meetup (collecting all kinds of crashes on the way  from ‘CLR detected an invalid program’ to ‘unexpected exception’), I couldn’t resist but look at what happens when you move some checks to the type level.
Let’s define a refinement type for the natural numbers in F* and make sure it works (you can try the examples in your browser):


Now it’s turn for our abs
function:


The first error is kind of expected, because the literal 2147483648
is too large for int
. However, I’d think the second one should be ok, and after a quick look at the F* lexer not sure why they both fail ("Allow <max_int+1> to parse as min_int"
). Anyway, there’s another interesting case:


A bit strange, isn’t it? If you ask Scala or F# what 2147483647 + 1
is, you get 2147483648
, that means abs (2147483647 + 1)
can’t be of nat
type! Here’s a bunch of checks for ‘+1’ with different refinements:








All the cases above succeeded for the max value:


I also tried these examples on my oldslightlyworking F* 0.7 alpha Mono build, where the results seem to be more reasonable:




Maybe one day I’ll finally setup a VM with Windows to take a look at IL, but for now the conclusion is to always be on the lookout.
P.S. Pex can find the failing case (for some reason, at least in online version this example works only with C# and VB):


Author Natallie
LastMod 20140425