ニコニコ大百科

分離乙です

カリー化は米田埋め込みらしい

打ち消し線の多さがまさに数学ノートの趣があって良い

だいぶ迷走してるな

関数型言語やOperationalモナドの文脈で米田の補題で語るなら、Coyonedaは任意の * -> * を関手に持ちあげられるというだけなので一旦Operationalモナドを切り離して考えた方がいい

fmapの定義がこれ
fmap :: (a -> b) -> f a -> f b

で、これは下のように変形できる
fmap :: ((a -> b), f a) -> f b

つまり、a -> bとf aの組からf bを作れるものがファンクタというわけだ

ところで、Coyonedaの定義は以下だった
CoYoneda f a = (f x, x -> a)

これはx -> aとf xの組からCoyonedaを構成すると言っているのだから、Coyonedaは単にfmapを代数的データ型で表したものといえる。これが関手を実装できるのはごく当然だろう
ここから、Coyonedaのことを自由関手と呼ぶ

ここからOperationalモナドの話(つまり蛇足)

Freeモナドは任意の関手をモナドに持ちあげられるものだが、その定義は以下
Free f a where
Pure :: a -> Free f a
Join :: f (Free f a) -> Free f a

で、モナドの定義はこれ
class Monad m where
pure :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

CoyonedaとFunctorの関係と、Freeとモナドの関係は見るからにそっくりで、同様の理屈でFreeはモナドを実装する
Freeは自由モナドと呼ばれる

この二つを積み上げると、f :: * -> * からモナドを構成できるようになる
type M f = Free (Coyoneda f)

Mは自由モナドであるから、好きなようにアクション(Haskell上で、戻り値の型がm aであるような関数)を作成し、後から"実行"することができる

ここからOperationalモナドが何の役に立つのか(つまり蛇足の蛇足)

下のようにget, putというのアクションを予め用意しておいて、

data Sample a where
Get :: Sample String
Put :: String -> Sample ()
type SampleM = M Sample
get :: SampleM String
get = toM Get
put :: String -> SampleM ()
put = toM . Put

自由モナドを"実行"する時にそのアクションの振る舞いを決める(構造を"潰す")ことができる
runSampleM :: SampleM a -> IO a
runSampleM (Pure a) = pure a
runSampleM (Join (Coyoneda f Get)) = getContents >>= runSampleM . f
runSampleM (Join (Coyoneda f (Put s)) = putStrLn s >>= runSampleM . f

予めアクション(operations)を用意しておけることから、Operationalモナドと呼ばれている

>>4
分割前の記事に書き始めてから4年余り。ようやく分かっている人にめぐりあえました。
これを逃すと4年後まで誰も現れないかもしれないので、色々ご教授願えませんでしょうか。

ひとまず>>4について、以前から分からなかった点があるのですが、
1つ目:
> fmapの定義がこれ
> fmap :: (a -> b) -> f a -> f b
ということなのですが、これは関数の型を定義しているだけで、実装の定義ではないと思うのですが、実装の定義はどこにあるのでしょうか?

2つ目:
CoYoneda f a = (f x, x -> a)のxは何なんでしょうか?
記事で、CoYoneda f a x = f x -> (x -> a)として、
CoYoneda f a = x -> f x -> (x -> a)までは当時わかっていたと思うのですが、どうしても上記までつなげることが出来ませんでした。

>>7
好き勝手書いておいて返事が遅くなって申し訳ないです。

1. fmapの実装
ここでは「fmap :: (a -> b) -> f a -> f bという関数を持つ構造をファンクタと呼ぶ」ということが定義されているのであり、fmapが具体的にどのような関数であるかはそのファンクタの具体的な構造に依ります。

例えばListファンクタのfmapは「fmap :: (a -> b) -> List a -> List b」という型になり、この関数の意味するところは「a -> b」という関数を「List a -> List b」という関数に"持ち上げる"ということになります。
Listの場合、その振舞いは下のようになるのが自然でしょう。
>>> fmap (* 2) ([1,2,3])
[2,4,6]

ファンクタの数だけfmapの実装があるのであり、ファンクタに一般的なfmapの実装があるわけではありません。

2. Coyoneda f a = (f x, x -> a)のx
上のxは全称量化された型です。省略せずに書くと、
Coyoneda f a = ∀x. (f x, x -> a)
ということです。
日本語で書けば、「全てのxに対して、f xとx -> aのペアはCoyoneda f aを構成する」というような感じです。

下の二つは少し正しいとはいいがたいです。
* Coyoneda f a x = f x -> (x -> a)
* Coyoneda f a = x -> f x -> (x -> a)

前者は、全称量化のニュアンスが消えています。
後者は、余計な要素xが増えています。
後者を日本語で書くと、「全てのxに対して、xとf xとx -> aのペアはCoyoneda f aを構成する」となってしまっています。

個人的には、米田の補題についての記事を書くなら関数型プログラミングでの応用よりは圏論での米田の補題をシンプルに書くだけでもいいと思うけどな

局所的に小さな圏Cの表現可能関手Hom(A, _) -> Setsから任意の関手F:C -> Setsへの自然変換ηとFAが同型であるというだけの話だし

> この記事はモナド(プログラミング)の一部として作成された内容を元にしています。
ここ見落としてた。すまん。

理解が行き届かない質問にお答え下さりありがとうございます。もうしばらくお付き合い願えれば幸いです。

>>8-1
> ファンクタの数だけfmapの実装があるのであり、ファンクタに一般的なfmapの実装があるわけではありません。
Coyonedaを用いると、任意の型クラスfからfmapの実装が導き出せる
もしくは米田の補題の証明に出てくる何かがfmapの実装になっている
ということだと思っているのですが、
もしかして米田の補題はfに対応するfmapの「存在」を証明しているだけで、実装を導き出すことは出来ないのでしょうか。

>>8-2
> 下の二つは少し正しいとはいいがたいです。
勘違いかも知れませんが、参考にしたサイトでは唐突にこの謎変換が起きていて理解が進まなくなっていました。
>>8-1が自分の勘違いかによっても位置づけが変わってくるので、後でもう少し考えてみたいですが、今からあのサイトを読み直すのはキツい…

>>9
おっしゃる通りです。元々は米田の補題とOperationalモナドの2つの記事となる構想でした。
力尽きてしまったため未完成の記事を増やす愚を軽減すべく両者を同居させています。

俺、この記事が完成したら、故郷に帰って分割するんだ…

>>11
失礼しました、Coyoneda fのfmapの実装ですね。それでしたら、下のように実装できます。

data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)

instance Functor (Coyoneda f) where
fmap f (Coyoneda g h) = Coyoneda (f . g) h

それぞれの型を捕捉すると、
fmap :: (a -> b) -> Coyoneda f a -> Coyoneda f b
f :: a -> b
g :: x -> a
h :: f x
f . g :: x -> b

* (.)は次を満たす関数合成演算子, g(f(a)) == (g . f)(a)

圏論は筆者によって結構図や式の書き方に違いがあるので、その文脈では正しいのかもしれないですね。しかし、ここまでで用いてきたような記法とは齟齬がありそうです。

Haskellの文法が分かるのであれば、この辺なんかが参考になるかもしれません。
https://ryota-ka.hatenablog.com/entry/2018/07/03/021216

>>12
ありがとうございます。当時Scalazのソースコードまで探しに行ったのですが、分からずじまいでしたので助かりました。

と言いたいところですが、data Coyonedaの右辺にCoyondeaが出てきたり(Freeモナドみたいに再帰的?)、fって型クラス?なの関数なの?みたいに混乱しているので、1-2週間ほど考える時間を頂けませんでしょうか。

>>13
これはfmapの実装をHaskellの文法で書いているので、Haskellの文法を知らないと理解しづらいと思います。
（Coyonedaの右辺にCoyonedaが出てきたり、fが型(kindは* -> *)だったり関数だったりするのもHaskellの文法によるものなのです）
Haskell 代数的データ型　定義
Haskell 型クラス 実装
等で調べるといい記事がヒットするかもしれません。

>>12
参りました。2週間近く考えても、何を聞けばいいのかすらわからない。
とりあえず以下について確認させて下さい。

1.
> data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)
これはFreeモナドみたいな再帰的定義ということでよろしいでしょうか。

2. 関手(Functor)について
2-1:
一般に圏から圏への射と表現されますが、圏が対象と対象間の射からなる以上、
関手は「対象と射」を別の「対象と射」に変換するものということであっていますでしょうか。

2-2:
2-1のプログラミング上の実装は、
元のクラス(型)の「値」を別のクラスの「値」に変換する関数と、
「元のクラスの値を引数に取る関数」を「別のクラスの値を引数に取る関数」に変換する関数、
が合わさったものになると思っているのですが、間違っているところがありますでしょうか。

2-3:
>>12において、fmapが2-1の「変換するもの」という解釈でよろしいでしょうか。
それともクラス(型)をクラス(型)に変換するCoyoneda fが「圏から圏への変換」にあたるのでしょうか。

>>15
1. 違います。>>14 で提案した通り、Haskellの文法で代数的データ型の定義する方法を調べてください。

2-1. その通りです。
例えば、関手はF: C -> Dは、任意の対象X∈Obj(C)をF(X)∈Obj(D)に移し、任意の射f∈Mor(C)をF(f)∈Mor(D)に移します。

2-2. 少し違います。
Haskellでは型を対象、関数を射としている（Hask圏）ので、「ある型を受け取って別の型を返すもの」が関手になりうることになります。
「元のクラスの値を引数に取る関数」を「別のクラスの値を引数に取る関数」で言わんとしていることは合っているように思います。

2-3. 少し違いますかね。
2-1で示した通り、関手は対象の変換と射の変換の組です。
fmapはそのうち射の変換を行っているものです。
型を型に変換するCoyoneda fは対象の変換を行っているものです。
Coyoneda fとfmapを合わせて初めて圏から圏への変換ができる、つまり関手として成り立つということになります。

>>16
ありがとうございます。ヤクの毛刈り状態ですが、この記事や親記事でも少し触れている長年の疑問がちょっとずつですが解決しているので助かります。

1 調べて、forallは型スキーマ(型抽象)を表わし、型の世界のλである。
https://uehaj.hatenablog.com/entry/2014/01/23/121923
ということは理解していましたが、
これだけと左辺と右辺にCoyonedaが来ることを解釈できませんでした。

他の代数的データ型の解説はたいてい列挙型・直積型・直和型くらいで終わっており、
https://qiita.com/7shi/items/1ce76bde464b4a55c143
やはり左辺と右辺に同じものが来るのは、再帰的定義と解釈せざるを得なかったです。

2-2
> Haskellでは型を対象
値が対象でないというのは目から鱗かも。

あれ? ということは、Functorは元のクラス(型)の「値(オブジェクト指向でいうところのインスタンス)」を
別のクラスの「値」に変換する関数を提供しないということでしょうか。

>>17
1.
CoyonedaはHaskell上では直積型で表されていますので、参考にされた記事の上記記事の直積型の構文と例を見てください。
https://qiita.com/7shi/items/1ce76bde464b4a55c143#%E7%9B%B4%E7%A9%8D%E5%9E%8B

> data 型 = コンストラクタ [フィールドの型 ...]
>
> data Point = Point Int Int deriving Show

ここで、右辺に現れるPointはコンストラクタです。同様に、
data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)
という定義の右辺に出てくるCoyonedaはフィールドの型ではなくコンストラクタであり、再帰的定義ではありません。

2-2.
はい、その通りです。
>元のクラス(型)の「値(オブジェクト指向でいうところのインスタンス)」を別のクラスの「値」に変換する関数
というのは、型で表すと a -> f a というような関数になりますが、これはHaskellでいうApplicativeのpure（= Monadのreturn）が担っている機能です。

余談ですが、代数的データ型を定義するときの左辺を「型コンストラクタ」右辺を「値コンストラクタ」と言ったりします。

下のような直積型は、

data A a = A a a

例えばJavaで書くと次のような定義になりますが、

> class A<T> {
> public A(T a, T b) {
> this.a = a;
> this.b = b;
> }
> public T a;
> public T b;
> }

型宣言のA a（A<T>）は「型を1つ受け取って型を作るもの」、コンストラクタAは「値を2つ受け取って値を作るもの」とみなせます。

ここで、型コンストラクタはAは型aを型A aに変換するものと言えるので、これが関手の対象の変換に相当するものとなるわけです。

理解の助けになればと思います。

>>18
1. ありがとうございました。少し理解が進みました。
こういう>>17のforallと直積型を組み合わせた解釈というのは、知っている人にはそのようにしか見えないものですが、知らない自分にはそれ以外の組み合わせによる解釈も同等の確からしさを持っているように見えるので、考えが及びませんでした。申し訳ございません。

2. 誤解していた点が判明してすっきりしました。まだまだわからないところも多いですが、また1-2週間考えてみたいと思います。

何度もお手数をおかけして申し訳ございません。
>>12
data Coyoneda f a = forall x. Coyoneda (x -> a) (f x)について
左辺は左結合((Coyoneda f) a)で型クラスfがCoyonedaの型引数になっているのに対し、
右辺の(f x)はfがxを型引数にしているという解釈であっていますでしょうか。

昔Haskellの文法を勉強したことはあるのですが、このように結合方向とかで、fが引数になったり、引数をとる側に回ったりというのが、文法に精通していないと読むことすらできないので、いまだに馴染めずにいます。

ただfを型クラスと考えると、fmapが型クラスを引数に取る関数ということになって、関数と呼んでいいものかわからなくなってしまうのですが、

instance Functor (Coyoneda f) where
fmap f (Coyoneda g h) = Coyoneda (f . g) h
の1行目のfと2行目の左辺と2行目の右辺のf、及び代数データ型の定義の左辺で出てきたfは同じものを指している(同じ型クラスをあてはめられる?)ということであっていますでしょうか。

>>21
左辺 data Coyoneda f a は、
型fと型aを引数に取るCoyonedaという型を宣言するという意味です。
右辺 forall x. Coyoneda (x -> a) (f x) は、左辺で宣言したCoyoneda f aの定義がこの通りであるという意味で、f xの解釈は仰る通りです。

そうですね、Haskellは独特の文法を持っていて、慣れるまで読みづらい言語ではあると思います。ただ、米田の補題をHaskellの文脈で理解したいというのであれば、Haskellの文法を勉強は避けられないと思います。このレスを含め、私の解説はほぼHaskellの文法解説になってきているわけですし。
せっかく実際に動くコードなのですから、動かして遊んでみたら理解も深まるのではないでしょうか。

https://ideone.com/l1sh9Q

fは型クラスではく、高階型と呼ばれるものです。
Haskellの型には、カインド（kind, 種）という、型の型とも呼べるものがあります。
明示的に書くとf :: * -> *、 a :: * となり、fは「カインド*の型を受け取ってカインド*の型になるような型」というわけです。

> instance Functor (Coyoneda f) where
> fmap f (Coyoneda g h) = Coyoneda (f . g) h
> の1行目のfと2行目の左辺と2行目の右辺のf、及び代数データ型の定義の左辺で出てきたfは同じものを指している(同じ型クラスをあてはめられる?)ということであっていますでしょうか。
いいえ、合っていません。
一行目のfは、代数的データ型の定義の左辺のfにこのfを割り当てているということです。
Functorはカインド* -> *を持つ型しかインスタンスに取れません。CoyonedaはCoyoneda :: (* -> *) -> * -> *というカインドを持つため、fを当てはめてやるとCoyoneda f :: * -> *となってFunctorのインスタンスに取れるようになるということです。

二行目のfは、単にfmapの第一引数の仮引数名です。

>>22
> 米田の補題をHaskellの文脈で理解したい
親記事の過去リビジョンに書いていますが、プログラミング言語や圏論の記号を使わずに説明することを目指したいというのが、当記事の元になった記事のコンセプトでした。

色々引き止めて申し訳ございませんでした。何年も誤解したままだったものが、いくらかでも解消できたのは>>22のおかげです。ありがとうございました。

もし気が向きましたら、たまには巡回していただけましたら幸いです。

個人的に米田の補題を調べていてここにたどり着いたのですが、具体的な使い方がある程度わかったほうが全体像が把握しやすいということもあると思うので、自分としてはいきなりOperationalモナドから入るのもありなのではないかと思います。

そうは言っても結局米田の補題の理解が問題になるわけですが…
仕組みとしては、自分はhttps://its-out-of-tune.hatenadiary.org/entry/20130601/1370109743の解説が一番わかりやすかったのですが、おそらく理論として重要なのはHom(A,-)からの変換とF(A)の組が一対一に対応する(どちらかが重複したりしない)という点なのかなと思います。

正直自分もよく分かってない

だいぶいい加減ですが加筆してみました。
間違ってるところがあったらすいません。

構造や中身に関していくつか書かせていただきます。

1.「概要」は全体的に意味が不明瞭です。ただ説明方法の代案は思いついておらず申し訳ないです。
2.「Operationalモナド」について。ここで主に書かれているのはCoyonedaについてであるため名前を変更した方が良さそうです。
また、米田の補題とHaskellでCoyonedaと呼ばれているものは、co-Yoneda lemmaで繋がっているわけですが、そのあたりがわかりにくいのでhttps://ncatlab.org/nlab/show/co-Yoneda+lemma あたりの中身を可能なら盛り込みたい気持ちになりました。(多分相当難しいですが)
3. 「ファンクター・アプリカティブ」は米田の補題との関連性がはっきりしない気がします。「関手」の記事とマージしてよさそうです。

自分でこのページを書き直すとしたら、HaskellのCoyonedaには触れたいですが、Operationalモナドは自由モナド寄りという気がするので、「Freeモナド」に移動して、ここでは軽く触れるくらいにしたいですね。

>>26
1. 概要は自分でなく>>25の手によるものを概要に格上げしたものなので>>25とご相談下さい。
2.,3. 自分の記述は必ずしも残さなくて結構です。だた、>>23で述べたように米田の補題, Co-Yoneda, ファンクター・アプリカティブ等をプログラミング言語や圏論の記号を使わずに説明することを目指すという主旨の記事だったので、その点は引き継いで頂ければとは思います。

>>27
1. 承知しました。
2.,3. すでにHaskellの記法を使用していますし、また少なくともカリー化に触れずに説明するのは不可能だと思うので、プログラミング言語の記号を使わないのは無理だと思っています。圏論の記号はなるべく使わないようにしたいですが…。

>>28
> すでにHaskellの記法を使用しています
その通りですが、一応極力避けて、使う時も非Haskellユーザー向けに説明してから使うようにしていました(親記事や兄弟記事で説明していたという昔の記憶)。
Haskellや圏論を事前に知っていないと意味不明、という事態は避けたいところです。

>>26
概要部分を書いたものですが、内容は自分の備忘録程度なので全面的に書き換えていただいて構いません。
といっても自分自身よくわかっていないので、自分もあんまりいい案は思い浮かばないのですが…