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

[Isaac Dupree]

On 05/29/10 21:24, Carlos Camarao wrote:
> The situation is as if we 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.

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?

> module C where
>    class F a b | a->b where f :: a ->   b
>    class O a where o :: a
>
> module P where
>    import C; instance F Bool Bool where f = not
>    instance O Bool where o = True
>    g:: Bool ->  Bool
>    g = f
>    k::Bool
>    k = g o
>
> module Q where
>    import C
>    instance F Int Bool where f = even
>    instance O Int where o = 0
>    g::Int->Bool
>    g = f
>    k :: Bool
>    k = g o

you can inline these "k"-definitions into module Main and it will work 
(modulo importing C).

module Main where
     import C
     import P
     import Q
     main = do { print (((f :: Bool -> Bool) o) :: Bool);
                 print (((f :: Int -> Bool) o) :: Bool) }

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, if I 
understand correctly (the inlining would cause ambiguity errors -- 
unless of course the above distinct type-signatures are added).

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").
I'm trying to work out whether it's possible to violate the invariants 
of a Map by using your extension (having it select a different instance 
in two different places, given the same type).. I think, no it is not 
possible for Ord or any single-parameter typeclass, though there might 
be some kind of issues with multi-parameter typeclasses, if the library 
relies on a FD-style relationship between two class type-parameters and 
then two someones each add an instance that together violate that 
implied FD-relationship (which is allowed under your scheme, unlike if 
there was an actual FD).  Er, odd, I need to play with some actual FD 
code to think about this, but I'm too sleepy / busy packing for a trip.

Did any of the above make sense to you?  It's fine if some didn't, type 
systems are complicated... and please point out if something I said was 
outright wrong.


-Isaac