Ambiguous reified dictionaries

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

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
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... _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Lennart Augustsson wrote:
That program is incorrect, it contains two instances for Monoid Int, and the compiler should flag it as illegal.
Two simultaneous instances are okay as long as you don't use any of those instances, right? Just like two imported symbols with the same name are okay as long as you don't use them. Martijn.

Martijn van Steenbergen wrote:
Two simultaneous instances are okay as long as you don't use any of those instances, right? Just like two imported symbols with the same name are okay as long as you don't use them.
This makes little sense. Sorry, my bad. I was thinking about instances available in the complete module instead of also those made available by pattern matching on constructors. Martijn.

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@haskell.org [mailto:haskell-cafe-bounces@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
|

On Thu, Apr 9, 2009 at 5:14 AM, Simon Peyton-Jones
| > 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
Simon, While we can't give him exactly what he asked for, we can approximate the construction using Oleg and CC Shan's Implicit Configurations and fulfill the spirit of the request.
{-# LANGUAGE ScopedTypeVariables, TypeOperators, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances, Rank2Types, GeneralizedNewtypeDeriving #-}
Please, pardon the gratuitous use of extensions.
import Data.Bits import Data.Monoid import Data.Reflection -- from package 'reflection'
First define the concept of a dictionary for a monoid.
type M a = (a, a -> a -> a)
Then provide a type level brand that indicates which dictionary you are going to use.
data (a `WithMonoid` s) = Mon { getWithMonoid :: a } deriving (Eq,Ord,Show)
Use reflection to access the dictionary
instance (s `Reflects` M a) => Monoid (a `WithMonoid` s) where mempty = Mon (fst (reflect (undefined :: s))) Mon a `mappend` Mon b = Mon ((snd (reflect (undefined :: s))) a b)
Reify a monoid dictionary for use within a universally quantified world, ala ST.
reifyMonoid :: a -> (a -> a -> a) -> (forall s. (s `Reflects` M a) => s -> w) -> w reifyMonoid = curry reify
Change the type of the above to avoid the spurious argument, and to automatically unwrap the result.
withMonoid :: a -> (a -> a -> a) -> (forall s. (s `Reflects` M a) => w `WithMonoid` s) -> w withMonoid = withMonoid' undefined where withMonoid' :: w -> a -> (a -> a -> a) -> (forall s. (s `Reflects` M a) => w `WithMonoid` s) -> w withMonoid' (_::w) (i::a) f k = reifyMonoid i f (\(_::t) -> getWithMonoid (k :: w `WithMonoid` t))
And now we have some likely candidates to test:
test :: Int test = withMonoid 0 (+) (mconcat [Mon 2,mempty,Mon 0])
test2 :: Int test2 = withMonoid 1 (*) (mconcat [Mon 3,mempty,Mon 2])
test3 :: Integer test3 = withMonoid 0 xor (mconcat [Mon 4,mempty,Mon 4])
*Main> test Loading package reflection-0.1.1 ... linking ... done. 2 *Main> test2 6 *Main> test3 0 There you have it, everything works out. Amusingly, I have a similar set of constructions for reifying other kinds of constructs in my 'monoids' library on Hackage, but I don't currently provide a reified Monoid type, mainly because the signature isn't enough to enforce its associativity. However, I do allow you to reify an arbitrary function into a 'Reducer' using this trick to enable you to uniformly inject values into a particular monoid. -Edward Kmett
| -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto: haskell-cafe-bounces@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 |
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@haskell.org | > http://www.haskell.org/mailman/listinfo/haskell-cafe | > | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Simon Peyton-Jones wrote:
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).
Unless of course, your program implicitly depends on the coherence of dictionary choice for its own soundness, for example, a program using Data.Typeable to implement Dynamic or similar. Jules
participants (5)
-
Edward Kmett
-
Jules Bean
-
Lennart Augustsson
-
Martijn van Steenbergen
-
Simon Peyton-Jones