Superclass Cycle via Associated Type
Gábor Lehel
illissius at gmail.com
Fri Jul 22 18:27:39 CEST 2011
2011/7/22 Simon Peyton-Jones <simonpj at 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.
More information about the Glasgow-haskell-users
mailing list