15/04/28 18:49:24.22 s9k+iiT5.net
>>168
何らかの多相型をMとおいたとき、f : a -> bなる関数をmapで持ち上げたmap f : M a -> M bというと、
多相性を持ったまま何らかの操作を行う関数tx : forall a. M a -> M aは可換である、ということはなんとなく分かる。
多分、証明もできる。
もっと緩い条件もあるかもしれないけど、型レベルだとこの程度しか言えないんじゃないか？
15/04/28 18:49:24.22 s9k+iiT5.net
>>168
何らかの多相型をMとおいたとき、f : a -> bなる関数をmapで持ち上げたmap f : M a -> M bというと、
多相性を持ったまま何らかの操作を行う関数tx : forall a. M a -> M aは可換である、ということはなんとなく分かる。
多分、証明もできる。
もっと緩い条件もあるかもしれないけど、型レベルだとこの程度しか言えないんじゃないか？