Latest Post

Abs Puzzle

[This blog was moved here]

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:

1: let abs x = if x < 0 then -x else x

The obvious question – do the answers match your expectations? That depends…

absx

It’s quite obvious when you think about the corner cases – here it’s the minimal integer value:

-(-2147483648) = -2147483648

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):

1: module Nums
2: 
3: type nat = x:int{x >= 0}
4: 
5: let good_x: nat = 42
6: let bad_x: nat = -42
input(6,17-6,20) : Error : Expected an expression of type: x_3:int{GTE x_3 0} but got
(op_Minus(42)): x_357_1:int{Eq2 int int x_357_1 (Minus (42))} Type checking failed: Nums

Now it’s turn for our abs function:

1: val abs: int -> nat
2: let abs x = if x < 0 then -x
3: 
4: let _ = abs 2147483647  
5: let _ = abs (-2147483647) 
6: 
7: // both following statements give Syntax error:
8: let _ = abs 2147483648
9: let _ = abs (-2147483648)

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:

1: let _ = abs (2147483647 + 1)
2: // And the result is...
Verified module: Nums

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:

1: val check: x:nat -> y:int{y > x}
2: let check x = x + 1 
3: 
4: let _ = check (2147483647 + 1)
Error : Let-bound variable op_Addition(2147483647, 1) escapes its scope in type
x_8_1:int{GT x_8_1 x_11_3}; insert an explicit type annotation. (expected type none)
Type checking failed: Nums
1: val check: x:nat -> y:int{y = (x+1)} 
Error : Let-bound variable op_Addition(2147483647, 1) escapes its scope in type
x_6_1:int{Eq2 int int x_6_1 (Add (x_9_5) (1))}; insert an explicit type annotation.
(expected type none) Type checking failed: Nums
1: val check: x:nat -> y:int{y > 0} 
Verified module: Nums
1: val check: x:nat -> y:int{y < 0 \/ y > x}
Error : Let-bound variable op_Addition(2147483647, 1) escapes its scope in type
x_8_1:int{((LT x_8_1 0) || (GT x_8_1 x_11_3))}; insert an explicit type annotation.
(expected type none) Type checking failed: Nums

All the cases above succeeded for the max value:

let _ = check 2147483647

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

1: let _ = abs 2147483648 
Error : Expected an expression of type: int but got (2147483648.000000): float
Type checking failed: Nums
1: let _ = abs (-2147483648) 
 starting backend
 starting derefinement
 starting expanding types
 finished with expanding types
Verified module: Nums

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):

1: using System;
2: using System.Diagnostics.Contracts;
3: 
4: public class Program {
5:   public static void Puzzle(int x) {
6:     var y = x < 0 ? -x : x;
7:     Contract.Assert(y >= 0);
8:   }
9: }
x            | Output/Exception  | Error Message
-----------------------------------------------------------
0            |                   |
int.MinValue | ContractException | Assertion failed: y >= 0