typecheckerとTagless-final, revised

1個前の記事でTagless finalについて触れたんだけどどうも全く頭が回っていなかったらしくほとんど内容がない記事になってしまったので書き直す、というかちょっと違う話を。

はじめに、TaPLにあるλ計算のtypecheckerをHaskellで実装することをやっている:

github.com

ここでは各λ項はTagless-finalで定義する。
ところで、データ型が取る型パラメータをa(あるいはaへの変換可能なもの全体)に限れば、データ型の値は常にa型をNodeにもつfinitely-branching treeで表現できる。
(これはTagless-finalの文献に書いてある)

ので、Tree StringをSyntaxと呼ぶことにして、
Syntaxへの変換とかはPatternSynonymsとかを使って良い感じに定義する。

-- Untyped value
class UVal repr where
  uabs :: repr -> repr

-- Untyped expr
class UVal repr => UExp var repr | repr -> var where
  uvar :: var -> repr
  uapp :: repr -> repr -> repr
  uisVal :: repr -> Bool

-- pattern synonymはコンストラクタに対するabbreviationだと思えばよい
pattern V v = T.Node v []
pattern Pvar var = T.Node "var" [V var]
pattern Pabs exp = T.Node "abs" [exp]
pattern Papp exp1 exp2 = T.Node "app" [exp1,exp2]

-- Syntax(= Tree String)へは常に変換可能
instance SpExp Int Syntax Syntax where
  svar = Pvar . show
  sabs v = PabsT (show v)
  sapp = Papp

こうすると、例えばsabs (svar 0) :: SyntaxがNode "abs" [Node "var" [V 0]]みたいに評価される。

さて、ここでcall-by-value(評価戦略は何でもいいんだけども)のevaluationを定義したいとする。

evalはeval: Term -> Termになるはずなので、Tagless finalでかくとeval: (UExp _ r) => UExp _ rみたいになるはず。

なので、こいつのinstanceを書けばいいんだけど、具体的にどうやるとよい感じなのかがイマイチわからない。
というか、多分それらしい実装は書けるんだろうけど、本来定義したい関数の実装からかなり離れた実装になるので、書いたものがcall-by-valueであるかどうかを判断するのがかなり難しいような気がする。

recursive functionを機械的にTagless final conversionに変換できればいいような気がするけど、できるんだろうか(真面目に考えてない)

ちなみに一旦Syntaxに飛ばしてからSyntax -> Syntaxを構成するという方法もあるけど、これは例えば上のUExpを拡張したときにevalの関数全体をすべて書き直す羽目になるので(再帰項のスコープの都合)イマイチ

さてどうしような〜って思って若干困っています

こういう感じで、Tagless-final representationのデータ型の間の変換は結構かきにくいことがあり、どうするのがいいんだろうか

詳しい人いたらぜひ教えてください

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になるのですごく良い感じになる。

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

Freer Monadじゃあないんですよ

Extensible Effectsという、大変有名なモナドの合成方法があって、まぁこれはいいんだけど、関連する話でFreer monads, more extensible effectsという論文があり、これまた界隈では有名なんだけどなんやねんって話。

とりあえずext effはモナドを直和していい感じにするってことと、freerはOperational Monadを使ったんやなってことがわかっていればひとまずクリアという感じ。

よく知らない人はこれ読んで めっちゃわかりやすいから👇

Freer Monads, More Extensible Effects from Hiromi Ishii

www.slideshare.net

さて、まぁ上のような説明も上にあげた論文もHaskellのコードしか書いてなくてさっぱり分からないのでもっとちゃんと定式化しようねということを簡単にまとめます。

というか主にOperational monadの話な気がする。

Free Monad

今更言うまでもないけどFree monadはforgetful U : Mon{C} -> [C,C]のleft adjointである。

Old Eff

Freerじゃない方のExt Effは次で定まるものである。

Eff <Ti> := Free((+)Ti)

(+)TiはTiたちの直和のことで、TiたちがfunctorであればEff <Ti>はモナドになるし、(+)Ti -> (+)SjなるnatはEffの間のmonad morphismを誘導する。

Operational Monad

Operational MonadはOpM = Free . Coyoneda : [Ob(C),Ob(C)] -> Mon{C}っていう形のやつで、
CのObjectの間のmap familyがあればそこからモナドが作れるというなかなか面白いやつです。

ちなみにCoyonedaというのは次のようなもの:

Coyoneda f = Lan f 1 = 1†f = ∃b. (hom(b,-),Fb)

一番最後の形はKan拡張をcoendでかいたやつで、右のタプルをbに渡って直和を取ったものと思えばいい。

coend形を見れば、なぜOb(C)の間のmap familyがFunctorに拡張できるのかはすぐにわかると思う。

Freer Monad

これを使って次のようにしよう:

Eff <Ti> := Free(Coyoneda((+)Ti)) = OpM (+)Ti

すると、map family(+)Tiからモナドが得られる。

つまり、ただのmap familyたちTiがあると、(これは例えばGADTとかで1変数データ型を適当に作ってやればいい)
それらの作用をすべて含むモナドができて嬉しいねという話である。

さらにこれはいくつかの便利operationがあって、

send : Ti --> Eff<Ti> (injectionみたいなやつ)や
run : (T --> Ti) -> (Eff (T : <Ti>) --> Eff <Ti>) (injectionのMonad morphismへの持ち上げ)みたいなやつが得られるので

まぁ便利ねということである。

---

とかいうことを真面目にpdfにしようかなと思ったんだけど
需要があるのかよくわからないしやめました

でもせっかくなのでformalizeとかしたいねという気持ちはたしかにあります
ところで以下のようなcategory theory formalize projectがありますので(唐突な宣伝)
協力してくれる人、困ったときに相談に乗ってくれる人なんかがいましたらぜひに。

ちなみに現在の進捗は非常に辛かったコンマ圏のuniversalityを示し、そろそろ各点Kan拡張を定義するあたりです。

github.com

おわり