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

# Heterogeneous Lists (HList) とは

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

* https://qiita.com/search?q=hlist
* [元のHaskell'04論文](https://userpages.uni-koblenz.de/~laemmel/TheEagle/dl/KiselyovLS04.pdf)

# HList を OCaml で

HListを扱うにはコンパイル時に型の上の走査が必要なため依存型か Haskell の型クラス、 [Scala の implicits のような仕組み](https://qiita.com/yyu/items/4941417ec555ea5ab590#%E8%87%AA%E7%84%B6%E6%95%B0%E3%81%AE%E5%AE%9F%E8%A3%85) が一般には必要です。あるいは TypeScript のような型お化け型機能を使う。
HList をそのような**型レベルプログラミング機能がない** OCaml でどう作るか？というのがこの記事の主眼です。

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

## 方針

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

# コード

```ocaml
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
```

## 使ってみる

```ocaml
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 自体は次のように定義できます。

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

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

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

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


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

まあ読めなくはない。

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

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

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

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

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

```haskell
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` とする

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

```ocaml
  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

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

```ocaml
  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を書くいくつかの方法](https://qiita.com/dico_leque/items/ec31aae6cc43325e60f0)

## upd

```ocaml
  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](https://keigoimai.info/linocaml-paper/jpn-draft.pdf)
* 論文版 Journal of Information Processing [Lightweight linearly-typed programming with
lenses and monads](https://www.jstage.jst.go.jp/article/ipsjjip/27/0/27_431/_article/-char/ja/)

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

# 余談

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