Alexander Solla wrote:

You specifically ask withConstraintsOf to accept only Suitable2's when you say

withConstraintsOf :: Suitable2 m a b => m a b -> (Constraints m a b -> k) -> k

But you aren't saying that the argument of withConstraintsOf IS a Suitable2, when you say:

instance (RCategory c1, RCategory c2) => RCategory (c1 :***: c2) where
id = withResConstraints $ \ProdConstraints -> id :***: id
-- f@(f1 :***: f2) . g@(g1 :***: g2) =
--   withResConstraints $ \ProdConstraints ->
--   withConstraintsOf f $ \ProdConstraints ->
--   withConstraintsOf g $ \ProdConstraints ->
--   (f1 . g1) :***: (f2 . g2)

As I understand, Sjoerd expects this to be done at the definition of (.) in the type class RCategory, so that an instance method can relay on the constraints collected by it:

class RCategory (~>) where
  id :: Suitable2 (~>) a a => a ~> a
  (.) :: (Suitable2 (~>) b c, Suitable2 (~>) a b, Suitable2 (~>) a c) => b ~> c -> a ~> b -> a ~> c

A simple example:

class Show el=> ExceptionNote el where
comment:: Show exception=> exception-> el-> String

instance ExceptionNote Int where
comment exception refId = show refId ++ ": " ++ show exception

Here you don't need to constrain «exception» to be of «Show» at the instance declaration. So it does not appear wrong for Sjoerd to expect f and g to already be of Suitable2...

This is exciting stuff, I am really a little astonished about the giant leap Haskell has made since my efforts to translate the examples of Rydeheart & Burstall, which actually was my intro to categories, from ML to Haskell. This looks very elegant... Maybe it's time for a second edition of the unique approach of Rydeheart & Burstall on basis of Haskell? Wow, really cool stuff... :-)

Cheers,

Nick