nicolas
nicolas

Reputation: 9805

Free monad and type constraints

I am looking for practical strategies or tips for dealing with constraints in haskell, as illustrated by the case below.


I have a functor Choice and I want to transform an interpreter from Choice x functor to m x to an interpreter from Free Choice x to m x.

-- Choice : endofunctor  
data Choice next = Choice next next deriving (Show)
instance Functor Choice where 
   fmap f (Choice a b) = Choice (f a) (f b)

-- I have a function from the functor to a monad m
inter1 :: Choice x -> IO x
inter1 (Choice a b) = do 
  x <- readLn :: IO Bool 
  return $ if x then a else b

-- universal property gives me a function from the free monad to m 
go1 :: Free Choice x -> IO x
go1 = interpMonad inter1

where

type Free f a = FreeT f Identity a
data FreeF f r x = FreeF (f x) | Pure r deriving (Show)
newtype FreeT f m r = MkFreeT { runFreeT :: m (FreeF f r (FreeT f m r)) }

instance Show (m (FreeF f a (FreeT f m a))) => Show (FreeT f m a) where
  showsPrec d (MkFreeT m) = showParen (d > 10) $
    showString "FreeT " . showsPrec 11 m

instance (Functor f, Monad m) => Functor (FreeT f m) where
    fmap (f::a -> b) (x::FreeT f m a)  =
        MkFreeT $ liftM f'  (runFreeT x)
                where f' :: FreeF f a (FreeT f m a) -> FreeF f b (FreeT f m b)
                      f' (FreeF (fx::f (FreeT f m a))) =  FreeF $ fmap (fmap f) fx
                      f' (Pure r) = Pure $ f r

instance (Functor f, Monad m) => Applicative (FreeT f m) where
  pure a = MkFreeT . return $ Pure a
  (<*>) = ap

instance (Functor f, Monad m) => Monad (FreeT f m) where
    return = MkFreeT . return . Pure
    (MkFreeT m) >>= (f :: a -> FreeT f m b)  =  MkFreeT $ -- m (FreeF f b (FreeT f m b))
           m  >>= -- run the effect in the underlying monad !
             \case FreeF fx -> return . FreeF . fmap (>>= f) $ fx -- continue to run effects
                   Pure r -> runFreeT (f r) -- apply the transformation

interpMonad :: (Functor f, Functor m, Monad m) =>
               (forall x . f x -> m x) ->
               forall x. Free f x -> m x
interpMonad interp (MkFreeT iFfxF) = (\case
      Pure x -> return x
      FreeF fxF -> let mmx =  interp $ fmap (interpMonad interp) fxF
                   in join mmx) . runIdentity $ iFfxF

All is fine until I require Show x in my interpreter.

interp2 :: Show x => Choice x -> IO x
interp2 (Choice a b) = return a -- we follow left


go2 :: Show x => Free Choice x -> IO x
go2  = interpMonad interp2   -- FAILS

Then it can not find the show constraint to apply in interp2

I suspected the quantifiers were the problem, so I simplified to

lifting :: (forall x . x -> b) ->
           (forall x.  x -> b)
lifting = id

lifting2 :: (forall x . Show x => x -> b) ->
            (forall x . Show x => x -> b)
lifting2 = id


somefunction :: Show x => x -> String
somefunction = lifting show    -- FAILS

somefunction2 :: Show x => x -> String
somefunction2 = lifting2 show  -- OK

This highlight the problem : Could not deduce (Show x1) arising from a use of ‘show’ from the context (Show x) we have two distinct type variable, and constraint do not flow from one to the other.


I could write some specialized function playing with the constraints as follows (does not work btw) but my question is what are the practical strategies for dealing with this ? (the equivalent of undefined, look at the type, go on...)

interpMonad2 :: (Functor f, Functor m, Monad m) =>
               (forall x . ( Show (f x)) => f x -> m x) ->
               forall x.  ( Show (Free f x)) => Free f x -> m x
interpMonad2 interp (MkFreeT iFfxF) = (\case
      Pure x -> return x
      FreeF fxF -> let mmx =  interp $ fmap (interpMonad interp) fxF
                   in join mmx) . runIdentity $ iFfxF

edit

based on the answer provided, here is the modification for the lifting function.

lifting :: forall b c. Proxy c
           ->  (forall x . c x => x -> b)
           ->  (forall x . c x => x -> b)
lifting _ = id


somefunction3 :: Show x => x -> String
somefunction3 = lifting (Proxy :: Proxy Show) show

Upvotes: 2

Views: 185

Answers (1)

user2407038
user2407038

Reputation: 14578

I don't see your interpMonad function, so I will include one possible definition here:

interpMonad :: forall f m x . (Functor f, Monad m) 
            => (forall y . f y -> m y) -> Free f x -> m x 
interpMonad xx = go . runIdentity . runFreeT  where 
  go (FreeF x) = xx x >>= go . runIdentity . runFreeT
  go (Pure  x) = return x 

In order to also have a class constraint on the inner function, you simply add the constraint to the inner function. You also need the correct constraint on the type Free, and you need the extra Proxy to help the typechecker out a bit. Otherwise, the definition of the function is identical:

interpMonadC :: forall f m x c . (Functor f, Monad m, c (Free f x)) 
             => Proxy c 
             -> (forall y . c y => f y -> m y) 
             -> (Free f x -> m x) 
interpMonadC _ xx = go . runIdentity . runFreeT  where 
  go (FreeF x) = xx x >>= go . runIdentity . runFreeT
  go (Pure  x) = return x 

And now quite simply:

>:t interpMonadC (Proxy :: Proxy Show) interp2
interpMonadC (Proxy :: Proxy Show) interp2
  :: Show x => Free Choice x -> IO x

Upvotes: 3

Related Questions