Предоставляет ли FreeT преимущества эквационального рассуждения Free?

Ответ 1

Да. FreeT не зависит от каких-либо конкретных свойств базовой монады, кроме того, что это монада. Каждое уравнение, которое вы можете вывести для Free f, имеет эквивалентное доказательство для FreeT f m.

Чтобы продемонстрировать это, повторите упражнение в своем сообщении в блоге, но на этот раз с помощью FreeT:

data TeletypeF x
  = PutStrLn String x
  | GetLine (String -> x)
  | ExitSuccess
  deriving (Functor)

type Teletype = FreeT TeletypeF

exitSuccess :: (Monad m) => Teletype m r
exitSuccess = liftF ExitSuccess

Используйте следующие определения для свободных монадных трансформаторов:

return :: (Functor f, Monad m) => r -> FreeT f m r
return r = FreeT (return (Pure r))

(>>=) :: (Functor f, Monad m) => FreeT f m a -> (a -> FreeT f m b) -> FreeT f m b
m >>= f = FreeT $ do
    x <- runFreeT m
    case x of
        Free w -> return (Free (fmap (>>= f) w))
        Pure r -> runFreeT (f r)

wrap :: (Functor f, Monad m) => f (FreeT f m r) -> FreeT f m r
wrap f = FreeT (return (Free f))

liftF :: (Functor f, Monad m) => f r -> FreeT f m r
liftF fr = wrap (fmap return fr)

Мы можем использовать эквациональные рассуждения, чтобы вывести, что exitSuccess сводится к:

exitSuccess

-- Definition of 'exitSuccess'
= liftF ExitSuccess

-- Definition of 'liftF'
= wrap (fmap return ExitSuccess)

-- fmap f ExitSuccess = ExitSuccess
= wrap ExitSuccess

-- Definition of 'wrap'
= FreeT (return (Free ExitSuccess))

Теперь мы можем представить, что exitSuccess >> m= exitSuccess:

exitSuccess >> m

-- m1 >> m2 = m1 >>= \_ -> m2
= exitSuccess >>= \_ -> m

-- exitSuccess = FreeT (return (Free ExitSuccess))
= FreeT (return (Free ExitSuccess)) >>= \_ -> m

-- use definition of (>>=) for FreeT
= FreeT $ do
    x <- runFreeT $ FreeT (return (Free ExitSuccess))
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- runFreeT (FreeT x) = x
= FreeT $ do
    x <- return (Free ExitSuccess)
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Monad Law: Left identity
-- do { y <- return x; m } = do { let y = x; m }
= FreeT $ do
    let x = Free ExitSuccess
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Substitute in 'x'
= FreeT $ do
    case Free ExitSuccess of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- First branch of case statement matches 'w' to 'ExitSuccess'
= FreeT $ do
    return (Free (fmap (>>= (\_ -> m)) ExitSuccess))

-- fmap f ExitSuccess = ExitSuccess
= FreeT $ do
    return (Free ExitSuccess)

-- do { m; } desugars to 'm'
= FreeT (return (Free ExitSuccess))

-- exitSuccess = FreeT (return (Free ExitSuccess))
= exitSuccess

Блок do в доказательстве принадлежал к базовой монаде, но нам никогда не нужно было использовать какой-либо конкретный исходный код или свойства базовой монады, чтобы манипулировать им экваториально. Единственное свойство, которое нам нужно было знать, было то, что это была монада (любая монада!) И подчинялась законам монады.

Используя только законы монады, мы все еще смогли вывести, что exitSuccess >> m = exitSuccess. Это причина, по которой законы монады имеют значение, потому что они позволяют нам рассуждать о коде в полиморфной базовой монаде, зная только, что это монада.

В более общем плане, это причина, по которой люди говорят, что классы классов должны всегда иметь связанные законы (например, законы монады или законы функтора или законы категории), поскольку они позволяют вам рассуждать о коде, который использует этот тип класса, не обращаясь к конкретным экземплярам этого типа. Без такого рода законов интерфейс типа класса не будет действительно слабо связанным интерфейсом, так как вы не сможете его равнозначно рассуждать без консультации с исходным исходным кодом экземпляра.

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

(forall m. (Monad m) => FreeT f m r) ~ Free f r

Символ ~ означает, что "изоморфен", что означает, что мы должны доказать, что существуют две функции: fw и bw:

fw :: (forall m . (Monad m) => FreeT f m r) -> Free f r

bw :: Free f r -> (forall m . (Monad m) => FreeT f m r)

... такое, что:

fw . bw = id

bw . fw = id

Это интересное доказательство, и я оставляю его как упражнение!