Re: [Haskell-cafe] Kind-agnostic type classes

On Fri, Oct 3, 2008 at 9:49 AM, Luke Palmer wrote:

On Fri, Oct 3, 2008 at 4:22 AM, Florian Weimer 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 ;-)).

You don't necessarily need explicit dictionaries. For example, I've occasionally wanted to have a constraint (forall a. Show a => Show (f a)). One fairly simple way to do this to declare a new class. class Show1 f where showsPrec1 :: (Show a) => Int -> f a -> ShowS instance Show1 [] where showsPrec1 = showsPrec The same technique is used in Data.Typeable. -- Dave Menendez http://www.eyrie.org/~zednenem/