[Haskell-cafe] Type classes

[Johannes Gerer]

What about these two very simple type classes. Are they equivalent?
(As Monad and ArrowApply)

(This actually compiles in GHC)

class Pointed f where
  pure  :: a -> f a

class Unit f where
  unit :: f a a

newtype UnitPointed f a = UnitPointed f a a
instance Unit f => Pointed (UnitPointed f) where
  pure f = UnitPointed unit

newtype Kleisli f a b = Kleisli (a -> f b)
instance Pointed f => Unit (Kleisli f) where
  unit = Kleisli pure

On Tue, May 28, 2013 at 6:05 PM, Johannes Gerer <kuerzn at gmail.com> wrote:
> Ok, now I see a difference, why Kleisli can be used to relate
> typeclasses (like Monad and ArrowApply) and Cokleisli can not:
>
> "Kleisli m () _"  =  "() -> m _" is isomorphic to "m _"
>
> whereas
>
> "Cokleisli m () _" = "m _ -> ()" is not.
>
> Can somebody point out the relevant category theoretical concepts,
> that are at work here?
>
>
>
> On Tue, May 28, 2013 at 5:43 PM, Tom Ellis
> <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> wrote:
>> On Tue, May 28, 2013 at 05:21:58PM +0200, Johannes Gerer wrote:
>>> That makes sense. But why does
>>>
>>> instance Monad m => ArrowApply (Kleisli m)
>>>
>>> show that a Monad can do anything an ArrowApply can (and the two are
>>> thus equivalent)?
>>
>> I've tried to chase around the equivalence between these two before, and
>> I didn't find the algebra simple.  I'll give an outline.
>>
>> In non-Haskell notation
>>
>> 1) instance Monad m => ArrowApply (Kleisli m)
>>
>> means that if "m" is a Monad then "_ -> m _" is an ArrowApply.
>>
>> 2) instance ArrowApply a => Monad (a anyType)
>>
>> means that if "_ ~> _" is an ArrowApply then "a ~> _" is a Monad.
>>
>> One direction seems easy: for a Monad m, 1) gives that "_ -> m _" is an
>> ArrowApply.  By 2), "() -> m _" is a Monad.  It is equivalent
>> to the Monad m we started with.
>>
>> Given an ArrowApply "_ ~> _", 2) shows that "() ~> _" is a Monad.  Thus by
>> 1) "_ -> (() ~> _)" is an ArrowApply.  I believe this should be the same
>> type as "_ ~> _" but I don't see how to demonstrate the isomorphsim here.
>>
>> Tom
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe