Reputation: 9805
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
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