Well that's interesting... I looked at the link you posted and noticed the other floating point types. I tried "double" and "long double" in the Arduino sketch - all of them returned "8 and 8". But in GCC and Linux, the type "double" gives me 16 and 16, and "long double" gives me 20 and 20.
I suppose this means there is no difference (for Arduino) between "float" and "double"... yes?