On Thu, Jul 21, 2011 at 6:46 PM, Simon Peyton-Jones wrote:

You point is that the (C Int) dictionary has (C String) as a superclass, and (C String) has (C Int) as a superclass. So the two instances are mutually recursive, but that’s ok.

That is not unreasonable. But it is dangerous. Consider

         class C [a] => C a

Then any dictionary for (C a) would contain a dictionary for (C [a]) which would contain a dictionary for C [[a]], and so on.  Haskell is lazy so we might even be able to build this infinite dictionary, but it *is* infinite.

It’s a bit like the “recursive instance” stuff introduced in “Scrap your boilerplate with class”.

After 5 mins thought I can’t see a reason why this could not be made to work.  But it’d take work to do.  If you have a compelling application maybe you can open a feature request ticket, describing it, and referring this thread?

Has anyone else come across this?

Yes. I wanted to write typeclasses for data which can be converted between mutable and immutable forms like this: (from memory and simplified a bit, so not entirely correct in other respects) class Immutable (Frozen a) => Mutable a where type Frozen a unsafeFreeze :: a -> Frozen a makeCopy :: a -> IO a class Mutable (Thawed a) => Immutable a where type Thawed a unsafeThaw :: a -> Thawed a As this causes a superclass cycle, I had to go with a MPTC instead. Not any less capable, but not as nice looking. Actually, I had wanted to write: class (Immutable (Frozen a), Thawed (Frozen a) ~ a) => Mutable a where ... and vice versa So I was depending on multiple as-yet unimplemented features. This is different from the original example - I don't know if cyclic equality superclass contexts would be sensible and-or implementible?

Simon

From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Ryan Trinkle Sent: 20 July 2011 17:37 To: glasgow-haskell-users@haskell.org Subject: Superclass Cycle via Associated Type

The following code doesn't compile, but it seems sensible enough to me.  Is this a limitation of GHC or is there something I'm missing?

class C (A x) => C x where

  type A x :: *

instance C Int where

  type A Int = String

instance C String where

  type A String = Int

The error I get is:

SuperclassCycle.hs:1:1:

    Cycle in class declarations (via superclasses):

      SuperclassCycle.hs:(1,1)-(2,15): class C (A x) => C x where {

                                           type family A x :: *; }

Ryan

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-- Work is punishment for failing to procrastinate effectively.

2011/7/22 Simon Peyton-Jones :

I talked to Dimitrios.  Fundamentally we think we should be able to handle recursive superclasses, albeit we have a bit more work to do on the type inference engine first.

The situation we think we can handle ok is stuff like Edward wants (I've removed all the methods):

class LeftModule Whole m => Additive m class Additive m => Abelian m class (Semiring r, Additive m) => LeftModule r m class Multiplicative m where (*) :: m -> m -> m class LeftModule Natural m => Monoidal m class (Abelian m, Multiplicative m, LeftModule m m) => Semiring m class (LeftModule Integer m, Monoidal m) => Group m class Multiplicative m => Unital m class (Monoidal r, Unital r, Semiring r) => Rig class (Rig r, Group r) => Ring r

The superclasses are recursive but  a) They constrain only type variables  b) The variables in the superclass context are all         mentioned in the head.  In class Q => C a b c         fv(Q) is subset of {a,b,c}

Question to all: is that enough?

======= The main difficulty with going further ==============

Here's an extreme case   class A [a] => A a where      op :: a -> Int

  f :: A a => a -> Int   f x = [[[[[x]]]]] + 1

The RHS of f needs A [[[[[a]]]]] The type sig provides (A a), and hence (A [a]), and hence (A [[a]]) and so on.

BUT it's hard for the solver to spot all the now-infinite number of things that are provided by the type signature.

Gabor's example is less drastic   class Immutable (Frozen a) => Mutable a where      type Frozen a   class Mutable (Thawed a) => Immutable a where      type Thawed a

but not much less drastic.  (Mutable a) in a signature has a potentially infinite number of superclasses        Immutable (Frozen a)        Mutable (Thawed (Frozen a))        ...etc...

It's not obvious how to deal with this.

However Gabor's example can perhaps be rendered with a MPTC:

 class (Frozen t ~ f, Thawed f ~ t) => Mutable f t where   type Frozen a   type Thawed a   unsafeFreeze :: t -> Frozen t   unsafeThaw :: f -> Thawed f

And you can do *that* today.

Yeah, this is pretty much what I ended up doing. As I said, I don't think I lose anything in expressiveness by going the MPTC route, I just think the two separate but linked classes way reads better. So it's just a "would be nice" thing. Do recursive equality superclasses make sense / would they be within the realm of the possible to implement?

Simon

-- Work is punishment for failing to procrastinate effectively.

My situation is fairly similar to Gabor's, and, like him, I was able to make do with an equality superclass. However, instead of combining two classes, I found that I needed to add a third. My concept here is to create two monads which share much of their functionality, but not all of it. Specifically, one of them is "high" and one is "low". Values of type "Low" encapsulate computations in the low monad, and values of type "High" encapsulate values in the high monad. Both low and high monads can *create* Low and High values and *execute* Low values, but only the high monad can *execute* High values. So, what I'd like to write is: data High a data Low a class (Monad m, MonadLow (LowM m), MonadHigh (HighM m)) => MonadLow m where execLow :: Low a -> m a type LowM m :: * -> * mkLow :: LowM m a -> m (Low a) type HighM m :: * -> * mkHigh :: HighM m a -> m (High a) class MonadLow m => MonadHigh m where execHigh :: High a -> m a data L a data H a instance Monad L instance MonadLow L where type LowM L = L type HighM L = H instance Monad H instance MonadLow H where type LowM H = L type HighM H = H instance MonadHigh H Of course, this has a superclass cycle. Instead, I can write: ... class Monad m => MonadLow m where ... class (MonadHigh m, MonadLow (LowM m), HighM m ~ m, HighM (LowM m) ~ m, LowM (LowM m) ~ LowM m) => MonadHigh' m where {} Then I can use MonadHigh' wherever I might have instead used MonadHigh, and achieve roughly the result I was looking for. However, it doesn't seem like a very clean definition to me. That being said, I haven't found any problem with using the MonadHigh' approach, although I've just recently started investigating it. Ryan 2011/7/22 Dan Doel

2011/7/22 Gábor Lehel :

...

Yeah, this is pretty much what I ended up doing. As I said, I don't think I lose anything in expressiveness by going the MPTC route, I just think the two separate but linked classes way reads better. So it's just a "would be nice" thing. Do recursive equality superclasses make sense / would they be within the realm of the possible to implement?

Those equality superclasses are not recursive in the same way, as far as I can tell. The specifications for classes require that there is no chain:

C ... => D ... => E ... => ... => C ...

However, your example just had (~) as a context for C, but C is not required by (~). And the families involved make no reference to C, either. A fully desugared version looks like:

type family Frozen a :: * type family Thawed a :: *

class (..., Thawed (Frozen t) ~ t) => Mutable t where ...

I think this will be handled if you use a version where equality superclasses are allowed.

-- Dan

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

2011/7/23 Gábor Lehel

2011/7/22 Dan Doel :

...

2011/7/22 Gábor Lehel :

...

Yeah, this is pretty much what I ended up doing. As I said, I don't think I lose anything in expressiveness by going the MPTC route, I just think the two separate but linked classes way reads better. So it's just a "would be nice" thing. Do recursive equality superclasses make sense / would they be within the realm of the possible to implement?

Those equality superclasses are not recursive in the same way, as far as I can tell. The specifications for classes require that there is no chain:

C ... => D ... => E ... => ... => C ...

However, your example just had (~) as a context for C, but C is not required by (~). And the families involved make no reference to C, either. A fully desugared version looks like:

type family Frozen a :: * type family Thawed a :: *

class (..., Thawed (Frozen t) ~ t) => Mutable t where ...

I think this will be handled if you use a version where equality superclasses are allowed.

To be completely explicit, I had:

class (Immutable (Frozen t), Thawed (Frozen t) ~ t) => Mutable t where type Frozen t ... class (Mutable (Thawed t), Frozen (Thawed t) ~ t) => Immutable t where type Thawed t ...

I had a similar issue in my representable-tries package. In there I had type family Key (f :: * -> *) :: * class Indexable f where index :: f a -> Key f -> a class Indexable f => Representable f where tabulate :: (Key f -> a) -> f a such that tabulate and index witness the isomorphism from f a to (Key f -> a). So far no problem. But then to provide a Trie type that was transparent I wanted. class (Representable (BaseTrie e), Traversable (BaseTrie e), Key (BaseTrie e) ~ e) => HasTrie e where type BaseTrie e :: * -> * type (:->:) e = BaseTrie e which I couldn't use prior to the new class constraints patch. The reason I mention this is that my work around was to weaken matters a bit class (Representable (BaseTrie e)) => HasTrie e where type BaseTrie e :: * -> * embedKey :: e -> Key (BaseTrie e) projectKey :: Key (BaseTrie e) -> e This dodged the need for superclass equality constraints by just requiring me to supply the two witnesses to the isomorphism between e and Key (BaseTrie e). Moreover, in my case it helped me produce instances, because the actual signatures involved about 20 more superclasses, and this way I could make new HasTrie instances for newtype wrappers just by defining an embedding and projection pair for some type I'd already defined. But, it did require me to pay for a newtype wrapper which managed the embedding and projection pairs. newtype e :->: a = Trie (BaseTrie e a) In your setting, perhaps something like: type family Frozen t type family Thawed t class Immutable (Frozen t) => Mutable t where thawedFrozen :: t -> Thawed (Frozen t) unthawedFrozen :: Thawed (Frozen t) -> t class Mutable (Thawed t) => Immutable t where frozenThawed :: t -> Frozen (Thawed t) unfrozenThawed :: Frozen (Thawed t) -> t would enable you to explicitly program with the two isomorphisms, while avoiding superclass constraints. -Edward

2011/7/25 Gábor Lehel

...

type family Frozen t type family Thawed t class Immutable (Frozen t) => Mutable t where thawedFrozen :: t -> Thawed (Frozen t) unthawedFrozen :: Thawed (Frozen t) -> t

class Mutable (Thawed t) => Immutable t where frozenThawed :: t -> Frozen (Thawed t) unfrozenThawed :: Frozen (Thawed t) -> t

would enable you to explicitly program with the two isomorphisms, while avoiding superclass constraints.

Hmm, that's an interesting thought. If I'm guesstimating correctly, defining instances would be more cumbersome than with the MPTC method, but using them would be nicer, provided I write helper functions to hide the use of the isomorphism witnesses. I'll give it a try. Thanks!

I seem to recall that in one of your packages, you had a typeclass method returning a GADT wrapping the evidence for the equality of two types, as a workaround for the lack of superclass equality constraints -- what makes you prefer that workaround in one case and this one in another?

In a very early version of representable-tries I used my eq package to provide equality witnesses: http://hackage.haskell.org/packages/archive/eq/0.3.3/doc/html/Data-Eq-Type.h... But I've turned in general to using explicit isomorphisms for things like http://hackage.haskell.org/packages/archive/representable-tries/2.0/doc/html... because they let me define additional instances that are isomorphic to old instances quickly, while an actual equality witness would require me to bang out a new representation and all 20+ superclass instances. This enables me to write instances for thin newtype wrappers like those in Data.Monoid, etc. that I would be forced to just skip in a heavier encoding. -Edward

2011/7/22 Simon Peyton-Jones

I talked to Dimitrios. Fundamentally we think we should be able to handle recursive superclasses, albeit we have a bit more work to do on the type inference engine first.

The situation we think we can handle ok is stuff like Edward wants (I've removed all the methods):

class LeftModule Whole m => Additive m class Additive m => Abelian m class (Semiring r, Additive m) => LeftModule r m class Multiplicative m where (*) :: m -> m -> m class LeftModule Natural m => Monoidal m class (Abelian m, Multiplicative m, LeftModule m m) => Semiring m class (LeftModule Integer m, Monoidal m) => Group m class Multiplicative m => Unital m class (Monoidal r, Unital r, Semiring r) => Rig class (Rig r, Group r) => Ring r

The superclasses are recursive but a) They constrain only type variables b) The variables in the superclass context are all mentioned in the head. In class Q => C a b c fv(Q) is subset of {a,b,c}

Question to all: is that enough?

This would perfectly address all of the needs that I have had! -Edward

On Mon, Jul 25, 2011 at 4:46 AM, Simon Peyton-Jones wrote:

On further reflection I have a question.****

** **

Under the limited design below, which Edward says will do all he wants:*** *

**· **The mutually recursive classes (call them A, B, C) must be defined all together. Like class B a => A a; class C a => B a; class A a => C a****

**· **If a type T is an instance of any of those classes, it must be a member of all of them****

**· **If a function f has type f :: A a => blah, then the signature f :: B a => blah and f :: C a => blah would work equally well

In short, I see no advantage to making A,B,C separate classes compared to simply unioning them into a single class.

**

Bottom line: adding recursive superclasses with the restrictions I describe below would add no useful expressive power. But it would cost effort to implement. So why do it?****

** **

Maybe I’m missing something.

In the univariate case this is true, but I think we've lost sight of the original motivation. In the MPTC case there is a real difference. In my example (with methods), If you have an associative (+), then you can use (.*) to multiply by a whole number, I currently do fold a method into the Additive class to 'fake' a LeftModule, but you have to explicitly use it. class Additive m => LeftModule r m class LeftModule Whole m => Additive m This says that if you have an Additive semigroup, then there exists a LeftModule over the whole numbers, and that every leftmodule is additive, but there can exist other LeftModules than just ones over the whole numbers! Given LeftModule Integer m, you'd know you have Additive m and LeftModule Whole m. LeftModule Integer m => LeftModule Whole m <=> Additive m. Balling them up together precludes the ability to use LeftModule to describe the relationship of whole numbers to a semigroup. But moreover it causes me to have to write code that would be parameterized by the LeftModule in question 5 times, because I have to special case the module structures over wholes, naturals, integers and the ring itself relative to code for any other module. There is a gain in expressive power, but you need multiple parameters to exploit it. -Edward

On Mon, Jul 25, 2011 at 1:40 PM, Jacques Carette wrote:

** On 25/07/2011 9:55 AM, Edward Kmett wrote:

If you have an associative (+), then you can use (.*) to multiply by a whole number, I currently do fold a method into the Additive class to 'fake' a LeftModule, but you have to explicitly use it.

class Additive m => LeftModule r m class LeftModule Whole m => Additive m

This says that if you have an Additive semigroup, then there exists a LeftModule over the whole numbers, and that every leftmodule is additive, but there can exist other LeftModules than just ones over the whole numbers!

Given LeftModule Integer m, you'd know you have Additive m and LeftModule Whole m.

LeftModule Integer m => LeftModule Whole m <=> Additive m.

I believe that part of the issue here is that you are using a single relation (given by class-level => ) to model what are actually two different relations: a 'constructive' inclusion and a 'view' (to use the terminology from the Specifications community, which is clearly what these class definitions are).

Just like inheritance hierarchies fail miserably when you try to model more than one single relation, it should not be unsurprising that the same thing befalls '=>', which is indeed a (multi-ary) relation.

In my own hierarchy for Algebra, I use two relations. Slightly over-simplifying things, one of them reflects 'syntactic' inclusion while the other models 'semantic' inclusion. There are very strict rules for the 'syntactic' one, so that I get a nice hierarchy and lots of free theorems, while the semantic one is much freer, but generates proof obligations which must be discharged. The syntactic one generates a nice DAG (with lots of harmless diamonds), while the semantic one is a fully general graph.

Here is another way to look at it: when you say

class LeftModule Whole m => Additive m you are closer to specifying an *instance* relation than a *class constraint* relation.

This is very true. However, as mentioned at the outset specifying such instance requires newtype noise (on m, to avoid incoherent overlap with the other instances) that leads to a particularly hideous programming style. newtype NaturalModule m = NaturalModule { runNaturalModule :: m } instance Monoidal m => LeftModule Natural (NaturalModule m) where It isn't so bad when working with simple examples like fiveTimes m = runNaturalModule (5 .* NaturalModule m) but it gets progressively worse as the hierarchy gets deeper, and I have to deal with putting on and taking off more and more of these silly wrappers. Placing the superclass constraint enforces that such instances will always be available to me, and admits optimized implementations, which I currently have to shoehorn into the main class and expose by convention. -Edward