Skip to content

Instantly share code, notes, and snippets.

@matonix
Created July 5, 2019 15:15
Show Gist options
  • Save matonix/73ae8fec2ed88b8f8ec795bfd949bc86 to your computer and use it in GitHub Desktop.
Save matonix/73ae8fec2ed88b8f8ec795bfd949bc86 to your computer and use it in GitHub Desktop.

Thinking with Types 読書会

演習 1.4-i

指数法則 a^b × a^c = a^(b+c) を型を使って示せ

to :: (b -> a, c -> a) -> Either b c -> a
from :: (Either b c -> a) -> (b -> a, c -> a)

を作って、 to . from = id かつ from . to = id を示せば良い。

回答

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))

証明

以下の = は束縛とかじゃなくてプログラム運算みたいなものです

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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment