Lens와 요네다 보조 정리 (작성 예정)

Lenses, Stores 그리고 요네다 - 바르토즈 밀레프스키
Twan van Laarhoven - Talk on Lenses

렌즈의 목적을 간단히 얘기하면,
b 아래 서브 구조에 있는 a를 가져오는 것과
b 아래 서브 구조에 a를 지정하는 것으로 볼 수 있습니다.

get :: b -> a
set :: b -> a -> b

이 걸 Stroe 구조를 반환하는 하나의 함수로 표현 할 수도 있습니다.

data Store a b = Store
  { pos :: a
  , peek :: a -> b
  }

둘의 관계가 잘 드러나게 정렬해 보면

get  :: b -> a
pos  ::      a

set  :: b -> a -> b
peek ::      a -> b

get,set과 같은데, b->만 빠진 상태로 볼 수 있습니다.

여기에 Twan van Laarhoven은 완전히 다른 표현을 생각해 냈습니다.

forall g. Functor g => (a -> g a) -> g b

Store의 pos와 peek는 둘 모두 위 폴리모픽 함수로 볼 수 있습니다. Functor g =>라 했으니, 구현 어디선가 fmap을 쓴다를 선언했습니다. fmap의 서명은

fmap :: (a -> b) -> g a -> g b

입니다. Laarhoven 식 안에서 g의 fmap을 써서 g b를 만들려면, 함수 (a->b)와 a가 있어야 합니다. a에 a -> g a를 적용해서 g a를 만들고, 여기에 fmap으로 a->b를 적용해 g b를 만들 수 있습니다. Laarhoven 식의 서명만으로 (a->b),a를 가지고 있다는 걸 알 수 있습니다. (텍스트에선 이 후 복잡한 식을 쫓아가며 설명하는데, 미리 결과를 말하자면, (a -> g a) -> g b는 (a, a->b)와 Laarhoven equivalence입니다.)

어디서 본 듯한 이 패턴은 바로 요네다 보조 정리에 나오는 패턴입니다.
forall t. (a -> t) -> g t ~= g a

요네다 보조 정리를 말로 풀면 다음과 같습니다.
“어떤 폴리모픽 함수(a->t까지가 아니라 자연 변환 forall t. (a->t) -> g t)는 어떤 펑터 g의 상image에 있는 값들의 집합과 대응한다.”
서명만 봐도 a->t만 줬는데, g a가 나오려면 안에 a를 가지고 있다는 말입니다.