Leanのモナド たぶん続きがある

  1. クラスBindは、">>=" または bind を持っている構造のクラス。
  2. クラスPureは、pure を持っている構造のクラス。
  3. クラスFunctorは、map を持っている構造のクラス。mapしてから適用するのを <$> で表す??
  4. 型クラスのベース〈パラメータ〉は型関数=総称型だが、異なる型宇宙のあいだの型関数でもよい。関手に関しては確かに異なる宇宙に意味がある。
  5. クラスSeqは、seq または "<*>" を持っている構造。
  6. クラスSeqLeftは、seqLeftまたは "<*" を持っている構造。左作用積かな?
  7. クラスSeqRightは、seqRightまたは "*>" を持っている構造。右作用積かな?
  8. Applicativeは extends Functor , Pure , Seq , SeqLeft , SeqRight となっている。
  9. 「定数」とは、終対象からの射の形のアロー型の要素を意味している。圏のポイントの型理論的にエンコードしたもの。c : Unit → α

The seq operator gives a notion of evaluation order to the effects とのこと。


説明で“独特な曖昧な言い回し”をしていて、圏論とは違う用語法なので、僕にはかえって分かりにくい。解釈にコストがかかってちょっとイラッとする。

説明で、「コンテナ」と言っているが、List/Bag などのコレクション型を (F α) と書いたとき、これを α から定義されたコンテナ型と言っているんだろう。αの要素をunderlying valueと言っている。「台値」にするか。αはコンテナ型(=関手の値)の台型〈underlying type〉。

inside the container は、「→ (F α)」みたいな状態かな? 「関数をmapする」は、関手の射パートを適用すること。単にmapするだけでなくて、それを適用することが大事で、(F.map f) x のような演算を重視しているようだ。モナドのバインドも拡張してから適用してるし。適用をずっと引きずるのね。そこが僕の発想とズレる。

(F.map f) x が構文的メカニズムで (x.map f) と書ける。まー、これは便利。型の要素がメソッドを持つときはオブジェクトと呼んでいるのかな? メソッドはドット記法で呼び出せる関数。ドット記法は名前空間の補完を使っている。値 x から型推論してから型クラス解決してメソッド呼び出しを実現している。中身はけっこう複雑。

「List α 型は、mapメソッドを持つ」ので「List α 型の値〈要素〉はmapメソッドをドット記法で呼べる」、したがって、メソッド適用可能な要素だから「オブジェクト」である。となる。

「要素にメソッド適用できる」はよくよく考えたほうがよい。

"List has a specialized version of map" -- map は多相関数〈総称関数〉で、その具体化としてリストのmapがある。リストのmapはList名前空間に入るが、List名前空間は、List再帰型の定義時に自動生成される。

文字列もオブジェクトで、s.capitalize などが使える。文字列は文字列クラスの要素で、文字列クラスは構造(型+α)だが、型クラスではない! 型名と名前空間名を同じにすることによりOO風クラスを実現している。

「型が関手である」とは、どういう意味? 単一の型のことではなくて「リスト型」とか「オプション型」とかの型パラメータを持つ型、つまり「総称型」を「型」と略称している。で、「総称型が関手」とは、総称型=型関数が、関手型クラスのインスタンスになっている。もっとちゃんというと、ある定義環境下で、その総称型が関手まで増強可能。Leanのメカニズムだと、型クラス=相対指標の増強は一意である必要はない。「自然数{の集合}?はモノイドである」で、どんなモノイドかは一意に決まらない。