RowToListで型プログラミングをやってみた話

さいきんC#でgenericの再帰定義を使った型遊びをしていたのですが、これって型レベルプログラミングの一種なのでは？と気づいてそろそろ型レベルの概念をちゃんと覚えたくなってきたところに、@hiruberutoさんの「RowToListであそぼう！（苦悶）」というたのしい記事を見て「こんなことまでできるのか！」と興味を持ったのでぼくもRowToListで遊んでみることにしました。

propsってFFI使わないで定義できるのでは？

元記事のpropsはかなり使えそうな形をしていますが、対象がAff固定なのと、実装がJavaScriptのFFIなのが気になりました。ぼくはJavaScriptを1行も書いたことがないのでこれからも1行も書かないまま生きていたいのです。
それは置いといて、要するに{ x :: m a, y :: m b }をm { x :: a, y :: b }にできればいいわけです。この形ってなんか見覚えがあるような？sequence :: t (m a) -> m (t a)ですね。つまりRecordに対するTraversableみたいなものをつくればいいということだ！

一筋縄ではいかなかったですが、なんか、できました。
ついでにいろいろな知見を得られたので最後に書いています。

まずは全てのコードから

class RowTraversable list xs ys m f | list -> ys m where
  traverseRow :: (RLProxy list) -> (m ~> f) -> { | xs } -> f { | ys }

instance rowTraversableNil :: Applicative f => RowTraversable RL.Nil xs () m f where
  traverseRow _ _ _ = pure {}

instance rowTraversableCons ::
  ( IsSymbol key
  , Row.Cons key (m a) xs' xs
  , Row.Cons key a ys' ys
  , Row.Lacks key ys'
  , RowTraversable tail xs ys' m f
  , Applicative f
  ) => RowTraversable (RL.Cons key (m a) tail) xs ys m f where
  traverseRow _ f obj = Record.insert key <$> f (Record.get key obj) <*> traverseRow tail f obj
    where
    key = SProxy :: SProxy key
    tail = RLProxy :: RLProxy tail

sequenceRow
  :: forall rowList mr r m
  .  RL.RowToList mr rowList
  => RowTraversable rowList mr r m m
  => { | mr } -> m { | r }
sequenceRow = traverseRow (RLProxy :: RLProxy rowList) identity

props
  :: forall rowList mr r m f
  .  RL.RowToList mr rowList
  => RowTraversable rowList mr r m f
  => Parallel f m
  => { | mr } -> m { | r }
props = sequential <<< traverseRow (RLProxy :: RLProxy rowList) parallel

とりあえず解説は後にして、

使ってみる

 -- {x :: Maybe Int, y :: Maybe String } -> Maybe { x :: Int, y :: String }
> sequenceRow { x: Just 123, y: Just "abc" }
Just { x: 123, y: "abc" }

> sequenceRow { x: Just 123, y: Nothing :: Maybe String }
Nothing -- 1個でもNothingがあればNothingになる

-- Arrayの場合でも……？
> sequenceRow { x: [1, 2, 3], y: ["a", "b"] }
[{ x: 1, y: "a" },{ x: 1, y: "b" },{ x: 2, y: "a" },{ x: 2, y: "b" },{ x: 3, y: "a" },{ x: 3, y: "b" }]

propsくんは元記事と同じ動きをします。Parallelに一般化してるのでAff以外も入ります！

classの定義

class RowTraversable list xs ys m f | list -> ys m where
  traverseRow :: (RLProxy list) -> (m ~> f) -> { | xs } -> f { | ys }

listはRecordのRowList、xsとysは変換元/変換先のrow、mとfはコンテナの型です。
ふつうのtraverseはa -> m bの関数を取って全ての要素を変換できるんですが、Recordの場合はaの型が一つにならないので、代わりにm ~> fを置いてみました。わりと便利。かも。
list -> ys mはFunctional Dependenciesの定義で、型のinputとoutputを区別します。今回はlistが決まれば残りが一意に定まるという意味で、つまり、classのパラメータのうちys mは「出力変数」ってことになりますね。これを「型の関数」と見なして悪用するのが型レベルプログラミング……ということなのかしら？

インスタンスの定義

instance rowTraversableNil :: Applicative f => RowTraversable RL.Nil xs () m f where
  traverseRow _ _ _ = pure {}

instance rowTraversableCons ::
  ( IsSymbol key
  , Row.Cons key (m a) xs' xs
  , Row.Cons key a ys' ys
  , Row.Lacks key ys'
  , RowTraversable tail xs ys' m f
  , Applicative f
  ) => RowTraversable (RL.Cons key (m a) tail) xs ys m f where
  traverseRow _ f obj = Record.insert key <$> f (Record.get key obj) <*> traverseRow tail f obj
    where
    key = SProxy :: SProxy key
    tail = RLProxy :: RLProxy tail

うわーすごい。わけがわからん。一つずつ追っていきます。

再帰的定義

Nil

まずRowListはkey :: Symbolとvalue :: Typeのペアを1要素とした再帰リストとなっているので、これをRL.Consを使ったパターンマッチで型定義のところで分解しています。そうすると、再帰定義の終端があるわけで、それが、

RowTraversable RL.Nil xs () m f

です。
RL.Nilが「空のRowList」で、これにマッチしたときysが()になる、という定義です。
関数の実装は、

traverseRow _ _ _ = pure {}

で、RowListが空なんだから空のRecordを返せばよいということですね。後々このnewobjを元にRecordを構築することになります。

Cons

Cons側のインスタンス定義は、

instance rowTraversableCons ::
  ( IsSymbol key
  , Row.Cons key (m a) xs' xs
  , Row.Cons key a ys' ys
  , Row.Lacks key ys'
  , RowTraversable tail xs ys' m f
  , Applicative f
  ) => RowTraversable (RL.Cons key (m a) tail) xs ys m f

constraint多すぎてわけがわからない……一つずつ追います。

まずはIsSymbol keyですが、これはkeyがSymbolであることを表していて、Symbolを用いる関数を呼ぶために必要となる制約です。直接の仕組みには関係ないものです。

次のRow.Consについては、2つの役割があります。一つは「分解」で、Row.Cons key (m a) xs' xsの行は「xsとkeyが定まっている時に、(m a)とxs'が取り出せる」という意味になります。xs'にはxsからkeyの要素を取り除いたものが入ります。Listのパターンマッチで使う場合のconsですね。

もう一つの役割は「結合」で、Row.Cons key a ys' ysの行では結合の用途で使っています。「ys'があるときにkeyとaを渡すと、ysを取得できる」というもので、これはListを結合するときのconsに相当します。

と、ここでようやくRowListの使い道に気づいたんですが、Row.Consはあくまで「keyがあらかじめ分かっている場合」に使えるもので、rowから「keyを取り出すことはできない」のです。そこで、RowToListでrowをRowListに変換することで初めて未知のkeyを取り出すことができるようになるのです。これは便利。

次のRow.Lacks key rowは、rowに対してkeyの項目が存在しないことを保証する制約です。こちらも実装側の関数を呼ぶために必要になっています。

最後のRowTraversable tail xs ys' m fが再帰的なパターンマッチです。tailはRowListから1つ目の要素を取り出した残り(この後に書いてます)で、これをxsといっしょに渡すとys'が返ってくるということを宣言しています。マッチする度にtailが減っていくので、最終的にはRL.Nilにマッチします。そのときにys'が()となるので、そこから戻ってくるときにRow.Cons key a ys' ysで1個ずつ結合していくことになります。

そしてインスタンスの定義ですが、

RowTraversable (RL.Cons key (m a) tail) xs ys m f

これは、与えられたlistをRL.Consでその場で分解しています。ここで未知のkeyとm aを取得し、さらにkeyを取り除いた後のtailが手に入ります。すごい！定義に書かれた通り、要素の型がm aであるときだけマッチするので、この再帰定義は全てのrow要素がm なんとかであるときだけ成立します。それ以外ではコンパイルエラーになる！すごいすごい！mは定義中で固定していますが、aにはどの型が入っていても成り立ちます。

ここでいったん型変数を整理しましょう。
パターンマッチ時に最初から与えられている型はkey m a tail xsの5つです。前の4つは事前にxsから作られるlist :: RowListをRL.Consで分割するだけで得られるので、実質の型情報の大本はxsになりますね。RL.Consのパワーがすごい。ここからysの型を確定させなければなりません。
次に、RowTraversable tail xs ys' m fの制約によってtailからys' mが取得できます。わからなかったら上に書いてあるfundepの定義をもう一度見てみてください。
最後に、Row.Cons key a ys' ysの制約によってysが決まります。
これで定義に必要な型情報が手元に揃いました。

• input: key m a tail xs
• output: xs'(使用しない) ys' ys

fに関しては、traverseRowの引数によって指定されるためunknownのままで良いようです。わからない……。

ここから関数の定義ですが、

traverseRow _ f obj = Record.insert key <$> f (Record.get key obj) <*> traverseRow tail f obj
  where
  key = SProxy :: SProxy key
  tail = RLProxy :: RLProxy tail

Applicativeで大分アレな見た目ですけど、単に「tailから作ったnewobjに対して、objからRecord.getで手に入れた値をfにくぐらせて、Record.insertで挿入」というのをしているだけです。traverseRow tail f objは最終的にRL.Nilにマッチして{}を返すので、再帰の戻り際に逆順で挿入を繰り返していることになります。
SProxyはSymbolのProxy、RLProxyはRowListのProxyです。Proxyは簡単に言うと型情報を関数の引数として渡すための入れ物ですね。例えばNothing :: Maybe aを引数に渡すと、値はただのNothingですがこっそり型aの情報を渡せる、みたいなイメージです。

ここで、Record操作による構築を行っていますが、Record系の関数を扱うにはrowの挿入や要素の抽出を型安全に行うためにIsSymbolやRow.Cons、Row.Lacksによる制約を付ける必要があります。obj :: Record xsに対してRecord.getを行うためにはRow.Cons key (m a) xs' xsが必要なのはなんとなく分かるんじゃないでしょうか。そして、newobj :: Record ys'に対するRecord.insertを行うには、Row.Cons key a ys' ysに加えてRow.Lacks key ys'が必要になります。ys'にkeyが存在しない場合に限り、key aの要素をinsertできてysが得られる、という意味になります。

使える

まずは冒頭に書いたsequence :: t (m a) -> m (t a)に相当するものを作りました。

sequenceRow
  :: forall rowList mr r m
  .  RL.RowToList mr rowList
  => RowTraversable rowList mr r m m
  => { | mr } -> m { | r }
sequenceRow = traverseRow (RLProxy :: RLProxy rowList) identity

ここでようやくRowToListが出てきました。関数の引数は{ | mr }で、これは「mrのrowで構成されたRecord型」を表していて、つまり普通のRecordです。ここからmrを手に入れることができて、それをRL.RowToList mr rowListでrowListに変換しています。mrは# Typeで、rowListはRowListなので種類が違うのです。rowListが手に入ってしまえば、あとはさっき定義したRowTraversableに放り込むだけです。traverseRowの引数m ~> fは、この場合はidentityを渡します。これで、{ x :: m a, ... } -> m { x :: a, ... }という面白関数を最初から最後まで型安全で実装することができました。わーい！

props
  :: forall rowList mr r m f
  .  RL.RowToList mr rowList
  => RowTraversable rowList mr r m f
  => Parallel f m
  => { | mr } -> m { | r }
props = sequential <<< traverseRow (RLProxy :: RLProxy rowList) parallel

propsのほうは、m ~> fにparallelを渡して、まとめた後にsequentialで戻す、をやってるだけなのでほとんど一緒ですね。

くるしい

これだけを書くのに何時間意味不明なエラーメッセージを見続けたのであたまがおかしくなってしまった。
でもこれを書いてから急にRowToList系の定義が読めるようになったので得られたものは思ったより多かった。MultiParamTypeClassが型の変換ルールを記述しているというのが見えるようになったのが大きい。
型でプログラミングするときに重要なのは、「どの型があらかじめ与えられていて、どの型が計算されるものか」を見極めることだということを理解するまでに時間を掛けすぎたのだ……。

さんこう

PureScriptに関しては、@hiruberutoさんがちょう丁寧に解説してるので、記事全部読むのがいいと思います。型レベルの話だとJustin-san(@kimagure)が最先端でいつも何言ってるのか全然わからないんですけど、それ以前に英語よめないマンなのでむしろソースコード直読みがめちゃ参考になりました。purescript-simple-jsonが素晴らしい。どうかしてる。

おわり

• RowToListはrowから未知のkeyを取り出すための手段
• 「与えられた型」と「計算された型」を区別し、見極める
  • fundepの定義はinの型とoutの型を見分ける唯一の方法
• Row.Consは分解と結合の両方に用いる
• Recordを操作するにはpurescript-recordの関数を使おう
• 型安全なRecord操作をするにはRow.ConsやRow.Lacksによる正しい制約が必要
• Proxyは型の情報を渡したいけど値は別に要らないときに使うもの
  • kindの種類によってProxyとかSProxyとかRProxyとかRLProxyとかいろいろある
• 型レベルプログラミングわからない。人間の書くものじゃない。

全体のコードはここに置いてます