Re: Superclass Cycle via Associated Type
I just thought of an additional consideration regarding this part of the
design space.
On 25/07/2011 2:02 PM, Edward Kmett wrote:
(I had said):
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.
My understanding is that in Coq, using either Canonical Structures (as
George Gonthier does it) or Matthieu Sozeau's implementation of type
classes, one still defines the infrastructure as you have it, i.e. the
equivalent of
newtype NaturalModule m = NaturalModule { runNaturalModule :: m }
instance Monoidal m = LeftModule Natural (NaturalModule m) where
but then the inference mechanism is powerful enough to figure out that
fiveTimes m = 5 .* m
is to be resolved using that instance. Essentially because it 'knows'
that NaturalModule is a (named) identity Functor, and it is the only one
that has been encountered (and could work) during the unification phase
of type inference. So it is able to insert the necessary (identity!)
coercions. While general coercions are very evil, those which are
automatically-provable identities 'by construction', are perfectly OK.
Jacques
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/25 Edward Kmett ekm...@gmail.com: 2011/7/25 Gábor Lehel illiss...@gmail.com 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.html 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/Data-Functor-Representable-Trie.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. Ah, so it was an earlier version of the same package that I saw? Okay. I'm aware of the advantages of the explicit isomorphisms, I was just wondering if maybe the GADT equality witnesses also had some advantages which caused you to use both in different places - but now I know that you don't, in fact, use both of them in different places, but have switched from to the other. -- Work is punishment for failing to procrastinate effectively. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Superclass Cycle via Associated Type
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.
Simon
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 22 July 2011 20:07
To: Simon Peyton-Jones
Cc: Gábor Lehel; glasgow-haskell-users@haskell.org
Subject: Re: Superclass Cycle via Associated Type
2011/7/22 Simon Peyton-Jones
simo...@microsoft.commailto:simo...@microsoft.com
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 r
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/23 Edward Kmett ekm...@gmail.com: 2011/7/23 Gábor Lehel illiss...@gmail.com 2011/7/22 Dan Doel dan.d...@gmail.com: 2011/7/22 Gábor Lehel illiss...@gmail.com: 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. I believe we actually discussed this on IRC. :-) 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. 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? -- Work is punishment for failing to procrastinate effectively. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
On Mon, Jul 25, 2011 at 4:46 AM, Simon Peyton-Jones simo...@microsoft.comwrote: 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/25 Gábor Lehel illiss...@gmail.com 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.html 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/Data-Functor-Representable-Trie.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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
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. In a general categorical setting, this is not so surprising as 'classes' and 'instances' are the same thing. A 'class' typically has many non-isomorphic models while an 'instance' typically has a unique model (up to isomorphism), but these are not laws [ex: real-closed Archimedian fields have a unique model even though a priori that is a class, and the Integers have multiple Monoid instances]. Jacques ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
On Mon, Jul 25, 2011 at 1:40 PM, Jacques Carette care...@mcmaster.cawrote:
**
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/22 Dan Doel dan.d...@gmail.com: 2011/7/22 Gábor Lehel illiss...@gmail.com: 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 ... When I last tried this in the 7.0 time frame (before it was discovered that equality superclasses don't actually work yet and got disabled), it gave me a superclass cycle error for the first halves of those contexts, and for the second halves (the equality constraints) I believe it caused some kind of context stack depth to be exceeded (again because of the recursiveness). I'll have to try this again once I manage to get 7.2 compiled. -- Dan -- Work is punishment for failing to procrastinate effectively. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/23 Gábor Lehel illiss...@gmail.com 2011/7/22 Dan Doel dan.d...@gmail.com: 2011/7/22 Gábor Lehel illiss...@gmail.com: 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 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
On Thu, Jul 21, 2011 at 6:46 PM, Simon Peyton-Jones
simo...@microsoft.com 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-boun...@haskell.org
[mailto:glasgow-haskell-users-boun...@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.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Superclass Cycle via Associated Type
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.
Simon
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/22 Simon Peyton-Jones simo...@microsoft.com:
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.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/22 Simon Peyton-Jones simo...@microsoft.com
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
2011/7/22 Gábor Lehel illiss...@gmail.com: 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
Re: Superclass Cycle via Associated Type
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 dan.d...@gmail.com
2011/7/22 Gábor Lehel illiss...@gmail.com:
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Superclass Cycle via Associated Type
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?
Simon
From: glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-users-boun...@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
Re: Superclass Cycle via Associated Type
*Simon Peyton-Jones* simonpj at microsoft.com glasgow-haskell-users%40haskell.org?Subject=Re%3A%20Superclass%20Cycle%20via%20Associated%20TypeIn-Reply-To=%3C59543203684B2244980D7E4057D5FBC125661A72%40DB3EX14MBXC308.europe.corp.microsoft.com%3E -- 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. This is actually an active problem for me in my 'algebra' package. We can define additive, additive abelian and multiplicative semigroups: class Additive m where (+) :: m - m - m class Additive m = Abelian m class Multiplicative m where (*) :: m - m - m then we can define semirings (in the semirings are semigroups with distributive laws sense): class (Additive m, Abelian m, Multiplicative m) = Semiring m then to define monoids, we enforce the fact that every additive monoid is a module over the naturals. class (Semiring r, Additive m) = LeftModule r m where (.*) :: r - m - m class LeftModule Natural m = Monoidal m where This makes it an obligation of anyone that provides a Monoidal instance to ensure that they also supply the LeftModule, side-stepping what would be a hugely overlapping instance, and ensuring we can rely on it. But we weren't able to exploit the fact that any Additive semigroup forms a module over N+, due to the cycle. Moreover, we also weren't able to encode that every semiring is a module over itself. If we could have superclass cycles, we could restate this all as class LeftModule Whole m = Additive m where (+) :: m - m - m class Additive m = Abelian m class (Semiring r, Additive m) = LeftModule r m where (.*) :: r - m - m class Multiplicative m where (*) :: m - m - m class LeftModule Natural m = Monoidal m where zero :: m class (Abelian m, Multiplicative m, LeftModule m m) = Semiring m class (LeftModule Integer m, Monoidal m) = Group m where recip :: m - m class Multiplicative m = Unital m where one :: m class (Monoidal r, Unital r, Semiring r) = Rig r where fromNatural :: Natural - r fromNatural n = n .* one class (Rig r, Group r) = Ring r where fromInteger :: Integer - r fromInteger n = n .* one ... There are a number of typeclass cycles in there, but I can safely instantiate the whole mess without any overlapping instances and I already have to ball all of these classes up in the same 'Internals' module to avoid orphans instances anyways. Using the usual dodge of a newtype to provide Self module over any given semiring is particularly unsatisfying because the Natural and Integer multiplication become horrific, and I wind up having to multiply the code below this point in the hierarchy to deal with the 'self algebra' cases. =/ I've also run into the problem about once or twice a year when encoding other concepts that are usually more categorical in nature. I would love to be able to do this. -Edward Kmett ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
On Wed, Jul 20, 2011 at 10:07 PM, Ryan Trinkle ryant5...@gmail.com wrote: 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 :: * Did you mean class (A x) = C x where type A x :: * -- Anupam ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Superclass Cycle via Associated Type
This isn't a GHC limitation. The report specifies that the class
hierarchy must be a DAG. So C cannot require itself as a prerequisite,
even if it's on a 'different' type.
Practically, in the implementation strategy that GHC (and doubtless
other compilers) use, the declaration:
class C (A x) = C x ...
means that a C x dictionary contains a C (A x) dictionary, which
contains a C (A (A x)) dictionary And dictionaries are strictly
evaluated, so this sort of infinite definition cannot work.
-- Dan
On Wed, Jul 20, 2011 at 12:37 PM, Ryan Trinkle ryant5...@gmail.com wrote:
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
