Just $ A sandbox

プログラミングと計算機科学とかわいさ

Lensで行こう!(2):Isoへの拡張

このエントリーはLensで行こう! - みょんさんの。の続編にあたります。

前回の復習

前回、Lens型について詳しく見ました。 Lens型は以下のような型のデータです。

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

これはFuctorを上手く定めてやれば(ConstIdentityでしたね!)getter,setterとして振る舞うことのできる素敵な型でした。

さて、この型がどれだけの力を持っているかを実感した方は、きっと「こんなややこしそうに見える型がどこから降ってきたのか?」という疑問が湧いてくると思います。 今回はこのことについて見ていくことにします。

Iso型とは?

ではLensについて考えるのに、やはりHackageを参照しましょう→The lens package

このページ真ん中に、大きな図が書いてあると思います。その図の右上と左下のあたりに、SetterとGetterがあるのが見えると思います。矢印をたどれば、(前回見たように)どちらも確かにLens型の特殊な形であることが分かります。

さてここで、LensにはIsoと書かれた箱から矢印が伸びているのが見えると思います。

そうです、実はLens型はIso型の特殊な場合に過ぎません

Lensのややこしい形がどこから降ってきたのかを知るためには、Lensの更に一般的な形であるIsoについて考える必要が出てきます。 今回はこのIsoモジュールを探検することにしましょう。

Isoについて

Control.Lens.Iso (Hackage)

例によってまずは型を調べることにします。上のリンクを開いてみると一番上に書いてあります。

type Iso s t a b = forall k f. (Isomorphic k, Functor f) => k (a -> f b) (s -> f t)

さて、以外なことにIsoはFunctorだけでは構成できません。Isomorphic型という制限がkにはかかっています。 Isomorphicの中身を見る前に、Lensについて思い出しましょう。

type Lens s t a b = forall   f.                Functor f  =>   (a -> f b) -> s -> f t
type Iso  s t a b = forall k f. (Isomorphic k, Functor f) => k (a -> f b)   (s -> f t)

非常によく似た形をしています。IsoはLensの一般的な形だったことを思い出せば、たぶん(->)がIsomorphicのインスタンスになっているんでしょうという予想が付きます。 さてIsomorphicとは以下のような型クラスです。

class Category k => Isomorphic k where
    iso :: Functor f => (s -> a) -> (b -> t) -> k (a -> f b) (s -> f t)

-- isoは以下のような性質を満たします
-- view (iso f g) ≡ f
-- view (from (iso f g)) ≡ g
-- set (iso f g) h ≡ g . h . f
-- set (from (iso f g)) h ≡ f . h . g

instance Isomorphic (->) where
  iso sa bt afb s = bt <$> afb (sa s)

予想通り、(->)がIsomorphicのインスタンスとして定義されていました。

さてここで注目していただきたいのはIsomorohicがCategoryを継承しているということです。Categoryは以下のような型クラスで、恒等函数(恒等射)と函数(射)の合成が定義されています。

class Category cat where
    id :: cat a a
    (.) :: cat b c -> cat a b -> cat a c

種明かしをしてしまえばCategory型クラスは圏を提供しています。そしてIsomorphic型クラスは同型の概念を提供します。つまり「AとBが同型である」というのをiso函数を使って定めましょう、ということです*1

Isomorphicが同型を提供するとはどういうことでしょうか。isoは以下のような型でした。

iso :: (Functor f, Isomorphic k) => (s -> a) -> (b -> t) -> k (a -> f b) (s -> f t)

上の型シグネチャは``(s -> a)と(b -> t)から{(a -> f b),(s -> f t)}の組を同型な関係kで定める"と読めます*2

つまり、k(f,g)を同型な関係と呼ぶことにすれば、それは2つの函数とファンクターがあればその間の同型な関係が定められると言っています。

言葉で表現してもわかりづらいので、図に表すことにしましょう。

b     |   [a    ->    f b]
      |
↓bt  |   ↑sa          ↓fmap bt
      |
t     |   [s    ->    f t]

ここで、sa,btは(->)のインスタンス宣言で使われている函数で、(s -> a)と(b -> t)を表しています。

図のように型a,b,s,tとファンクターfが与えられた時、saとbtの2つの函数によってk(a -> f b, s -> f t)が同型な関係kで結ばれます!これを見れば分かるように、Isomorphicは単純に型からファンクター値を作る函数が2つあればその同型を提供してくれています

同型という関係を定めるために2つの函数を並べて考えている、と見れば、いかにこのIsomorphic型クラス(と函数iso)が本質的な構造を与えるものかというのがよく分かります。

そうやって考えれば、以下の形をしたLensももう怖くないですね!

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

LensはIsomorphicの「同型な関係」を(->)のインスタンスとして与えてくれています。Isoの特殊な場合と考えることができますね。

Isoをもう少しだけ

Isoについてはもう大丈夫だと思いますので、あとほんの少しだけ応用例を見てみることにします。

  • Isoid

同じくIsoモジュール(Control.Lens.Iso)のIsoidについて。以下が定義です。

type family CoA x :: *
type family CoB x :: *

type instance CoA (a -> f_b) = a
type instance CoB (a -> f_b) = ArgOf f_b

data Isoid ab st where
  Isoid :: Isoid ab ab
  Iso   :: (CoA y -> CoA x) -> (CoB x -> CoB y) -> Isoid x y

同じ函数を2つ用意すればIsoにできる、というただそれだけですね。Isoの自明な構成例です。

enum函数は以下のように動作します。

>>> 97^.enum :: Char
'a'

これが以下のように、Isoで与えられています。

enum :: Enum a => Simple Iso Int a
enum = iso toEnum fromEnum

type Simple f s a = f s s a a

見慣れないSimpleというのがあるかと思いますが、これはLensのTypeモジュール(Control.Lens.Type)の方で提供されているもので、型をより単純に(そこまで一般化して使いたくないときに)するためのものです。

enumはPreludeで定義されたtoEnum(Int -> a)とfromEnum(a -> Int)が、片方の矢印の向きを逆にすると同型である*3という関係を保証しています。

  • Prism

最後はPrism(Control.Lens.Prism)です。

PrismはIsoの特殊化で、Setterの一般化という位置づけです。

type Prism s t a b = forall k f. (Prismatic k, Applicative f) => k (a -> f b) (s -> f t)

class Isomorphic k => Prismatic k where
  prism :: Applicative f => (b -> t) -> (s -> Either t a) -> k (a -> f b) (s -> f t)

instance Prismatic (->) where
  prism bt seta afb = either pure (fmap bt . afb) . seta

Prism型の定義を見れば、Isoとほとんど同じ形をしていることが分かります。ただ、Isomorphicの代わりにPrismatic、Functorの代わりにApplicativeが使われています。

そしてPrismatic型クラスはIsomorphicを継承しており、途中に(s -> Either t a)があります。

Eitherはここでは失敗するかもしれない文脈(そして失敗した場合にはそれを知らせるための型を別で持っている)、Maybeの一般化として使われています。

prismは同型が構成できるかどうかわからないような函数に対してそれをやってみて、上手く行けばこのような函数を、失敗すればこちらの函数を適用して返してあげるというような操作をするのに使われます。

nat :: Simple Prism Integer Natural
nat = prism toInteger $ \ i ->
    if i < 0
    then Left i
    else Right (fromInteger i)


>>> (-3,4) & both.nat *~ 2
(-3,8)

あくまで例の一つですが、上の例ではペアの値に「自然数であれば2をかけてそうでなければそのままにする」という操作を行なっています。

このようなエラー処理が、both側ではなくてnatの側の函数を調節して機能を実現させることができるというところがまさにPrismの(Isoの)魔法といったところでしょうか。

まとめ

長々と見てきましたが、今回でControl.Lensがどれだけの力を持っていて、しかもそれが本質的な概念から出発しているのかを実感していただけたかと思います。

Lensは確かに素晴らしいパッケージですが、それはあくまで使いようであって、核の部分はとても素朴なものでした。これは同型やプリズムと言った諸概念が``Functor"と結びついたときにどれだけの力を発揮するのかというよい例の1つだと思います。

Functorという概念がどれだけ豊かな構造を与えるかということは、きっとまだ誰にもわからないでしょう。でも、Functorの力を知ることはHaskellの力を知るという意味で非常に大切なことだと思います。

あなたも、ご自身の力で、Haskellの秘められた可能性を探る旅に出ませんか!

Have a good journey with Haskell magical programming!

参考文献

*1:少しだけ圏論の用語が出てきますが分からなくてもあまり関係ないと思います。気になる方はググって定義だけ確認していただければと思います

*2:日本語が怪しい気がしますが言いたいことの雰囲気を掴んでいただければ幸いです

*3:互いに双対の関係であると呼びます