• Sign Up
• Login
• API
• FAQ
• Tools
• Archive
SHARE
TWEET # Untitled a guest Jul 17th, 2019 67 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. # Thinking with Types 読書会
2.
3. ## 演習 1.4-i
4.
5. >  指数法則 a^b × a^c = a^(b+c) を型を使って示せ
6.
7. ```haskell
8. to :: (b -> a, c -> a) -> Either b c -> a
9. from :: (Either b c -> a) -> (b -> a, c -> a)
10. ```
11. を作って、 `to . from = id` かつ `from . to = id` を示せば良い。
12.
13. ### 回答
14.
15. ```haskell
16. to :: (b -> a, c -> a) -> Either b c -> a
17. to (f, g) = \x -> case x of
18.     Left b -> f b
19.     Right c -> g c
20.
21. from :: (Either b c -> a) -> (b -> a, c -> a)
22. from h = (\b -> h (Left b), \c -> h (Right c))
23. ```
24. ### 証明
25.
26. 以下の `=` は束縛とかじゃなくてプログラム運算みたいなものです
27.
28. ```haskell
29. to (from h) -- f <- \b' -> h (Left b'), g <- \c' -> h (Right c') に置き換え
30. = \x -> case x of -- 二箇所とも簡約
31.     Left b -> (\b' -> h (Left b')) b
32.     Right c -> (\c' -> h (Right c')) c
33. = \x -> case x of -- x の中身にかかわらずそのまま値を h に与えているので、id …だよね？
34.     Left b -> h (Left b)
35.     Right c -> h (Right c)
36. = h
37.
38. from (to (f, g)) -- h の出現を to (f, g) に置き換え
39. = (\b -> (to (f, g)) (Left b), \c -> (to (f, g)) (Right c)) -- 二箇所とも簡約
40. = (\b -> f b, \c -> g c) -- この形はそれぞれが id
41. = (f, g)
42. ```
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!

Top