「関数の型から実装が自動的に決まる」で理解する米田の補題

圏論の米田の補題を Haskell で考えてみるとすごく直感的に理解できる、なんなら当たり前に思える、というアイデアを知って感動したので、興奮しているうちに紹介したいと思います。 型が a -> a な関数は id しかない、という話から2ステップで米田の補題に辿り着きます。 f :: a -> a な関数はどれだけあるか Haskell で関数を書いていると、型から実装が自動的に決まることがあるのを感じると思います。たとえば次のような型の関数を考えます。 これを実装する人の立場で考えます。まず返り値の型から読むと 「指定された型 a の値を必ず何か返しなさい」 となります。次に引数の型を読むと 「ただし、型 a の値 x が渡されます」 となります。 この関数では、型 a の値を返す必要があります。そしてそのためには渡された引数 x を使うほかに手段がありません。また型 a については事

[paradoxparanoic]

チャッピーに聞いてようやく理解した。 α (β f) = α (f id) = \g -> fmap g (f id) あたりが難しかった

[SWIMATH2]

かなりわかりやすかった