続・OCamlでもLensしたい2020

この記事は ML Advent Calendar 2020 24日目の記事です。

OCamlでもLensしたい2020 - Qiita の続編です。

前置き

OCamlでもLensしたい2020 - Qiita では、 OCaml でも Lens と Prism を統一的に扱える方法を紹介した。

ただ、この方法では Optics の階層構造（例えば optics/optics.png とかみたいな）は無視しており、「Prism は Getter の部分型でないので get はできない」のようなことは表現できていなかった。

この記事では、幽霊型をつかって Optics の部分型関係を表現することを試みる¹。

実装

実装側は型定義以外同じなので、インタフェースのみを示す。

まず、部分型関係を表現するための型を定義する。たまには OCaml の O を使う。

optic.mli

class type a_setter = object
  method setter : unit
end

class type a_getter = object
  method getter : unit
end

class type a_lens = object
  inherit a_getter
  inherit a_setter
  method lens : unit
end

class type a_prism = object
  inherit a_setter
  method prism : unit
end

class type an_iso = object
  inherit a_prism
  inherit a_lens
  method iso : unit
end

a_setter, a_getter, a_lens, a_prism, an_iso が Optics の階層構造に対応するクラス型だ。この型は目印としてしか使わないので、各クラスで自分自身を表すメソッドをひとつずつ追加していくだけだ（型も何でもいいので unit にしておく）。

optic.mli

type (+'k, -'s, +'t, +'a, -'b) _t =
  { op : 'r. ('a -> ('b -> 'r) -> 'r) -> ('s -> ('t -> 'r) -> 'r) }

type (+'k, -'s, +'t, +'a, -'b) t = unit -> ('k, 's, 't, 'a, 'b) _t

_t に型パラメーター 'k を追加し、さきほど定義した型を使うような感じにしていく。共変にしたいので型パラメーターには + をつけておく。幽霊型なので 'k は _t の右辺には現れない。

optic.mli

type (-'s, +'t, +'a, -'b) setter = (a_setter, 's, 't, 'a, 'b) t
type (-'s, +'t, +'a, -'b) getter = (a_getter, 's, 't, 'a, 'b) t
type (-'s, +'t, +'a, -'b) lens = (a_lens, 's, 't, 'a, 'b) t
type (-'s, +'t, +'a, -'b) prism = (a_prism, 's, 't, 'a, 'b) t
type (-'s, +'t, +'a, -'b) iso = (an_iso, 's, 't, 'a, 'b) t

val lens   : ('s -> 'a) -> ('s -> 'b -> 't) -> (a_lens, 's, 't, 'a, 'b) _t

val prism  : ('b -> 't) -> ('s -> ('a, 't) Result.t) -> (a_prism, 's, 't, 'a, 'b) _t
val prism' : ('b -> 's) -> ('s ->       'a Option.t) -> (a_prism, 's, 's, 'a, 'b) _t

'k を固定した型を定義したり、ユーティリティに型パラメーターを追加したりしていく。

optic.mli

val (//) :
  ('k, 'a, 'b, 'c, 'd) t
  -> ('k, 'c, 'd, 'e, 'f) t
  -> ('k, 'a, 'b, 'e, 'f) t

合成はとりあえず同じ種類のものだけ合成できるようにしておく。

optic.mli

val id : ('s, 'a, 's, 'a) iso

val _1 : ('a * 'x, 'b * 'x, 'a, 'b) lens
val _2 : ('x * 'a, 'x * 'b, 'a, 'b) lens

val _Ok    : (('a, 'x) Result.t, ('b, 'x) Result.t, 'a, 'b) prism
val _Error : (('x, 'a) Result.t, ('x, 'b) Result.t, 'a, 'b) prism

val _Some : ('a Option.t, 'b Option.t, 'a, 'b) prism

インスタンスの型もいい感じに。

optic.mli

val over : (#a_setter, 's, 't, 'a, 'b) t -> ('a -> 'b) -> ('s -> 't)
val set : (#a_setter, 's, 't, 'a, 'b) t -> 'b -> 's -> 't
val get : (#a_getter, 's, 't, 'a, 'b) t -> 's -> 'a
val (.%[]<-) : 's -> (#a_setter, 's, 't, 'a, 'b) t -> 'b -> 't
val (.%[]) : 's -> (#a_getter, 's, 't, 'a, 'b) t -> 'a

over や get たちは特定の Optics の部分型でだけ実行できるような型にしておく。 #-型を使うのがポイントだ。

使ってみる

# #load "optic.cmo";;

# open Optic;;

# get _1 (1, 3.14);;
- : int = 1

# get (_2 // _1) (1, (3.14, "foo"));;
- : float = 3.14

# set (_2 // _1) 1.414 (1, (3.14, "foo"));;
- : int * (float * string) = (1, (1.414, "foo"))

Lens は get も set もできるし、 Lens 同士で合成もできる。

# set _Some "foo" (Some 0);;
- : string option = Option.Some "foo"

# set _Some "foo" None;;
- : string option = Option.None

# set (_Some // _Some) 42 (Some (Some 0));;
- : int option option = Option.Some (Option.Some 42)

Prism は set できるし、Prism 同士の合成もできる。

# get _Some None;;
Line 1, characters 4-9:
Error: This expression has type
         (a_prism, 'a option, 'b option, 'a, 'b) t =
           unit -> (a_prism, 'a option, 'b option, 'a, 'b) M._t
       but an expression was expected of type
         (#a_getter as 'c, 'd, 'e, 'f, 'g) t =
           unit -> ('c, 'd, 'e, 'f, 'g) M._t
       Type a_prism = < prism : unit; setter : unit >
       is not compatible with type 'c = < getter : unit; .. > 
       The first object type has no method getter

Prism の get はできない。

ここまではよさそうだ。

が、 Lens と Prism を合成しようとすると面倒になる。

# _1 // _Some;;
Line 1, characters 6-11:
Error: This expression has type
         (a_prism, 'a option, 'b option, 'a, 'b) t =
           unit -> (a_prism, 'a option, 'b option, 'a, 'b) M._t
       but an expression was expected of type
         (a_lens, 'c, 'd, 'e, 'f) t = unit -> (a_lens, 'c, 'd, 'e, 'f) M._t
       Type a_prism = < prism : unit; setter : unit >
       is not compatible with type
         a_lens = < getter : unit; lens : unit; setter : unit > 
       The second object type has no method prism

OCaml では Subtyping is never implicit. なので頑張って型強制しないといけない。

# (_1 :> _ setter) // (_Some :> _ setter);;
- : (a_setter, '_weak1 option * '_weak2, '_weak3 option * '_weak2, '_weak1,
     '_weak3)
    t
= <fun>

# set ((_1 :> _ setter) // (_Some :> _ setter)) 3.14 (Some 42, "foo");;
- : float option * string = (Option.Some 3.14, "foo")

うーん……。

# let setter x = (x : (#a_setter, _, _, _, _) t :> _ setter);;
val setter : (#a_setter, 'a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) setter = <fun>

# set (setter _1 // setter _Some) 3.14 (Some 42, "foo");;
- : float option * string = (Option.Some 3.14, "foo")

うーむ……。

追記：型強制必要なかった

2022-11-14追記：型強制が必要になるのは、 _1 等の型が ('a * 'x, 'b * 'x, 'a, 'b) lens = (a_lens, 'a * 'x, 'b * 'x, 'a, 'b) t のように幽霊型部分（t の 'k 部分）が閉じたオブジェクト型になっているのが原因だった。多相バリアントを使って列変数を導入してやればうまく単一化されるようになり型強制は必要なくなる（オブジェクトでもできそうな気がするのだけどやり方がわからなかった）。

参考：幽霊型による部分型付けの紹介

# set (_1 // _Some) 3.14 (Some 42, "foo");;
- : float option * string = (Option.Some 3.14, "foo")

# _1 // _Some;;
- : (_[< `Setter ], '_weak6 option * '_weak7, '_weak8 option * '_weak7,
     '_weak6, '_weak8)
    t
= <fun>

# get _Some None;;
Error: This expression has type
         ([< prism ] as 'a, 'b option, 'c option, 'b, 'c) t =
           unit -> ('a, 'b option, 'c option, 'b, 'c) Optic._t
       but an expression was expected of type
         ([> getter ] as 'd, 'e, 'f, 'g, 'h) t =
           unit -> ('d, 'e, 'f, 'g, 'h) Optic._t
       Type 'a = [< `Prism | `Setter ] is not compatible with type
         'd = [> `Getter ]
       The first variant type does not allow tag(s) `Getter

# get _1;;
- : '_weak9 * '_weak10 -> '_weak9 = <fun>

# get (_1 // _Some);;
Error: This expression has type
         ([< `Setter ] as 'a, 'b option * 'c, 'd option * 'c, 'b, 'd) t =
           unit -> ('a, 'b option * 'c, 'd option * 'c, 'b, 'd) Optic._t
       but an expression was expected of type
         ([> getter ] as 'e, 'f, 'g, 'h, 'i) t =
           unit -> ('e, 'f, 'g, 'h, 'i) Optic._t
       Type [< `Setter ] as 'a is not compatible with type 'e = [> `Getter ] 
       Types for tag `Getter are incompatible

インタフェース定義は下記のようになる（'k を固定した別名を定義するのをやめたので、幽霊型用の型に接頭辞をつけるのはやめた）。

type setter = [`Setter]
type getter = [`Getter]
type lens = [setter|getter|`Lens]
type prism = [setter|`Prism]
type iso = [lens|prism|`Iso]

type ('k, -'s, +'t, +'a, -'b) _t
type ('k, -'s, +'t, +'a, -'b) t = unit -> ('k, 's, 't, 'a, 'b) _t

val lens   : ('s -> 'a) -> ('s -> 'b -> 't) -> ([< lens], 's, 't, 'a, 'b) _t

val prism  : ('b -> 't) -> ('s -> ('a, 't) Result.t) -> ([< prism], 's, 't, 'a, 'b) _t
val prism' : ('b -> 's) -> ('s ->       'a Option.t) -> ([< prism], 's, 's, 'a, 'b) _t

val (//) : ('k, 'a, 'b, 'c, 'd) t -> ('k, 'c, 'd, 'e, 'f) t -> ('k, 'a, 'b, 'e, 'f) t

val id : ([< iso], 's, 'a, 's, 'a) t

val _1 : ([< lens], 'a * 'x, 'b * 'x, 'a, 'b) t
val _2 : ([< lens], 'x * 'a, 'x * 'b, 'a, 'b) t

val _Ok    : ([< prism], ('a, 'x) Result.t, ('b, 'x) Result.t, 'a, 'b) t
val _Error : ([< prism], ('x, 'a) Result.t, ('x, 'b) Result.t, 'a, 'b) t

val _Some : ([< prism], 'a Option.t, 'b Option.t, 'a, 'b) t

val over : ([> setter], 's, 't, 'a, 'b) t -> ('a -> 'b) -> ('s -> 't)
val set : ([> setter], 's, 't, 'a, 'b) t -> 'b -> 's -> 't
val get : ([> getter], 's, 't, 'a, 'b) t -> 's -> 'a
val (.%[]<-) : 's -> ([> setter], 's, 't, 'a, 'b) t -> 'b -> 't
val (.%[]) : 's -> ([> getter], 's, 't, 'a, 'b) t -> 'a

1. ちなみに Haskell の optics ライブラリは GHC 拡張をごりごりつかって部分型関係や、型の最小上界を求めたりしている。 ↩