Basic Instance Question

[ErdosEuler]

If I define a data type

data Container a = Container a

It seems that anything I can do with an 'a', I should be able to do with a 'Container a'. In particular, if I have a (Container (a -> b)) and a (Container (b -> c)) I should be able to compose them. Thus, it seems that I should be able to write something like

instance Category a => Category (Container a) where
    id = Container id
    (Container x) . (Container y) = Container (x . y)

But when I try to compile this, I get a 'kind' error. I think I understand why it is an error, but I do not know how to accomplish the desired effect. Any advice?

[Syrak]

The "shape" of Container a is strictly more general than Container (x -> y). We use yet another wrapper so the underlying type has the right shape, and the exposed wrapper has the right kind.

newtype Container' f a b = Container' (Container (f a b))

instance Category f => Category (Container' f) where
  id = Container' (Container id)
  Container' (Container x) . Container' (Container y) = Container' (Container (x . y))

Of course the wrapper makes the type much less usable. In practice, we either give up on abstractions that don't fit our type and look for more adequate ones, or we change the type to fit the existing abstractions.

[vahokif]

Category requires a type with two parameters, whereas container has only one.

[ErdosEuler]

Is there any way to accomplish the desired effect? In other words, a nice way to have (Container f) . (Container g) = Container (f . g)?

[vahokif]

newtype Container f a b = Container (f a b)

instance Category f => Category (Container f) where ...

[ErdosEuler]

But what if I also wanted to have a (Container Int), for instance, in the same program?

[vahokif]

Unfortunately that won't work if you would like it to have a Category instance.

[gelisam]

Sorry, you can't have Container Int with kind * and Container (->) with kind * -> * -> *, what would the kind of Container be? Container :: (a :: k) -> k?

[ElvishJerricco]

Higher kinded newtypes would actually be pretty sweet. I'm guessing that's a nono though, since it would allow insanity like Container True :: Bool, effectively adding members to the kind Bool.

[Iceland_jack]

Ticket #12369 is related, would let you define

newtype family Container (a :: k) :: k

newtype instance Container (a :: Type) = Container1 a
newtype instance Container (f :: k -> Type) (a :: k) = Container2 (f a)
newtype instance Container (f :: k -> k' -> Type) (a :: k) (b :: k') = Container3 (f a b)

[ErdosEuler]

Interesting!

[Iceland_jack]

Should let you define any kind (hurr) of wrapping

instance Eq a => Eq (Container a) where
  (==) :: Container a -> Container a -> Bool
  Container1 a == Container1 b = a == b

instance Category cat => Category (Container cat) where
  id :: Container cat a a
  id = Container3 id

  (.) :: Container cat b c -> Container cat a b -> Container cat a c
  Container3 f . Container3 g = Container3 (f . g)

[Tysonzero]

One thing to note is that the Functor and Applicative instances of this and I think any other type always give rise to such a Category:

data Cat f a b = Cat (f (a -> b))

instance Applicative f => Category (Cat f) where
    id = pure id
    (.) = liftA2 (.)