Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- # Thinking with Types 読書会
- ## 演習 1.4-i
- > 指数法則 a^b × a^c = a^(b+c) を型を使って示せ
- ```haskell
- to :: (b -> a, c -> a) -> Either b c -> a
- from :: (Either b c -> a) -> (b -> a, c -> a)
- ```
- を作って、 `to . from = id` かつ `from . to = id` を示せば良い。
- ### 回答
- ```haskell
- to :: (b -> a, c -> a) -> Either b c -> a
- to (f, g) = \x -> case x of
- Left b -> f b
- Right c -> g c
- from :: (Either b c -> a) -> (b -> a, c -> a)
- from h = (\b -> h (Left b), \c -> h (Right c))
- ```
- ### 証明
- 以下の `=` は束縛とかじゃなくてプログラム運算みたいなものです
- ```haskell
- to (from h) -- f <- \b' -> h (Left b'), g <- \c' -> h (Right c') に置き換え
- = \x -> case x of -- 二箇所とも簡約
- Left b -> (\b' -> h (Left b')) b
- Right c -> (\c' -> h (Right c')) c
- = \x -> case x of -- x の中身にかかわらずそのまま値を h に与えているので、id …だよね?
- Left b -> h (Left b)
- Right c -> h (Right c)
- = h
- from (to (f, g)) -- h の出現を to (f, g) に置き換え
- = (\b -> (to (f, g)) (Left b), \c -> (to (f, g)) (Right c)) -- 二箇所とも簡約
- = (\b -> f b, \c -> g c) -- この形はそれぞれが id
- = (f, g)
- ```
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement