Maybe's Free

MaybeはFreeモナドの一つです。特に、Maybe = Free Proxyです。

data Maybe a = Nothing | Just a
data Free f a = Pure a | Wrap (f (Free f a))
data Proxy a = Proxy

-- 自然変換の矢印
type (~>) f g = forall x. f x -> g x

maybeToFree :: Maybe ~> Free Proxy
maybeToFree Nothing  = Wrap Proxy
maybeToFree (Just a) = Pure a

freeToMaybe :: Free Proxy ~> Maybe
freeToMaybe (Pure a)      = Just a
freeToMaybe (Wrap _proxy) = Nothing

これは単にFunctorとして同型であるだけでなく、Monadとしても同型になっています¹。 （そもそも、Maybeと同型なFunctorに定義できるMonadのインスタンスは一つしかありません。）

ここまでならば「ちょっと面白い」というだけなのですが、Freeモナドというのはとても特別なモナドです。 Freeモナドの普遍性というものがあるからです。

• どんなモナドmについても、モナド準同型 tr :: Free f ~> m と自然変換 h :: f ~> mは、 以下のfoldFreeによって一対一に対応する

  foldFree :: Monad m => (f ~> m) -> (Free f ~> m) 
  foldFree _ (Pure a)   = pure a
  foldFree h (Wrap fmx) = h fmx >>= foldFree h

MaybeはFree Proxyに同型であることを使えば、“Maybeモナドの普遍性”を以下のように得られます。

• どんなモナドmについても、モナド準同型 tr :: Maybe ~> m と自然変換 h :: Proxy ~> mは、 以下のfoldMaybeによって一対一に対応する

  foldMaybe :: Monad m => (Proxy ~> m) -> (Maybe ~> m)
  foldMaybe _ (Just a) = pure a
  foldMaybe h Nothing  = h Proxy

特に、モナド準同型 tr :: Maybe ~> m は tr Nothing :: ∀x. m x のみによって特徴付けられることがわかります。

また、Maybe = Free Proxyなのであれば、FreeT Proxy mは何でしょうか？ うれしいことに、それはMaybeT mと一致します²。

newtype MaybeT m a = MaybeT (m (Maybe a))

data FreeF f a b = PureF a | WrapF (f b)
newtype FreeT f m a = FreeT (m (FreeF f a (FreeT f m a)))

maybeT_freeT :: ∀m. Monad m => MaybeT m ~> FreeT Proxy m
maybeT_freeT (MaybeT x) = FreeT (maybeToFreeF <$> x)
  where maybeToFreeF (Just x) = PureF x
        maybeToFreeF Nothing  = WrapF Proxy

freeT_maybeT :: ∀m a. Monad m => FreeT Proxy m ~> MaybeT m
freeT_maybeT (FreeT x) = MaybeT (freeFToMaybe <$> x)
  where freeFToMaybe (PureF x)     = Just x
        freeFToMaybe (WrapF Proxy) = Nothing

FreeTにも普遍性があります。

• m, nをモナドとする。任意のモナド準同型tr :: FreeT f m ~> nは、 自然変換f :: f ~> nとモナド準同型tr2 :: m ~> nの組(f, tr2)へ、 以下のmergeFreeTによって一対一に対応する。

  mergeFreeT :: Monad n => (f ~> n) -> (m ~> n) -> (FreeT f m ~> n)
  mergeFreeT f tr2 = go
    where
      go (FreeT mx) = tr2 mx >>= goF
  
      goF (PureF a) = pure a
      goF (WrapF fy) = f fy >>= go

これも”MaybeTモナドの普遍性”に翻訳してみましょう。

• m, nをモナドとする。任意のモナド準同型tr :: MaybeT m ~> nは、 自然変換h :: Proxy ~> nとモナド準同型tr2 :: m ~> nの組(f, tr2)へ、 以下のmergeMaybeTによって一対一に対応する。

  mergeMaybeT :: Monad n => (Proxy ~> n) -> (m ~> n) -> (MaybeT m ~> n)
  mergeMaybeT h tr2 = go
    where
      go (MaybeT mx) = tr2 mx >>= maybe (h Proxy) pure

これは結構意外なことではないでしょうか？

例えば m a = Reader k a = k -> aとすると、モナド準同型trとは自然変換

tr :: MaybeT (Reader k) ~> n
--  ~ ∀a. (k -> Maybe a) -> n a

であって、モナド演算を保つという条件を満たすものです。 (k -> Maybe a)という関手は非常に”大きい”関手で、 仮に単独のdata F a = ...で表そうとするならば、 2^|k|個のコンストラクタを設けないといけません。 そのため、この”大きな”関手から別の関手nへの自然変換は、nによっては本当に凄まじい数が存在します。

ですが、もしその自然変換がモナド準同型であると知っているならば、 モナド準同型tr2 :: ∀x. (k -> x) -> n xとただ一つの値h Proxy :: ∀x. n xだけで記述できることがわかったのです。

凄いでしょう！