[additional] Functor 의 제 1법칙만 성립해도 Functor 가 된다?!

[leejaeseung]

연관 챕터

17

조사 내용

p.170 에 Functor 가 되기 위한 2 가지 조건이 나옵니다.

1. 부수효과가 없어야 한다.
2. 합성이 가능해야 한다.

이는 다른 책에서 아래와 같이 설명합니다.

1. 부수효과가 없어야 한다. fmap(identity()) == identity() 즉, fmap 에 identity 를 적용한 것과 identity 가 같다.
2. 합성이 가능해야 한다. fmap(f * g) == fmap(f) * fmap(g) 즉, 개별적으로 합성한 것과 합성 후 fmap 한게 동일하다.

여러 책들에서 위 두 가지 조건을 모두 만족하는 fmap 은 Functor 라고 정의할 수 있다고 합니다. 하지만 Functor 의 제 1 법칙을 만족한다면 제 2법칙은 항상 만족함을 증명한다는 글이 있어 정리해 봅니다.

[leejaeseung]

아래 내용은 이 글을 정리한 내용입니다.

Free theorem (자유 정리)

g . h == k . f

라면

$map g . fmap h == fmap k . $map f

이다. ($map 은 타입 생성자 F 의 기본 map)

$map

map :: (a -> b) -> [a] -> [b]

---

기본식 1

fmap id == id

라면

fmap f == $map f

이다.

---

증명

fmap f
= {- by $map id = id -}
$map id . fmap f
= {- by free theorem, using g = k = id, h = f -}
fmap id . $map f
= {- by fmap id = id -}
$map f

---

1. fmap f == id . fmap f (id 는 자기 자신이니까 어디든 붙을 수 있으니?)
2. id . fmap f == $map id . fmap f ($map id = id 에 의해)
3. $map id . fmap f == fmap id . $map f (g = k = id , h = f 로 가정하면, free theorem 에 의해 성립한다.)
4. 위처럼 가정한다면 id . f == id . f 이면 $map id . fmap f == fmap id . $map f
5. fmap id == id 이므로 fmap f == id . $map f
6. 따라서, fmap f == $map f
7. 그러면 fmap id == id 라면 fmap 과 $map 은 동일하다!

기본식 2

f . g == id . (f . g)

---

가정 2

fmap id == id

라면

fmap f . fmap g == fmap (f . g)

이다.

---

증명

fmap f . fmap g
= {- by lemma 1, fmap f = $map f -}
$map f . fmap g
= {- by the free theorem for fmap using lemma 2 for the precondition -}
fmap id . $map (f . g)
= {- by fmap id = id -}
$map (f . g)
= {- by fmap _ = $map _ -}
fmap (f . g)

---

1. 기본식 1 에 의해, fmap f . fmap g == $map f . fmap g 이다.
2. 자유 정리에서 g 를 f , h 를 g , k 를 id , h 를 (f . g) 라고 한다면
3. f . g == id . (f . g) 라면 ⇒ $map f . fmap g == fmap id . $map(f . g) 이다. (위 2, 3 번째 식)
4. fmap id 는 id 와 같고, 소거할 수 있다.
5. $map _ 은 fmap _ 로 치환할 수 있다. (기본식 1)
6. 따라서, fmap f . fmap g == fmap(f . g)

[ABizCho]

@leejaeseung ........ 쉽지 않네요...