[Haskell] Haskell's type inference considered harmful [Re: A riddle...]

[Andreas Abel]

Congratulations to all that solved the riddle so quickly.  (First answer 
in only 8 Minutes!)  Now to the point of the exercise:  Shocking 
realizations.

   1. Haskell's type inference is NON-COMPOSITIONAL!

In the riddle below, I am defining two things f ("rgbliste") and g 
("farbliste").  Even though they are not strongly connected, but g comes 
after f in the definition order, the code of g influences the type of f. 
  THAT'S WRONG! :-(

It gets worse:

   2. DEAD CODE changes a program's result!

Yes indeed.  Dead code ("farbliste") in the source cannot be removed 
safely.  And:

   3. Haskell "casts" 181935629 to Word16 value 7693 WITHOUT WARNING!

Needless to say, these are serious problems for leading-edge strongly 
typed language.  The experts are probably aware of this.  But I awoke 
harshly from a sweet dream.

Issue 3 is quite harmful and reminds me more of C than of a strongly 
typed language.  Fixing this is not trivial.  The problem is that all 
numeric constants have type Num a => a, and of course, type variable a 
can be instantiated to Int Word16 or whatever.  Numeric constants need 
to inhabit subclasses of Num, e.g., Word16, Int and Integer /classes/ to 
make this behavior go away.

Issues 1/2 go away with

   {-# LANGUAGE NoMonomorphismRestriction #-}

(thx to Christian who pointed me to this).  I wonder why this is not on 
by default?!  There seems to be an unresolved dispute about this... 
http://hackage.haskell.org/trac/haskell-prime/wiki/NoMonomorphismRestriction

But even with MonomorphismRestriction, issue 1/2 are avoidable with a 
more refined approach to type meta variables in the Haskell type 
inference:  After type-checking a strongly connected component, type 
meta variables created for this part of the Haskell program should not 
be instantiated in the (topologically) later defined parts of the 
program.  YOU DON'T WANT THE USE OF A FUNCTION INFLUENCE ITS DEFINITION! 
  There are two alternatives what to do with remaining meta-variables of 
a SCC:

   1. With monomorphism restriction: instantiate to the "best type".
      In our example below, Haskell chooses Integer.

   2. Without monomorphism restriction: generalize.

Choice 1 will give an error in the program below, but i rather have an 
error than a silent change of behavior of my program!

Cheers,
Andreas

P.S.: In Agda, in the situation of unsolved metas in an "SCC" (a mutual 
block), these metas are just frozen, triggering typing errors later 
(since Agda cannot generalize).  The user has to go back an insert more 
type annotations.  But this is safe, whereas silent late instantiation 
breaks compositionality.



On 16.07.2012 17:25, Andreas Abel wrote:
> Today a student came to me with a piece of code that worked it executed
> by itself, but produced different result in the context of his larger
> problem.  We cut down the example to the following:
>
>> import Graphics.UI.Gtk
>>
>> -- should produce [(26471,0,65535),...
>> rgbliste =
>>  (map (\ i ->
>>   let rb = 5 * (mod (mod 181935629 (4534+i)) 100)-250+128 in
>>   let gb = 5 * (mod (mod 128872693 (5148+i)) 100)-250+128 in
>>   let bb = 5 * (mod (mod 140302469 (7578+i)) 100)-250+128 in
>>   let r = min 255 $ max 0 rb in
>>   let g = min 255 $ max 0 gb in
>>   let b = min 255 $ max 0 bb in
>>   (r*257,g*257,b*257)) [0..])
>>
>> --farbliste = map (\ (r,g,b) -> Color r g b) rgbliste
>>
>> main :: IO ()
>> main = do
>>   print $ head rgbliste
>
> If you run it, it prints (26471,0,65535).
> If you uncomment the def. of farbliste, it prints (44461,65535,65535).
>
> I was surprised.  What is going on?
>
> Cheers,
> Andreas
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/