HListをOCamlで: 型クラス無しで作る異種混合リスト (heterogeneous list)

Heterogeneous Lists (HList) とは

主に静的型付きの関数型言語において、異種の型の値を型安全に格納するリストです。

• https://qiita.com/search?q=hlist
• 元のHaskell'04論文

HList を OCaml で

HListを扱うにはコンパイル時に型の上の走査が必要なため依存型か Haskell の型クラス、 Scala の implicits のような仕組み が一般には必要です。あるいは TypeScript のような型お化け型機能を使う。
HList をそのような型レベルプログラミング機能がない OCaml でどう作るか？というのがこの記事の主眼です。

この方法を使えば、型クラスのオーバーヘッドがないHListの実装ができます。ただし型パラメタの数が少し多くなる。

方針

• append は諦めます
• インデックスアクセスをする nth と、 n番目の要素を置き換える upd を実装してみます

コード

module HList = struct

  type (_,_,_,_) idx =
    | Zero : ('e1, 'e2, 'e1 * 'l, 'e2 * 'l) idx
    | Succ : ('e1, 'e2, 'l1, 'l2) idx -> ('e1, 'e2, 'e*'l1, 'e*'l2) idx

  type _ t =
    | [] : unit t
    | (::) : 'hd * 'tl t -> ('hd * 'tl) t

  let rec nth : type e1  e2 l1 l2 . l1 t -> (e1,e2,l1,l2) idx -> e1 = fun xs n ->
    match xs, n with
    | x::_, Zero -> x
    | _::xs, Succ n -> nth xs n
    | [], _ -> .

  let rec upd : type e1 e2 l1 l2. l1 t -> (e1,e2,l1,l2) idx -> e2 -> l2 t = fun xs n b ->
    match xs, n with
    | _::xs, Zero -> b::xs
    | x::xs, Succ n -> x::upd xs n b
    | [], _ -> .

end

使ってみる

open HList
let xs = [1;"3";false;7.0];;

let _0 = Zero
let _1 = Succ _0
let _2 = Succ _1
let _3 = Succ _2
let _4 = Succ _3

let x = nth xs _0
(* val x : int = 1 *)

let y = nth xs _1
(* val y : string = "3" *)

let z = nth xs _2
(* val z : bool = false *)

let w = nth xs _3
(* val w : float = 7. *)

(* 
nth xs _4;;
Line 1, characters 7-9:
Error: This expression has type
         ('a, 'b, int * (string * (bool * (float * ('a * 'c)))),
          int * (string * (bool * (float * ('b * 'c)))))
         idx
       but an expression was expected of type
         ('a, 'b, int * (string * (bool * (float * unit))), 'd) idx
       Type 'a * 'c is not compatible with type unit  
*)

解説

GADT による HList の定義

空リストを unit t, head の型が 'a, tail の型が 'b であるようなリストを ('a * 'b) t と表すことにします。OCaml では知らん間にリストのnilとコンスがオーバーライドできるようになっており、HList 自体は次のように定義できます。

type _ t =
  | [] : unit t
  | (::) : 'hd * 'tl t -> ('hd * 'tl) t

GADT の機能を使い、コンストラクタ毎に型パラメタを変えています。これを使って、

let xs = [1;"3";false;7.0];;

のような HList が自然に書けます。素敵ですね。次のような型が推論されます：

val xs : (int * (string * (bool * (float * unit)))) t =
  (::) (1, (::) ("3", (::) (false, (::) (7., []))))

まあ読めなくはない。

自然数の定義と型パラメタのハック

nth および upd のための自然数インデックスの型を定義します。これは通常、

type nat = 
  | Zero : nat
  | Succ : nat -> nat

とか定義されるものですが、このままでは数に応じて引数型が変わることが表現できません。

ここで、上の Haskell 論文の upd の型を見てみます：

class HNat n => HLookupByHNat n l e | n l -> e where 
  hLookupByHNat :: n -> l -> e
class HNat n => HUpdateAtHNat n e l l’ | n e l -> l’ where 
  hUpdateAtHNat :: n -> e -> l -> l’

fundeps を除けば、型引数は 自然数 n, 要素の型 e, 置き換え前のリスト l, 置き換え後のリスト l' からなることがわかります。

これらをnat型に型パラメタとして持たせることで、nth と upd の型付けへの道が開けます。必要な型パラメータは4つです。

型名はidx とします。 (e1,e2,l1,l2) idx で、次の2つをエンコードすることにします：

• 型 l1 の n番目の要素の型を e1 とする
• l1 の n 番目の要素の型を e2 で置き換えた型を l2 とする

そのような自然数型は次のとおりになります：

  type (_,_,_,_) idx =
    | Zero : ('e1, 'e2, 'e1 * 'l, 'e2 * 'l) idx
    | Succ : ('e1, 'e2, 'l1, 'l2) idx -> ('e1, 'e2, 'e*'l1, 'e*'l2) idx

Zero は、head の位置の要素に対する操作なので、その要素型が 'e1 とし、リストの型は 'e1 * 'l としています。'e1 を 'e2 に置き換えた型は 'e2 * 'l です。
その一方で、Succ はより深い位置にある(tailの)リストを置き換えるための ('e1, 'e2, 'l1, 'l2) idx を取り、headはそのまま 'e にするような型を持っています。

nth

型レベルの議論は上で終わっています。あとは素直に実装するだけです。

  let rec nth : type e1  e2 l1 l2 . l1 t -> (e1,e2,l1,l2) idx -> e1 = fun xs n ->
    match xs, n with
    | x::_, Zero -> x
    | _::xs, Succ n -> nth xs n
    | [], _ -> .

今の OCaml だと最後のケースを一応書く必要があるようです。 関連: OCamlでUninhabited typeを書くいくつかの方法

upd

  let rec upd : type e1 e2 l1 l2. l1 t -> (e1,e2,l1,l2) idx -> e2 -> l2 t = fun xs n b ->
    match xs, n with
    | _::xs, Zero -> b::xs
    | x::xs, Succ n -> x::upd xs n b
    | [], _ -> .

レンズ

よく見ると、 ('e1, 'e2, 'l1, 'l2) idx は put の型が多相的なレンズであり、nth は get, upd は put になっています。

由来

ガリグ先生との共著論文の最中に作っていただきました。

• プログラミング研究会発表資料 (日本語) Lightweight linearly-typed programming with
  lenses and monads
• 論文版 Journal of Information Processing Lightweight linearly-typed programming with
  lenses and monads

この論文では parameterised (indexed) monad による線形型のエンコーディングに加え、レンズで複数の線形リソースをモナドで扱えるようにしています。
上記のテクニックがどこに効いているのかというと、レンズの合成だと value restriction に引っかかって多相性が失われてしまいますが、 GADTによる表現を使えば、Succ n のようにコンストラクタの適用になるため多相性が維持されるのがポイントです。
さらにこの論文では線形型付きリストやセッション型の実装を多相ヴァリアントとppxを駆使して作っています。

余談

• 無限リストを使いたい場合には -rectypes を使うか GADT の型パラメタを多相ヴァリアントにすればできます
• レンズを使ったテクニックは、マルチパーティセッション型の OCaml 実装 にも使われており、pure OCaml でデッドロックフリー型を得るための不可欠なテクニックになっています。
  • 具体的には、MPST の全体のプロトコルを表すグローバルタイプを、個別のプロトコルを表すローカルタイプのheterogeneous listとみなし、グローバルタイプの個別のプリミティブに対する end point projection をレンズ操作として実現しています。