证明自由单子的函子定律;我做得对吗

Question

我有点难以理解如何证明自由monads的Functor定律和Monad定律。 首先，让我提出我正在使用的定义：

data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Free fa) = Free (fmap (fmap f) fa)
instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= f = f a
    Free fa >>= f = Free (fmap (>>=f) fa)
{-
Functor laws:
(1) fmap id x == x
(2) fmap f (fmap g x) = fmap (f . g) x
Monad laws:
(1) return a >>= f   ==  f a
(2) m >>= return     ==  m
(3) (m >>= f) >>= g  ==  m >>= (x -> f x >>= g)
-}

如果我理解正确，等式证明需要诉诸归纳假设，它或多或少像这个例子：

Proof: fmap id == id
Case 1: x := Pure a
fmap id (Pure a)
  == Pure (id a)   -- Functor instance for Free
  == Pure a        -- id a == a
Case 2: x := Free fa
fmap id (Free fa)
  == Free (fmap (fmap id) fa)  -- Functor instance for Free f
  == Free (fmap id fa)         -- By coinductive hypothesis; is this step right?
  == Free fa                   -- Functor f => Functor (Free f), + functor law 

我已经突出显示了我不确定我是否做对的步骤。

如果该证明是正确的，那么第二定律的Free构造函数案例的证明如下：

fmap f (fmap g (Free fa))
  == fmap f (Free (fmap (fmap g) fa))
  == Free (fmap (fmap f) (fmap (fmap g) fa))
  == Free (fmap (fmap f . fmap g) fa)
  == Free (fmap (fmap (f . g)) fa)           -- By coinductive hypothesis
  == fmap (f . g) (Free fa)

Answer 1

是的，这是正确的。共归纳的"基本情况"是Pure构造函数，归纳超过Free构造函数的嵌套级别。

完整的证明是

-- 1. First functor law
--   a. Base case
fmap id (Pure a) = Pure (id a) -- Functor instance for Free
                 = Pure a      -- definition of id
--   b. Inductive case
fmap id (Free fa) = Free (fmap (fmap id) fa) -- Functor instance for Free
                  = Free (fmap id fa)        -- coinductive hypothesis
                  = Free fa                  -- 1st functor law for f
-- 2. Second functor law
--   a. Base case
fmap f (fmap g (Pure a)) = fmap f (Pure (g a))   -- Functor instance for Free
                         = Pure (f (g a))        -- Functor instance for Free
                         = Pure ((f . g) a)      -- Definition of (.)
                         = fmap (f . g) (Pure a) -- Functor instance for Free
--   b. Inductive case
fmap f (fmap g (Free fa)) = fmap f (Free (fmap (fmap g) fa))        -- Functor instance for Free
                          = Free (fmap (fmap f) (fmap (fmap g) fa)) -- Functor instance for Free
                          = Free (fmap (fmap f . fmap g) fa)        -- 2nd functor law for f
                          = Free (fmap (fmap (f . g) fa))           -- Coinductive hypothesis
                          = fmap (f . g) (Free fa)                  -- Functor instance for Free