Quantcast

Re: Haskell's type inference considered harmful

classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Haskell's type inference considered harmful

oleg-30

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

Yes, it is -- and there are many examples of it. Here is an example
which has nothing to do with MonomorphismRestriction or numeric
literals

{-# LANGUAGE ExtendedDefaultRules #-}

class C a where
    m :: a -> Int

instance C () where
    m _ = 1

instance C Bool where
    m _ = 2

main = do
       x <- return undefined
       let y = x
       print . fst $ (m x, show x)
       -- let dead = if False then not y else True
       return ()

The program prints 1. If you uncomment the (really) dead code, it will
print 2. Why? The dead code doesn't even mention x, and it appears
after the printing! What is the role of show x, which doesn't do anything?

Exercises: what is the significance of the monadic bind to x? Why
can't we replace it with "let x = undefined"?

[Significant hint, don't look at it]

Such a behavior always occurs when we have HM polymorphism restriction
and some sort of non-parametricity -- coupled with default rules or
overlapping instances or some other ways of resolving overloading. All
these features are essential (type-classes are significant,
defaulting is part of the standard and is being used more and more).


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Haskell's type inference considered harmful

Miguel Mitrofanov
Actually, both examples show that the problem isn't type inference, it's defaulting mechanism.

Отправлено с iPhone

Jul 17, 2012, в 12:46, [hidden email] написал(а):

>
>>   1. Haskell's type inference is NON-COMPOSITIONAL!
>
> Yes, it is -- and there are many examples of it. Here is an example
> which has nothing to do with MonomorphismRestriction or numeric
> literals
>
> {-# LANGUAGE ExtendedDefaultRules #-}
>
> class C a where
>    m :: a -> Int
>
> instance C () where
>    m _ = 1
>
> instance C Bool where
>    m _ = 2
>
> main = do
>       x <- return undefined
>       let y = x
>       print . fst $ (m x, show x)
>       -- let dead = if False then not y else True
>       return ()
>
> The program prints 1. If you uncomment the (really) dead code, it will
> print 2. Why? The dead code doesn't even mention x, and it appears
> after the printing! What is the role of show x, which doesn't do anything?
>
> Exercises: what is the significance of the monadic bind to x? Why
> can't we replace it with "let x = undefined"?
>
> [Significant hint, don't look at it]
>
> Such a behavior always occurs when we have HM polymorphism restriction
> and some sort of non-parametricity -- coupled with default rules or
> overlapping instances or some other ways of resolving overloading. All
> these features are essential (type-classes are significant,
> defaulting is part of the standard and is being used more and more).
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Haskell's type inference considered harmful

Andreas Abel
In reply to this post by oleg-30
Haha, I like this example.

However, if your are using ExtendedDefaultRules then you are likely to
know you are leaving the clean sound world of type inference.  The
example of my student works on plain GHC...

The other responses to my message confined to point me to "best
practices" to avoid the design bugs of Haskell's type inference.
However, if I want "best practices", I can go to JavaScript.

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

I am already biased towards Haskell.  But as an unbiased decision maker,
I would not consider a language with "undead code" for my projects...

Cheers,
Andreas


On 17.07.12 10:46 AM, [hidden email] wrote:

>>     1. Haskell's type inference is NON-COMPOSITIONAL!
>
> Yes, it is -- and there are many examples of it. Here is an example
> which has nothing to do with MonomorphismRestriction or numeric
> literals
>
> {-# LANGUAGE  #-}
>
> class C a where
>      m :: a -> Int
>
> instance C () where
>      m _ = 1
>
> instance C Bool where
>      m _ = 2
>
> main = do
>         x <- return undefined
>         let y = x
>         print . fst $ (m x, show x)
>         -- let dead = if False then not y else True
>         return ()
>
> The program prints 1. If you uncomment the (really) dead code, it will
> print 2. Why? The dead code doesn't even mention x, and it appears
> after the printing! What is the role of show x, which doesn't do anything?
>
> Exercises: what is the significance of the monadic bind to x? Why
> can't we replace it with "let x = undefined"?
>
> [Significant hint, don't look at it]
>
> Such a behavior always occurs when we have HM polymorphism restriction
> and some sort of non-parametricity -- coupled with default rules or
> overlapping instances or some other ways of resolving overloading. All
> these features are essential (type-classes are significant,
> defaulting is part of the standard and is being used more and more).
>
>

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

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

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Haskell's type inference considered harmful

oleg-30

> 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?


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Haskell's type inference considered harmful

Andreas Abel
Thanks for your answer and your examples.  It would be worthwile
collecting such examples in a small article.

I think some of the problems with type inference come from insufficient
theory about metavariables.  When I started studying higher-order
unification I always wondered what the scope of a metavariable is.  It
is created at some point and then just sits there waiting to be solved
by a constraint.  However, it is not clear where these constraints may
come from and at what time a metavariable should be declared unsolved or
be generalized over.

In the HM toy calculus (lambda + let), it is spelled out:
generalization must happen after a let, such that the solution for a
metavariable is determined solely by constraints in the *definition* of
a symbol, not in its *use*.

I'd be grateful for pointers to work that considers metavariable scope
in some bigger, more realistic calculi.  In Haskell, one thing that goes
wrong is that all definitions in a module are considered mutually
recursive by the type inference algorithm.  But in fact, the definitions
can be stratified by a strongly connected components analysis.  Doing
such an analysis, and limiting metavariable scope to an SCC, would
overcome the problem I outlined in my original mail and would result in
a more principled treatment of metavariables.

That concerned type inference for global definitions.  It is not clear
we want the same for local definitions.  There, it makes more sense to
assume that the programmer can overlook what he is doing, and thus one
could allow flow of information from the use of a symbol to its
definition.

Do we want information flow from dead code to live code? I'd say no.
"Dead" is unfortunately undecidable; but at least one can identify
unused local definitions, i.e., statically unreachable definitions.
Your examples seem to suggest you want such information flow, or maybe not?


On 21.07.2012 12:26, [hidden email] wrote:

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

Ah, I have never been in Japan at that time.

> 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.

Yes, that's a known problem.

> 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?

Yes, they were.  But for discussion about metavariables maybe something
like a haskell implementor's forum would be more appropriate.  Yet I am
only an Agda implementor.

Cheers,
Andreas


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

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

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Loading...