On Fri, 2008-10-03 at 12:22 +0200, 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.

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

instane Container Maybe where... What does copy :: Maybe -> IO Maybe mean?

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 ;-)). 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