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になるのですごく良い感じになる。
まぁ簡単な話ではあるのだけれど念の為まとめておいた。