Free monad

TIL

720

kiennt viết ngày 16/09/2016

Free monad là gì?

Với h là một Functor, chúng ta có thể tạo ra một monad từ h bằng cách định nghĩa như sau

data Free h a = Pure a  | Free (h (Free h a))

instance Functor h => Functor Free h where 
    fmap f (Pure a) = Pure (f a)                               (1)
    fmap f (Free ha) = Free (fmap (fmap f) ha)                 (2)

instance Functor h => Monad Free h where
    return = Pure                                              (3)
    Pure a >>= f = f a                                         (4)
    Free ha >>= f = Free (fmap (>>= f) ha)                     (5)

Chứng minh Free f là Functor

Trước hết chúng ta sẽ chưng minh cách định nghĩa hàm fmap là thoả mãn các rule của Fuctor
(rule của Fuctor có thể xem ở bài viết trước)

Trong vế phải của (2), hàm fmap chính là hàm fmap của functor f. Hàm fmap tuân thủ theo
luật của functor f, nên có các tính chất sau:

      fmap id (h a) = h a                                      (6)
      fmap (f . g) (h a) = fmap f . (fmap g) (h a)             (7)     

fmap id = id

fmap id (Pure a) 
  = Pure (id a)   -- theo (1)
  = Pure a        -- theo định nghĩa hàm id

fmap id (Free ha) 
  = Free (fmap (fmap id) ha)  -- theo (2)
  = Free (fmap id ha)         -- theo (6)
 = Free fa                    -- theo (6)

fmap (f . g) = (fmap f) . (fmap g)

fmap f (fmap g) (Pure a) 
  = fmap f Pure (g a)                -- theo (1)
  = Pure(f (g a))                    -- theo (1)
  = Pure((f . g) a)                  -- theo dinh nghia ham (.)
  = fmap (f . g) (Pure a)            -- theo (1)


fmap f (fmap g) (Free ha)
  = fmap f Free(fmap (fmap g) ha)                -- theo (2)
  = Free(fmap (fmap f) (fmap (fmap g) ha))       -- theo (2)
  = Free(fmap ((fmap f) . (fmap g)) ha)          -- theo (7)
  = Free(fmap (fmap (f . g)) ha)                 -- theo (7)
  = fmap (f . g) (Free ha)

Chứng minh Free f là Monad

return a >>= k = k a

return a >>= k 
  = Pure a >>= k                    - theo (3)
  = k a                             - theo (4)

m >>= return = m

Pure a >>= return 
  = return a                       - theo (4)
  = Pure a                         - theo (3)

Free ha >>= return
  = Free (fmap (>>= return) ha)    - theo (5)
  = Free ha                        - why???? what is (>>= k) means?

(m >>= k) >>= h = m >>= (\x -> k x >>= h)

(Pure a >>= k) >>= h
  = (k a) >>= h                   - theo (4)
  = Pure a >>= (\x -> k x >>= h)  - theo (4)

(Free ha >>= k) >>= h
  = Free (fmap (>>= k) ha) >>= h            - theo (5)
  = Free (fmap (>>= h) fmap (>>= k) ha)     - theo (5)
  = Free (fmap ((>>= h) . (>>= k)) ha)      - theo rule cua fmap
  = Free (fmap (>>= (\x -> k x >>= h)) ha)
  = Free ha >>= (\x -> k x >>= h)           - theo (5)

kiennt 16-09-2016