自由monad和类型约束

Question

我正在寻找实用的策略或技巧来处理haskell中的限制因素，如下面的案例所示。

我有一个函子Choice，我想把解释器从Choice x函子转换成m x，再把解释器从Free Choice x转换到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

哪里

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

在我需要在我的解释器中使用Show x之前，一切都很好。

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

则无法找到在interp2中应用的显示约束。

我怀疑量词是问题所在，所以我简化为

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

这突出了问题：Could not deduce (Show x1) arising from a use of ‘show’ from the context (Show x)我们有两个不同的类型变量，并且约束不从一个流到另一个。

我可以编写一些专门的函数，如下所示(不起作用)，但我的问题是，处理这个问题的实际策略是什么？(相当于未定义的类型，看看类型，继续.)

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

编辑

根据所提供的答案，下面是对lifting函数的修改。

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

Answer 1

我没有看到您的interpMonad函数，因此我将在这里包含一个可能的定义：

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 

为了在内部函数上也有一个类约束，只需将约束添加到内部函数。您还需要对类型Free进行正确的约束，并且需要额外的Proxy来帮助打字机解决一些问题。否则，函数的定义是相同的：

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 

现在很简单：

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