[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

>>    The situation is as if we [had] a FD:
> Well, that is indeed equivalent here in the second argument of class
> F, but I constructed the example to show an issue in the class's
> *first* argument.

The example should be equivalent in all respects (at least that was my
motivation when I wrote it).

> Notice you needed to add type-signatures, on the functions you named
> "g" -- in particular their first arguments -- to make the example
> work with only FDs?

I wrote g, with type signatures, just to avoid writing the type
signatures (f:: Bool->Bool and f::Int->Bool) inside (f o). I wanted to
use, textually, the same expression.

> These are two different expressions that are being printed, because
> " :: Bool -> Bool" is different from " :: Int -> Bool".  In my
> example of using your proposal, one cannot inline in the same way,

I wrote the example just to show that one can obtain the same effect with
FDs:
one not "inline", i.e. use "g o", in the same way.

> If your proposal was able to require those -- and only those -- bits
> of type signatures that were essential to resolve the above
> ambiguity; for example, the ( :: Int) below,
> module Q where
>  import C
>  instance F Int Bool where f = even
>  instance O Int where o = 0
>  k = f (o :: Int)
>, then I would be fine with your proposal (but then I suspect it
> would have to be equivalent to FDs -- or in other words, that it's not
> really practical to change your proposal to have that effect).
> I stand by my assertion that "the same expression means different
> things in two different modules" is undesirable, (and that I suspect
> but am unsure that this undesirability is named "incoherent
> instances").

"k::Bool; k=f o" in Q has exactly the same effect as "k=f(o::Int)",
under our proposal.

"(f o)::Bool" in P and in Q are not "the same expression", they are
distinct expressions, because they occur in distinct contexts which
make "f" and "o" in (f o)::Bool denote distinct values, just as "(g
o)::Bool" are
distinct expressions in P and Q in the example with a FD (because
"g" and "o" in (g o)::Bool denote distinct values in P and in Q).

Cheers,

Carlos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100530/28c5af96/attachment.html