Xóa bài viết
Bạn có chắc chắn muốn xóa bài viết này không ?
Xóa bình luận
Bạn có chắc chắn muốn xóa bình luận này không ?
Free monad
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
Bình luận

{{ comment.user.name }}
Bỏ hay
Hay

Cùng một tác giả

100
19
Mọi chuyện bắt đầu từ nắm 2013 trong quá trình xây dựng chức năng login với Facebook, tôi đã tìm ra một cách để tấn công vào các hệ thống login với...

73
5
Trong tuần vừa rồi, mình có đọc chương 7 cuốn sách (Link). Bài viết này nhằm mục đích giúp mình tổng hợp lại những kiến thức đã học được về chương ...

33
5
1. Đặt vấn đề Một trong các vấn đề của một hệ thống backend là bài toán điều phối request tới các nguồn dữ liệu. Xét bài toán với một hệ thống bl...
Bài viết liên quan

0
5
fCC: Technical Documentation Page note So I have finished the HTML part of this exercise and I want to come here to lament about the lengthy HTML ...

4
0
I used Spring boot, Hibernate few times back then at University, I'v started using it again recently. In this (Link), I want to check how Spring J...

24
1
Toán tử XOR có tính chất: + A XOR A = 0 + 0 XOR A = A Với tính chất này, có thể cài đặt bài toán sau với độ phức tạp O(N) về runtime, và với O(1)...