살펴보는게 너무 고통스럽습니다.


아니 솔직히 말할게요


IdentityT 빼고는 하나도 성공하지 못했습니다.




이제까지 모나드 공부할때마다



1. 모나드를 통한 자연스러운 어플리카티브 도출과 실제 어플리카티브의 구현이 일치하는가


2. 어플리카티브를 통한 자연스러운 펑터 도출과 실제 펑터의 구현이 일치하는가


3. 모노이드 제약조건 하에서, 어플리카티브를 통해 도출한 자연스러운 모노이드는 어떤 형태를 가지는가


4. Foldable의 foldr 과 foldM은 서로가 서로를 자연스럽게 도출하는가 (자연스러운 도출과 실제 구현이 일치하는가)


5. Traversable 에서 Identity 어플리카티브를 주면 functor가 되는가, Constant 어플리카티브를 주면 foldMap이 되는가




를 전부 체크해서


"모나드" 라는 하나의 개념을


펑터 어플리카티브 폴더블 트래버서블 로 전부다 연결시켜서 확장시켰는데요,




심지어


이런것도 했습니다.



(f <$> m) >>= g


는


(m >>= g . f) 와 같다. (실제로 풀어서 써보면, m >>= return . f >>= g가 되고, 여기에 모나드 결합법칙을 적용해서 (\x -> (return . f) x >>= g) 를 만들면,

(\x -> return (f x) >>= g) 가 되고, 이는 모나드 레프트 아이덴티티에 의해 (\x -> g (f x)) 가 됩니다.

m >>= \x -> g ( f x) 가 m >>= g . f 가 되는것을 알 수 있죠.



라던가


이런걸 응용해서

"이렇게 도출한 타입매칭과 저렇게 도출한 타입 매칭이 모두 같은 결과물인가?"


를 많이 생각해봤었습니다.


특히, (f <$> m) >>= g 같은 경우는 IO 라던지 복잡한 모나드트랜스포머에 대해서도 적용 가능한 항등식이라서 쏠쏠하게 재미를 봤죠.



어, 이것도 자연스럽고 저것도 자연스러운데.... 어떤게 맞을까???? 하는 그 물음...



이건 자연스러운데 그냥 자연스럽게 직관화 시켜버리고 싶은데, 그 자연스러움 뒷부분에 수학적 기틀을 마련하고 싶다.

문장처럼 자연스럽게 읽히는 이 구문은 읽히기만 자연스러운게 아니라 실제로 정확한 것이다!!!!





예


서론이 너무 길어졌네요.



MaybeT 의 모나드가, Composition 에 대한 어플리카티브와 호환이 가능한지 증명에 실패했습니다.


더 풀어서 쓰자면,


Monad m => Monad (MaybeT m) 의 인스턴스를 통해서


do

x <- (MaybeT m (a -> b))

y <- (MaybeT m a)

return x y


한 대상이, (용어가 난잡한건 죄송합니다. 근데 아마 뭘 얘기중인지 아실거라 믿습니다.)


Compose 의 어플리카티브인


(<*>) <$> (MaybeT m (a -> b)) <*> (MaybeT m a)


와 일치하는지가 궁금합니다.




하......


앞으로 배우게 될 모든 모나드 트랜스포머에 대해서 이 항등식을 체크할 생각을 하니까 갈길이 굉장히 멀게만 느껴집니다