Skip to content

How to get superclass Category (Kleisli m) to entail Monad m

Summary

The constraint FunctorOf dom cod f implies Category dom and Category cod. Since Category (Kleisli m) implies a Monad m constraint I would like to get a Monad constraint from FunctorOf (Kleisli m) (->) f.

instance Monad m => Category (Kleisli m)

Steps to reproduce

The following program

{-# Language ConstraintKinds          #-}
{-# Language FlexibleInstances        #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language KindSignatures           #-}
{-# Language MultiParamTypeClasses    #-}
{-# Language RankNTypes               #-}
{-# Language TypeOperators            #-}

import Control.Arrow
import Control.Category
import Data.Kind
import Data.Maybe
import Prelude hiding (fmap)

-- type FunctorOf :: Cat d -> Cat c -> Object (d->c)
class (Category dom, Category cod) => FunctorOf dom cod f where
 fmap :: dom a a' -> cod (f a) (f a')

instance FunctorOf (Kleisli Maybe) (->) [] where
 fmap :: Kleisli Maybe a a' -> ([a] -> [a'])
 fmap (Kleisli f) = mapMaybe f

-- from Data.Constraint
-- Dict :: Constraint -> Type
data Dict cls where
 Dict :: cls => Dict cls

-- (:-) :: Cat Constraint
newtype a :- b where
 Sub :: (a => Dict b) -> (a :- b)

-- a functor from `Kleisli m' entails that Kleisli m is a Category.
foo :: FunctorOf (Kleisli m) (->) f :- Category (Kleisli m)
foo = Sub Dict

-- • Could not deduce (Monad m) arising from a use of ‘Dict’
--   from the context: FunctorOf (Kleisli m) (->) f
-- baz :: FunctorOf (Kleisli m) (->) f :- Monad m
-- baz = Sub Dict

Expected behavior

I was hoping the functor constraint in baz would entail a monad constraint.

Is this Bidirectional Type Class Instances? https://arxiv.org/pdf/1906.12242.pdf, it's possible this shouldn't work at all since Category (Kleisli m) doesn't carry around a Monad m dictionary. This is exactly what I need at the moment though!

Environment

  • GHC version used: 8.10.0.20191123
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information