i remember nothing

文章の練習も兼ねています

Generic Programmingことはじめ

はじめに

この記事はHaskellなどの関数型言語におけるGeneric Programming が何なのかを知りたい人向けに書かれています。 ただ、この記事に出てくるコードは簡易的に書いてある擬似的な関数型言語なので、現状そのままでは実行できません。概念が理解できればと思います。

Generic Programmingは何が嬉しいのか

  • 型を任意に構成できる
  • 任意に構成した型を一般的に扱える関数が作れる

以下、Regular という実装方法を用いて generic に型を構成してみます。

1.Type Descriptorを用いていろんな型を構成しよう

今回のgeneric programmingでは、 型の構成法をバッカスナウア記法のような形で表記します。 例えば単純型付きラムダ計算の場合は

t = base | t -> t

のように表されます。 このような定義では、「または」を表す縦棒|で選択肢が区切られていて、 各選択肢の中は列挙されている要素で構成されています。

  • base : 基底 (ex. Unit)
  • t -> t : 2つの型から構成された矢印型

これを generic に表現するために、データ型として、 type descriptor を構成します。

これを擬似Haskellで表現すると

data Desc =
      Base
    | Desc :*: Desc
    | Desc :+: Desc
    | Rec

このデータ型のコンストラクタはそれぞれ

  • Base : 基底 (ex. Unit)
  • Desc :*: Desc : 直積(かつ)
  • Desc :+: Desc : 直和(または)
  • Rec : ここで再帰がおこることを示す

となる型を定義しています。

これを用いて、単純型付きラムダ計算

t = base | t -> t

を定義すると

stDesc :: Desc
stDesc = Base :+: Rec :*: Rec

のようになります。

これは

  • 最初の Base : 基底型
  • 次の Rec :*: Rec : t -> t
    • 関数型の両辺は任意の型が来て良いため Rec で明示

という意味になります。

これで型の定義を与えることが出来るようになりました。

2.具体的な型を表現しよう

定義が与えられるようになったので、次は具体的な型を表現してみます。 まず Descのプログラム上の表現(意味)を以下の関数で表現します。

descSemantic :: Desc -> Set -> Set
descSemantic Base x = T {-全称型-}
descSemantic (d1 :*: d2) x = (descSemantic d1 x) × (descSemantic d2 x) {-集合における直積-}
descSemantic (d1 :+: d2) x = (descSemantic d1 x) U (descSemantic d2 x) {-集合における直和-}
descSemantic Rec x = x

descSemantic は「再帰部分が x であるような Desc 型の値」を表しています。 この再帰部分 X に自分自身を入れる(再帰を閉じる)と、具体的に Desc 型の値を作ることが出来るようになるということです。

再帰を閉じるには、以下のFixという不動点を表すデータ型を使います。

data Fix (d : Desc) =
     F : descSemantic d (Fix d) -> Fix d
   | M : (x : Fin) -> Fix d

ここで、Fin は finite set(有限集合)の型です。

  • F は具体的な値を作り出す構成子
  • F の引数に再帰部分に自分自身である Fix D m を入れることで再帰を閉じている
  • M はメタ変数を表現する構成子

Fで明示的に再帰を閉じることで、任意に大きなデータを作ることが出来るのがポイントです。

すると、stDesc 型(単純型付きλ計算の型を表す型)を以下のように書くことができます。

stType :: Set
stType = Fix stDesc

すると、例えばUnit型は以下のように表現できます。

tbase : stType
tbase = F (tt._1)

また、関数型を作る関数を定義すると、さらに複雑な型を表現できます。

arrow : stType → stType → stType
arrow t1 t2 = F ((t1 , t2)._2)
ttt :: stType
ttt = arrow tbase (arrow tbase tbase)

ここで、ttt は base -> base -> base を表しています。

所感

疲れました。。。

ディスクリプタに対して関数を構成しておけば任意の型を受け取ることができるのはロマンがありますね。

参考文献

A Lightweight Approach to Datatype-Generic Rewriting http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-020.pdf