日記 (2019 年 4 月 29 日)

4 月 25 日 では、 lens パッケージに定義されている Lens' s a という型の意味や有用性について軽く説明しました。 今回は、 lens パッケージにある他の型について触れていこうと思います。

まず、 前回扱った Lens' s a 型ですが、 これは以下のような定義でした。

ここには (a -> f a) -> (s -> f s) という形が出てきています。 Lens' s a の定義では f に Functor であるという制約が課されていますが、 実は f にどのような制約をかけるかで、 この型は様々な意味のあるものに化けていきます。

さて、 前回説明したように、 Lens' s a 型はゲッターとセッターを合わせたような型でした。 しかし、 必ずしもゲッターとセッターが両方用意できるとは限りません。 例えば、 リストからその長さを取り出すゲッターを考えることはできますが、 リストの長さだけを設定するということは考えにくいので、 このゲッターに対応するセッターは作りにくいです。 そこで、 「ゲッターの機能だけのレンズ」 というものがあれば便利です。

ゲッターだけなわけなので、 単にゲッターを表す s -> a 型を 「ゲッターの機能だけのレンズ」 の型として採用すれば良いように思えます。 しかし、 s -> a 型と Lens' s a 型では形に互換性がないため、 例えば s -> a 型を要求する関数に Lens' s a 型の値を渡すことはできません。 ゲッターの機能だけのレンズを受け取る関数に、 ゲッターの機能も当然もつ普通のレンズが渡せない (もしくは渡すのに変換が必要になる) のは、 少し不便です。

しかし実は、 Lens' s a 型に出てくる f に対して Functor の他に Contravariant をさらに課すと、 ゲッターを表す s -> a 型と同型な型が作れます。 これは lens パッケージでは Getter s a として定義されています。

ちょっと Contravariant について触れておきましょう。 これは Functor と非常に似ている型クラスです。 Functor には fmap という関数が定義されていて、 u -> v 型の普通の関数があると、 f u -> f v 型の文脈に包まれた値を操作する関数に持ち上げることができます。 Contravariant では、 この変換後の関数の向きが逆になります。 より具体的には、 Contravariant には fmap の代わりに contramap という関数があり、 u -> v 型の関数に対して f v -> f u 型の関数を作ります。

Contravariant の例ですが、 定値関手を表す Const a がまずそうです。 Const a の fmap は実質的に全てを恒等関数に移すと実装されてるので、 向きが逆になろうとそのまま contramap の実装として使えます。

さて、 改めて Getter s a の定義を見てみましょう。 f に Functor と Contravariant の両方が課されているので、 u -> v 型の関数があると、 fmap を使って f u -> f v 型の関数も作れますし、 contramap を使って f v -> f u 型関数も作れることになります。

contramap が利用できるおかげで、 以下のように s -> a 型の普通のゲッターがあると、 Getter s a 型のレンズ版ゲッターが作れます。

すでに述べたように Const a は Functor にも Contravariant にもなるので、 逆は前と同じです。

厳密な証明は省きますが、 この 2 つの関数は互いに逆になっています。 つまり、 s -> a 型と Getter s a 型が本質的に同じものということなので、 ゲッターの型としては本質的にはどちらを使っても良いわけです。 しかし、 Getter s a の方は Lens' s a と型制約だけが異なるだけで、 型の本体は全く同じです。 このおかげで、 Getter s a 型として宣言された値を Lens' s a 型を受け取る関数にそのまま渡すことができます。 通常、 ある関数が異なる型の値を引数に受け取りたい場合は、 あらかじめ型を変換させるかその関数を多相化する必要がありますが、 違いが型制約だけになっているおかげでこの手間がありません。 画期的ですね!

ということで、 今回はゲッターのみの機能をもつレンズについて扱いました。 実際はセッターのみのレンズを扱いたいと思います。