Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

On Thu, May 27, 2010 at 5:43 PM, David Menendez <dave at zednenem.com> wrote:

> On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
> <carlos.camarao at gmail.com> wrote:
> > Isaac Dupree:
> >> Your proposal appears to allow /incoherent/ instance selection.
> >> This means that an expression can be well-typed in one module, and
> >> well-typed in another module, but have different semantics in the
> >> two modules.  For example (drawing from above discussion) :
> >>
> >> module C where
> >>
> >> class F 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
> >> k :: Bool
> >> k = f o
> >>
> >> module Q where
> >> import C
> >> instance F Int Bool where f = even
> >> instance O Int where o = 0
> >> k :: Bool
> >> k = f o
> >>
> >> module Main where
> >> import P
> >> import Q
> >> -- (here, all four instances are in scope)
> >> main = do { print P.k ; print Q.k }
> >> -- should result, according to your proposal, in
> >> -- False
> >> -- True
> >> -- , am I correct?
> >
> > If qualified importation of k from both P and from Q was specified, we
> > would have two *distinct* terms, P.k and Q.k.
>
> I think Isaac's point is that P.k and Q.k have the same definition (f
> o). If they don't produce the same value, then referential
> transparency is lost.
>
> --
> Dave Menendez <dave at zednenem.com>
> <http://www.eyrie.org/~zednenem/ <http://www.eyrie.org/%7Ezednenem/>>
>

The definitions of P.k and Q.k are textually the same but the contexts are
different. "f" and "o" denote distinct values in P and Q. Thus, P.k and Q.k
don't have the same definition.

Thanks for the clarification. I thought the point was about coherence.

Cheers,

Carlos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20100527/fea4d1f6/attachment.html