Advertisement
Guest User

Untitled

a guest
Jul 17th, 2019
91
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.21 KB | None | 0 0
  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. ```
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement