[Haskell-cafe] Kind-agnostic type classes

[Luke Palmer]

On Fri, Oct 3, 2008 at 4:22 AM, Florian Weimer <fw at deneb.enyo.de> wrote:
> I'm trying to encode a well-known, informally-specified type system in
> Haskell.  What causes problems for me is that type classes force types
> to be of a specific kind.  The system I'm targeting however assumes that
> its equivalent of type classes are kind-agnositic.

There is no choice of kinds, they are forced by the methods (since the
kind of an actual argument is * by definition).  But see below.

> For instance, I've got
>
> class Assignable a where
>    assign :: a -> a -> IO ()
>
> class Swappable a where
>    swap :: a -> a -> IO ()
>
> class CopyConstructible a where
>    copy :: a -> IO a
>
> class (Assignable a, CopyConstructible a) => ContainerType a
>
> class (Swappable c, Assignable c, CopyConstructible c) => Container c where
>    size :: (Num i, ContainerType t) => c t -> IO i

Which is illegal because the three above classes force c to be kind *,
but you're using it here as kind * -> *.

What you want is not this informal "kind-agnostic" classes so much as
quantification in constraints, I presume.  This, if it were supported,
would solve your problem.

class (forall t. Swappable (c t), forall t. Assignable (c t), forall
t. CopyConstructible (c t)) => Contanter c where ...

Incidentally, you *can* do this if you go to a dictionary passing
style (because then you are providing the proofs, rather than asking
the compiler to infer them, which is probably undecidable (what isn't
;-)).

data Assignable a = Assignable { assign :: a -> a -> IO () }
data Swappable a = Swappable { swap :: a -> a -> IO () }
data CopyConstructible a = CopyConstructible { copy :: a -> IO a }
data ContainerType a = ContainerType (Assignable a) (CopyConstructor a)
data Container c t = Container {
   containerAssignable :: forall t. ContainerType t -> Assignable (c t),
   containerSwappable :: forall t. ContainerType t -> Swappable (c t),
   containerCopyConstructible :: forall t. ContainerType t ->
CopyConstructible (c t),
   size :: forall i. (Num i) => ContainerType t -> c t -> IO i }

And then to make an "instance" of Container (construct an object of
it), you need to provide a "proof" of eg. forall t. ContainerType t ->
Assignable (c t).

For what it's worth, this is a well-known but very infrequently used
technique.  Try to come up with something simpler that accomplishes
the "big picture" you have in mind   (spend more time thinking about
the problem and less about the solution you think you want).

Also, OO-esque modeling like this in Haskell almost always leads to
overcomplexity, pain, and desire for yet more "missing" features.  A
more functional solution will serve you well (it takes time to learn
how to come up with functional solutions).

Luke