[Haskell-cafe] Restricted categories

[Alexander Solla]

On Feb 20, 2010, at 6:32 PM, Nick Rudnick wrote:

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

   There really are instances missing.  The context is coming from here:

> The instance for Suitable2 restricts objects to IsProduct, and  
> requires the Fst and Snd parts of the objects to be suitable in c1  
> resp. c2:
>
>> instance (IsProduct a, IsProduct b, Suitable2 c1 (Fst a) (Fst b),  
>> Suitable2 c2 (Snd a) (Snd b)) => Suitable2 (c1 :***: c2) a b where
>>  data Constraints (c1 :***: c2) a b = (IsProduct a, IsProduct b,  
>> Suitable2 c1 (Fst a) (Fst b), Suitable2 c2 (Snd a) (Snd b)) =>  
>> ProdConstraints
>>  constraints _ = ProdConstraints


Given types A and B, the product A x B has a type Fst which is A, and  
a type Snd which is B -- by construction:

> class IsProduct p where
>  type Fst p :: *
>  type Snd p :: *
>  fst :: p -> Fst p
>  snd :: p -> Snd p


So, if we have two products named a and b, and a = A + B, b = C + D  
(letting the first type in the addition be Fst, and the latter be Snd  
in each), a x b has
four "components":  (A x C)  +  (B x C) + (A x D) +  (B x D).

  a x b = (A | B) x (C | D) = (Fst a | Snd a) x (Fst b | Snd b) = (Fst  
a, Fst b) + (Snd a, Fst b) + (Fst a, Snd b) + (Snd a, Snd b)

This really comes down to the semantics of Suitability2, but I think  
Sjoerd made a logic mistake, and is trying to make a product out of a  
pair of products, in stead of a pair of categories.