Как кодировать действия, которые принимают монадические аргументы со свободными (или более свободными) монадами?

Question

Большинство монадических функций принимают чистые аргументы и возвращают монадическое значение. Но есть некоторые, которые нужны также монадические аргументы, например:

mplus :: (MonadPlus m) => m a -> m a -> m a 

finally :: IO a -> IO b -> IO a 

forkIO :: m() -> m ThreadId 

-- | From Control.Monad.Parallel 
forkExec :: m a -> m (m a) 

Каждые из них, кажется, чтобы вызвать различные проблемы, и я не могу получить понимание общего способа, как кодируют таких действий с использованием свободные монады.

• В обоих finally и forkIO проблема заключается в том, что монадическая аргумент другого типа, чем результат. Но для бесплатно нужно было бы, чтобы они были одного типа, так как IO a заменяется переменной типа типа кодировки, например data MyFunctor x = Finally x x x, которая будет кодировать только IO a -> IO a -> IO a.

  В From zero to cooperative threads in 33 lines of Haskell code автор использует Fork next next в кулак реализации

  cFork :: (Monad m) => Thread m Bool 
  cFork = liftF (Fork False True) 
  

  , а затем использует его для реализации

  fork :: (Monad m) => Thread m a -> Thread m() 
  

  , где вход и выход имеют разные типы. Но я не понимаю, было ли это получено с использованием какого-то процесса или просто специальной идеи, которая работает для этой конкретной цели.

• mplus, в частности, в заблуждении: наивное кодирование, как

  data F b = MZero | MPlus b b 
  

  распределяет над >>= и suggested better implementation является более сложным. А также нативная реализация бесплатного MonadPluswas removed from free.

  В freer это реализуется путем добавления

  data NonDetEff a where 
      MZero :: NonDetEff a 
      MPlus :: NonDetEff Bool 
  

  Почему MPlusNonDetEff Bool вместо NonDetEff a a? И есть способ, как заставить его работать с Free, где нам нужен тип данных, чтобы быть функтором, кроме использования CoYoneda functor?

• Для forkExec Я понятия не имею, как действовать вообще.

Answer 1

Я отвечу только о размере части Freer.Напомним определение:

data Freer f b where 
    Pure :: b -> Freer f b 
    Roll :: f a -> (a -> Freer f b) -> Freer f b 

Теперь с

data NonDetEff a where 
    MZero :: NonDetEff a 
    MPlus :: NonDetEff Bool 

мы можем определить

type NonDetComp = Freer NonDetEff 

Когда Roll применяется к MPlus, a унифицирована с Bool и тип второго аргумента Bool -> NonDetEff b который в основном кортеж:

tuplify :: (Bool -> a) -> (a, a) 
tuplify f = (f True, f False) 

untuplify :: (a, a) -> (Bool -> a) 
untuplify (x, y) True = x 
untuplify (x, y) False = y 

В качестве примера:

ex :: NonDetComp Int 
ex = Roll MPlus $ Pure . untuplify (1, 2) 

Таким образом, мы можем определить MonadPlus экземпляр для недетерминированных вычислений

instance MonadPlus NonDetComp where 
    mzero  = Roll MZero Pure 
    a `mplus` b = Roll MPlus $ untuplify (a, b) 

и запустить их

run :: NonDetComp a -> [a] 
run (Pure x)  = [x] 
run (Roll MZero f) = [] 
run (Roll MPlus f) = let (a, b) = tuplify f in run a ++ run b