Just $ A sandbox

プログラミングと計算機科学とかわいさ

Tagless-finalによるデータ型の間の変換

Q. Tagless-finalってなんぞや

A. (in short)

データ型DをF[D]のinitial algebraとみなしたとき、initialityより、任意のalgebra F[D](X) --> Xに対してunique transformation D --> Xがある。
このときfamily forall X. F[D](X) --> XをDのTagless-final representationとよぶ。

A. (in plain and concrete context)

Tagless-final representationというのがあり、なんぞやみたいなお話。

コードで詳しくみていきます

まずListの標準的なrepresentationは List[a] = 1 + a × List[a]になる。
データコンストラクタは Nil: 1 -> List[a]Cons: a -> List[a] -> List[a] の2つ。

で、ここで各コンストラクタを次のように変形する: nil: 1 -> r, cons: a -> r -> r
すると、 型rに対してnilとconsの組を与えると、uniqueにList[a] -> rが次のように決まる:

f : List[a] -> r,
f Nil = nil()
f (Cons x xs) = cons x xs

みるとわかるけどこれはちょうどリストに対する再帰関数を定義していることと同じである。
ノリはScott encodingでやっていることと同じ。

また、nil, consとしてNil, Consを取ると上で定義されるfがidentityになるので、ちょうどぴったり元々のList[a]に一致する。

で、List[a] -> rなる関数は上のnil, consで作ることができるので、例えばlistのsum関数が次のように計算できる:

-- 定義したいのは下
sum_of_List :: List -> Int
sum_of_List N = 0
sum_of_List (C x xs) = x + sum_of_List xs

-- 作り方は下
class TgList tg where
  nil :: tg
  cons :: Int -> tg -> tg

instance TgList (Tagged "sum_of_List" Int) where
  nil = 0
  cons m (Tagged n) = Tagged $ m + n

さて上ではnil, consをclassで定義したけれど、これはclassの継承関係がdatatypeのextensionに対応するから嬉しいヾ(。>﹏<。)ノ゙✧*。
つまり、List[a]を拡張する(データコンストラクタを追加する)ことが、class List[a]を継承したクラスを定義することに対応する。

Haskellのデータ型はextensibleではないので、上のような表示は後からデータ型を追加できるので嬉しいわけです。 (詳しくはサンプルのList2をみて)

このような、データコンストラクタを対応する関数を使って表示する仕方をTagless-final representationという。


まとめると、上で言うclass TgList tgインスタンスinstance TgList Xを書くと、List[a] -> Xが得られる。

さて、2つの異なるデータ型の間の変換をしたいとする。
このときこれらをTagless-final representationによって表現したい。

上のコードで言うとList --> List2という変換をしたいとする。

-- map between tagless final representations
-- duplication : List --> List2
-- <=> TgList List2
instance TgList2 tg => TgList (Tagged "duplication" tg) where
  nil = Tagged nil
  cons m (Tagged n) = Tagged $ cons2 m m n

これは次の関数を定める:

f : List -> List2
f Nil = Nil
f (Cons x xs) = Cons2 x x (f xs)

さて、これは一般に次のようにかける:

-- A = A1(f1..f1') | .. | An(fn..fn')
class TgA a where
  A1 : F1 -> ... -> F1' -> a
  ...
  An : Fn -> ... -> Fn' -> a

-- B = B1(g1..g1') | .. | Bn(gn..gn')
class TgB b where
  B1 : G1 -> ... -> G1' -> b
  ...
  Bn : Gn -> ... -> Gn' -> b

-- このとき、f: A -> Bは次のinstanceから定まる

instance TgB a => (TgA a)
  A1 = \f1 .. f1' -> M1(f1 .. f1')
  ...
  An = \fn .. fn' -> Mn(fn .. fn')

-- fはuniqueに定まる
f : A -> B
f A1(f1..f1') = M1(f1..f1')
...
f An(fn..fn') = Mn(fn..fn')

ので、まぁデータ型の間の変換はTagless-finalの間の変換にliftができる。


最後のpolymorphic typeについては、MultiTypeParameter typeclassが必要になるが、その際にFunctionDependencyが必要になる場合がある。
まぁそれはそれ

最近TaPLをやっていてλ計算のタイプチェッカーを書いているのだけれど、それを上のTagless-finalで表現している。
データ型がextensibleになるのですごく良い感じになる。

まぁ簡単な話ではあるのだけれど念の為まとめておいた。