@ailrunAilrun (UTC-5/-4) 생각해보면 return도 두 언어를 오가는 대응에 해당하네요. 모든 값을 계산으로 바꾼다는 점에서 force보다도 더 thunk의 짝이 되기 좋아보이나 싶지만 조금만 더 생각해보면 둘을 합성해서 항등 사상을 얻을 수가 없으니 아주 잘 어울리는 한 쌍은 못 되는군요. 뭔가 to의 역할을 잘 생각해보면 보이는 게 있을 거 같은데… 고민해봐야겠어요.
@ailrunAilrun (UTC-5/-4) 재밌게도 force . thunk랑 return . thunk 모두 항등 사상이 못 되네요. 이건 값이 ‘~인 것‘이기 때문일까요? ~인 것을 갖고 무언가를 더 하기 위해서 return과 to가 있는 것인가 싶어졌어요.
If you have a fediverse account, you can reply to this note from your own instance. Search https://hackers.pub/ap/notes/01963efc-0b1a-78a0-a6ac-fc7c4b41173c on your instance and reply to it.
@domatdo도막도 그 둘이 사실 수반 함자(Adjoint Functor)의 구현입니다. 강한 형 CBPV를 사용하면
thunk(-)
는 Up -
의 생성자고 return
은 Down -
의 생성자인데요, 이 두 함자 Up
과 Down
이 수반 함자 쌍을 이룹니다.
@domatdo도막도 그리고
force . thunk
는 항등사상이 맞습니다. M
은 M
이라는 계산을 하는 녀석이고, force (thunk (M))
도 정확히 M
이라는 계산을 하는 녀석이죠.