SATySFiでad hoc多相

# SATySFiでad hoc多相

[SATySFi](https://github.com/gfngfn/SATySFi)は現代的な設計に基づく組版処理システムです．
組版を行うバックエンドへ指示が関数型プログラミングで行えることが最大の特徴です．
言語としてはOCamlやSMLに近い構文を持ち，少しでもML系の言語とかHaskellに触ったことがある人なら特に苦労することなく高度な組版処理をプログラムすることができると思います．
実際私は技術書典の記事をSATySFiで記述していますがレイアウトに不満がある時などにささっと自分の手で変更できる(すくなくともそれに抵抗をあまり感じない)のは大きな魅力だと思います．(LaTeXを使う時はひたすらStack Exchangeで自分と同じようなハマり方をしてる人を探すガチャをしています．虚無．)

ただし，あくまで組版処理がメインのため，プログラミング言語単体で見るとまだまだ不便なところもあります．たとえばSATySFiにはMLライクなモジュールシステムがありますがfunctorがありません．またHaskellライクな型クラスもありません．そのためad hoc多相的なことができず，同じような見た目だけど少し違うコードを頻繁に書かなければならないことが多いです．SATySFiの型システムは基本的には教科書的なML式の型システム + 組版用の機能が実装されているのみなので，この制限は今後SATySFiに言語拡張が入らない限りはどうしようもないかなと思っていました．しかし昨日たまたまType-Indexed Value (TIV)なる概念を知りこれがSATySFiにも応用できることに気づきました．TIVを用いるとSATySFiでもad hoc多相(っぽいこと)ができるようになります．この記事ではSATySFiでTIVをやるための方法についてざっと解説します．

(TIVを教えてくれた@eldesh先生(の本)に感謝 :pray: )

# 結局何ができるのか

ad hoc多相でよく使われる例として`show`があります．
Haskellでは`Show`型クラスとして実装されているものです．
これはさまざまの型の値を文字列型に変換します．
受け取った値を文字列に変換する方法がなければ型検査時にエラーになります．
今回実装するTIVを使うと例えば以下のようなコードで`show`を実現することができます．

```
% register methods
Show.register int String.of-int
Show.register string Fn.id

% use methods
Show.apply int 42        % => `42`
Show.apply string `foo`  % => `foo`
Show.apply string 3      % => type error
```

ここで，`int`や`string`は`Type.t`という型の値です．(正確には`int Type.t`のように適切な型パラメータをとります．)
それぞれの型に対してどのように文字列化を行うかを指定するのが`Show.register`です．
`int`型の時は通常の10進のアラビア数字の表示によって文字列化を行い，`string`型の時はその値をそのまま返す，というルールにしています．
実際に文字列化を行うときは`Show.apply`を使います．`Show.apply`は文字列化を行う際に値そのものに加えてその値の型(を表す値)を受け取ります．この際，一番下の行のように値とその型(を表す値)にミスマッチがあれば型エラーになります．そのようなミスマッチがなければ型検査に通り，行末コメントで示してあるように整数値や文字列がさきほど指定したやり方で正しく文字列化されます．

今回のように型を明示的に渡さなければいけないのはどうしても外せない制限です．今後SATySFiにimplicit valueのような機能が追加されれば上のコード中の`int`や`string`は書かなくても良くなります．あと，ここでは`list int`の文字列化などは例として挙げていません．一応`list`の文字列化も可能なのですが話がややこしくなるので載せていません．あと，ここで`String.of-int`や`Fn.id`はSATySFiの標準ライブラリには存在しない関数ですが，これらは拙作のライブラリである[satysfi-lib](https://github.com/nyuichi/satysfi-lib)に実装されているものです．このライブラリはSATySFiで**もっと**関数型プログラミングしようという意図で作っているものです．普通に便利なので是非使ってみてください．

# 準備

TIVをするにはいくつか準備が必要です．関数型言語の上で変なことをするのに慣れている人(GHC拡張とかが好きな人)には追っかけるのは難しくないと思います．

まず，`PIso`というモジュールを用意します．
`PIso`はpartial isoの気持ちで，`'a 'b PIso.t`は型`'a`と型`'b`の間に部分単射があることを表します．部分単射はドメインとコドメインを入れ替えても部分単射なことに注意してください．ここではそれぞれの向きの部分単射を`inject`と`project`と呼んでいます．

先ほども言及しましたがSATySFiにはfunctorがないのでモジュールはただの名前空間以上の機能を持ちません．ここでわざわざモジュールにしているのは単に名前をわかりやすくするためです．

```
module PIso : sig
  type 'a 'b t
  val make : ('a -> 'b) -> ('b -> 'a) -> 'a 'b t
  val inject : 'a 'b t -> 'a -> 'b
  val project : 'a 'b t -> 'b -> 'a
end = struct
  type 'a 'b t = T of ('a -> 'b) * ('b -> 'a)
  let make i p = T (i, p)
  let inject (T (i, _)) = i
  let project (T (_, p)) = p
end
```

つぎに`Univ`というモジュールを用意します．
`Univ`はUniversal Typeの気持ちで，あらゆる型を`Univ.t`に埋め込むことができます．
埋め込みは型ごとに別々で，`piso ()`によって作成します．
ここで`()`を渡しているのはvalue restrictionがあるせいです．
埋め込みであることは`piso`の戻り値の型`'a t PIso.t`によって表現されています．

あらゆる型の値を一つの同じ型`Univ.t`に埋め込んでいるのでだいぶ怪しいコードに見えますが，
実際参照型をうまくハックした実装になっています．
以降の話でこの実装の中身を理解している必要はありませんが，これだけでも面白いので読んでみるといいでしょう．

```
module Univ : sig
  type t
  val piso : unit -> 'a t PIso.t
end = struct
  type t = unit -> unit
  let piso () =
    let r = Ref.make None in
    let inject a =
      fun () -> (r <- Some a) in
    let project f =
      (r <- None) before
      (f ()) before
      (match !r with
      | Some(a) -> a 
      | None -> error `oops`) in
    PIso.make inject project
end
```

次に型を表す値を作ります．モジュールの名前はずばり`Type`です．
型`'a`を表す`'a Type.t`は内部的には`string`と`'a Univ.t PIso.t`の組です．
`string`の方はその型の名前を表しているだけで，実際に大事なのは`'a Univ.t PIso.t`の方です．
名前を登録しなければいけないのは，このあと`Type.t`を鍵としたマップをつくるためです．
後々`forsome 'a. 'a Type.t`を鍵にとるようなマップが欲しくなるのですが，SATySFiではそのような型を持つマップがつくれないので`'a Type.t`の中の名前を鍵として代用します．

あと，`type 'a t = 'a u`とかかいう謎の文がありますが，これは[SATySFiの型検査器のバグ](https://github.com/gfngfn/SATySFi/issues/184)を回避するためのコードです．

```
module Type : sig
  type 'a t
  val make : string -> 'a t
  val name : 'a t -> string
  val piso : 'a t -> 'a Univ.t PIso.t
end = struct
  type 'a u = T of string * 'a Univ.t PIso.t
  type 'a t = 'a u
  let make name = T(name, Univ.piso ())
  let name (T(n, _)) = n
  let piso (T(_, i)) = i
end
```

最後に任意の値を表す`Any`というモジュールをつくります．
これは見た目だけのために導入するモジュールで，実質的には`Univ`と一緒です．
任意の値を`Any.t`にしたり，`Any.t`から任意の値を取り出すことができます．

```
module Any : sig
  type t
  val make : 'a Type.t -> 'a -> t
  val get : 'a Type.t -> t -> 'a
end = struct
  type u = Univ.t
  type t = u
  let make t a = PIso.inject (Type.piso t) a
  let get t x = PIso.project (Type.piso t) x
end
```

# 簡単な`Show`モジュール

ここまでの準備があるとad hoc多相を実現する`Show`モジュールが実装できます．
ただし冒頭で挙げた形にするにはもうワンステップ必要なので，その前に簡単な方の`Show`モジュールの実装を見せます．

`table`は，気分としては`('a -> string) Type.t`から`'a -> string`へのマップです．
ただしこのままだと型がおかしなことになるので鍵を`('a -> string) Type.t`から取り出した名前である`string`にし，値`'a -> string`を`Any.t`にキャストしています．
先ほどまでで準備した`Type`と`Any`がうまく使われています．

```
module Show : sig
  val apply : ('a -> string) Type.t -> 'a -> string
  val register : ('a -> string) Type.t -> ('a -> string) -> unit
end = struct
  let table : (string * Any.t) list = Ref.make []
  let apply t =
    match List2.assoc String.equal (Type.name t) (Ref.get table) with
    | Some(_, v) -> Any.get t v
    | None -> error `ooops`
  let register t f =
    table |> Ref.set (List2.acons (Type.name t) (Any.make t f) (Ref.get table))
end
```

# 正式な`Show`モジュール

先ほどの`Show`モジュールは`Show.apply`に渡す型(を表す値)が冒頭と違っていました．
これを解決するには`'a Type.t`を受け取って`('a -> string) Type.t`に変換する方法があればよさそうです．
ここで大事なのが，`Type.t`の実装です．
`Type.t`はその値ごとに違う埋め込みを表すので同じ`'a Type.t`に対して同じ`('a -> string) Type.t`を割り当てないといけません．
そこで，先ほどと同じようにして擬似的に`'a Type.t`から`('a -> string) Type.t`へのマップを作ります．
ということでそれを実装したのが以下になります．

```
module Show : sig
  val apply : 'a Type.t -> 'a -> string
  val register : 'a Type.t -> ('a -> string) -> unit
end = struct
  type 'a t = 'a -> string
  let tt : ('a t) Type.t = Type.make ` `
  let table2 : (string * Any.t) list = Ref.make []
  let get t =
    match List2.assoc String.equal (Type.name t) (Ref.get table2) with
    | Some(_, v) -> Any.get tt v
    | None -> error `oooops`
  let add t =
    table2 |> Ref.set (List2.acons (Type.name t) (Any.make tt (Type.make `fuga`)) (Ref.get table2))

  let table : (string * Any.t) list = Ref.make []
  let apply t =
    let t = get t in
    match List2.assoc String.equal (Type.name t) (Ref.get table) with
    | Some(_, v) -> Any.get t v
    | None -> error `ooops`
  let register t f =
    let _ = add t in
    let t = get t in
    table |> Ref.set (List2.acons (Type.name t) (Any.make t f) (Ref.get table))
end
```

すこしわかりにくいですが`get`と`add`は以下のような型です．

```
val get : 'a Type.t -> ('a t) Type.t
val add : 'a Type.t -> unit
```

# 実際に動かす

実際に動かすとこんな感じです．めでたしめでたし．

```
let int = Type.make `int`
let string = Type.make `string`
let _ = Show.register int String.of-int
let _ = Show.register string Fn.id
let _ = Debug.log (Show.apply int 42) % => `42`
let _ = Debug.log (Show.apply string `foo`) % => `foo`
in
finish
```

ここまでの話を応用するとあらゆる型に対してad hocに振る舞う等価性判定の述語`Equal`とかもつくれます．たとえば，SATySFiで言えばFloatの等価性やStringの等価性，Lengthの等価性を同じコードで記述できるようになります．
一方，こういった`Show`や`Equal`を大げさに「型クラス」と呼ぶことにすると，型クラスを定義するたびに毎回似たようなモジュールを書き続けることになります．こればっかりはSATySFiにfunctorがないのでどうしようもありません．
TIVによる型クラスのエミュレーションは実用できなくもないですが，本当のところをいえばSATySFiがネイティブにこのような機能をサポートしてくれることが望ましいです．
実際，ここでは書かなかった`('a list) Type.t`や`('a -> 'b) Type.t`のような高カインドの場合は上記のコードにくわえてやることがそれなりに増えてしまいます．
これからのSATySFiのさらなる発展に期待しましょう．