[Haskell-cafe] Ambiguous reified dictionaries

[Simon Peyton-Jones]

Yes, Haskell says that in any program there should be only one instance for any particular type (here Monoid Int).  GHC doesn't check that, but it should really do so.  It's not necessary for soundness (ie no runtime crash) but it is necessary for coherence (ie when you run the program the answer you get doesn't depend on which dictionary the typechecker arbitrarily chose).

[When type functions are involved, having a unique instance is necessary for soundness as well as coherence.]

This isn't the only place there may be a choice of dictionaries.  Consider

        class Eq a => C a where ...
        class Eq a => D a where ...

        f :: (C a, D a) => a -> ...
        f x = ....(x==x)....

Here the type checker can get the Eq dictionary it needs for (x==x) from either the (C a) dictionary or the (D a) dictionary.


| > 3) Is it possible to implement the following function?
| >
| >> mkMonoidInst :: a -> (a -> a -> a) -> MonoidInst a
| >> mkMonoidInst mempty mappend = ...

No it's not possible.  And now you know why!

Simon


| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On
| Behalf Of Lennart Augustsson
| Sent: 09 April 2009 09:54
| To: Martijn van Steenbergen
| Cc: Haskell Cafe
| Subject: Re: [Haskell-cafe] Ambiguous reified dictionaries
|
| That program is incorrect, it contains two instances for Monoid Int,
| and the compiler should flag it as illegal.
|
|    -- Lennart
|
| On Thu, Apr 9, 2009 at 10:35 AM, Martijn van Steenbergen
| <martijn at van.steenbergen.nl> wrote:
| > Good morning,
| >
| > The [1]GHC user's guide, section 8.4.5 says:
| >
| > "The new feature is that pattern-matching on MkSet (as in the definition of
| > insert) makes available an (Eq a) context. In implementation terms, the
| > MkSet constructor has a hidden field that stores the (Eq a) dictionary that
| > is passed to MkSet; so when pattern-matching that dictionary becomes
| > available for the right-hand side of the match."
| >
| > But what happens if there are several dictionaries available?
| >
| > Consider these three modules:
| >
| > ReifyMonoid.hs:
| >
| >> {-# LANGUAGE GADTs #-}
| >>
| >> module ReifyMonoid where
| >>
| >> import Data.Monoid
| >>
| >> data MonoidInst a where
| >>  MkMonoidInst :: Monoid a => MonoidInst a
| >
| > ReifySum.hs:
| >
| >> module ReifySum where
| >>
| >> import ReifyMonoid
| >> import Data.Monoid
| >>
| >> instance Monoid Int where
| >>  mempty = 0
| >>  mappend = (+)
| >>
| >> intSum :: MonoidInst Int
| >> intSum = MkMonoidInst
| >
| > ReifyProd.hs:
| >
| >> module ReifyProd where
| >>
| >> import ReifyMonoid
| >> import Data.Monoid
| >>
| >> instance Monoid Int where
| >>  mempty = 1
| >>  mappend = (*)
| >>
| >> intProd :: MonoidInst Int
| >> intProd = MkMonoidInst
| >
| > Now a function
| >
| >> emp :: MonoidInst a -> a
| >> emp MkMonoidInst = mempty
| >
| > works as you'd expect:
| >
| > *ReifySum ReifyProd> emp intSum
| > 0
| > *ReifySum ReifyProd> emp intProd
| > 1
| >
| > But what about this function?
| >
| >> empAmb :: MonoidInst a -> MonoidInst a -> a
| >> empAmb MkMonoidInst MkMonoidInst = mempty
| >
| > Now there are two dictionaries available. GHC consistently picks the one
| > from the second argument:
| >
| > *ReifySum ReifyProd> empAmb intProd intSum
| > 1
| > *ReifySum ReifyProd> empAmb intSum intProd
| > 0
| >
| > My questions are:
| >
| > 1) Shouldn't GHC reject this as being ambiguous?
| > 2) Should class constraints only be available on existentially qualified
| > type variables to prevent this from happening at all?
| > 3) Is it possible to implement the following function?
| >
| >> mkMonoidInst :: a -> (a -> a -> a) -> MonoidInst a
| >> mkMonoidInst mempty mappend = ...
| >
| > Thank you,
| >
| > Martijn.
| >
| >
| >
| > [1]
| > http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-
| extensions.html#gadt-style
| > _______________________________________________
| > Haskell-Cafe mailing list
| > Haskell-Cafe at haskell.org
| > http://www.haskell.org/mailman/listinfo/haskell-cafe
| >
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe