pepeiborra/control-monad-free

Missing function

Closed this issue · 2 comments

I came across this sentence in a paper (IR for the Masses):
"Thus a reflection ρ : F I O → M I → M O is a natural transformation from the functor F I to the monad M I → M− and as such induces a monad morphism from the free monad on F I to this monad."

This suggests the following function:

induce :: (Functor f, Monad m) => (forall a. f a -> m a) -> Free f a -> m a
induce f = foldFree return (join . f)

(induce is probably not the best name for this function.)

mapFree can be written with induce:

mapFree eta = induce (Impure . fmap Pure . eta)

but that's slower than the current implementation, unless GHC can optimize the overhead away.

Hi Sjoerd,
Thanks for the input. I have uploaded to Hackage a new version including induce.
I cooked an example based on Swierstra calculator:

import Control.Monad.Free
import Control.Monad.State

data CalcF a = Incr Int a
             | Recall (Int -> a)
             | Clear a
  deriving Functor

type Calc a = Free CalcF a

clear :: Calc ()
incr  :: Int -> Calc ()
clear  = Impure $ Clear (Pure ())
incr i = Impure $ Incr i (Pure ())
recall = Impure (Recall Pure)

runCalc :: Calc a -> Int
runCalc = (`execState` 0) . induce f where
  f (Incr i r) = modify (+i) >> return r
  f (Clear r)  = put 0 >> return r
  f (Recall k) = get >>= \i -> return (k i)

Do you have any other examples in mind?

I like your example a lot!

This was the Agda code I wanted to implement in Haskell:
http://personal.cis.strath.ac.uk/~ng/MonadicIR.agda

It now becomes:

class Reflective f where
reflect :: Monad m => f i o -> m i -> m o

decode :: (Reflective f, Functor (f i), Monad m) => Free (f i) o -> m i -> m o
decode = runReaderT . induce (ReaderT . reflect)

Pretty nice, but totally useless, as it all has to be done at type level to be of any use for induction recursion.