[Haskell-cafe] Haskell's type inference considered harmful

[oleg at okmij.org]

> However, if your are using ExtendedDefaultRules then you are likely to 
> know you are leaving the clean sound world of type inference.

First of all, ExtendedDefaultRules is enabled by default in
GHCi. Second, my example will work without ExtendedDefaultRules, in
pure Haskell98. It is even shorter:

instance Num Char
main = do
         x <- return []
         let y = x
         print . fst $ (x, abs $ head x)
         -- let dead = if False then y == "" else True
         return ()
The printed result is either [] or "".

Mainly, if the point is to demonstrate the non-compositionality of type
inference and the effect of the dead code, one can give many many
examples, in Haskell98 or even in SML.

Here is a short one (which does not relies on defaulting. It uses
ExistentialQuantification, which I think is in the new standard or is
about to be.).

{-# LANGUAGE ExistentialQuantification #-}

data Foo = forall a. Show a => Foo [a]
main = do
         x <- return []
	 let z = Foo x
         let dead = if False then x == "" else True
	 return ()

The code type checks. If you _remove_ the dead code, it won't. As you
can see, the dead can have profound, and beneficial influence on
alive, constraining them. (I guess this example is well-timed for Obon).


For another example, take type classes. Haskell98 prohibits overlapping of
instances. Checking for overlapping requires the global analysis of the
whole program and is clearly non-compositional. Whether you may define
	instance Num (Int,Int)
depends on whether somebody else, in a library you use indirectly,
has already introduced that instance. Perhaps that library is imported
for a function that has nothing to do with treating a pair of Ints as
a Num -- that is, the instance is a dead code for your
program. Nevertheless, instances are always imported, implicitly.

The non-compositionality of type inference occurs even in SML (or
other language with value restriction). For example,

   let x = ref [];;

   (* let z = if false then x := [1] else ();; *)

   x := [true];;

This code type checks. If we uncomment the dead definition, it
won't. So, the type of x cannot be fully determined from its
definition; we need to know the context of its use -- which is
precisely what seems to upset you about Haskell.

> To stirr action, mails on haskell-cafe seem useless.

What made you think that? Your questions weren't well answered? What
other venue would you propose?