9

我很难理解如何证明自由单子的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)
4

1 回答 1

6

是的，这是正确的。共归纳的“基本情况”是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
于 2013-12-21T13:00:58.457 回答