DSL

Tagless-finalの何がfinalでどうtaglessなのかの雑なメモ

Tagless-finalはOlegさんの作った言葉らしいですが、何がfinalでどうtaglessなのか、応用例はいっぱい出てくるけど定義そのものが出てこない状況が5年前からあまり変わってないようなので雑にメモとして残しておきます。

何が嬉しいのかは他の人がいっぱい書いているので適当にググってください。

何がfinalか

プログラミングをしていると、種からデータ構造を組み立てる操作(unfold)とデータ構造を潰して値を得る操作(fold)がよく出てきます。これを圏論をかじってる人たちは圏論から輸入した言葉で始代数 (initial algebra) と終余代数 (final coalgebra) と呼んだりします。1 元々tagless finalはインタープリタで使われていた言葉なのですが、それで説明するとソースコードを読んで構文木のデータ構造を作るのが始代数、評価して値を得るのが終余代数となります。

Finalとはこの終余代数のfinalだった気がする。。

どうtaglessなのか

Tagless finalでは陽に直和を使ったデータ構造を作らずに、代わりにfoldかそれに類するものを直接使ってしまいます。2 通常直和の実装にはどの種類か特定するためにタグが使われますが、関数の違いで表現するので不要になります。

Taglessとはこの直和のタグが要らないことだった気がする。。


  1. 余談ですが自分は運算系なのでanamorphismとかcatamorphismとかいいます。 

  2. 直和だけ部分的にチャーチエンコーディングした雰囲気