typecheckerとTagless-final, revised

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

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

ここでは各λ項は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のデータ型の間の変換は結構かきにくいことがあり、どうするのがいいんだろうか

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