nil sucks!

卒研テーマの2階マッチングアルゴリズムをOCamlで実装中。
そこでリストに不満を感じるようになったのでそれについて。

2階マッチングアルゴリズムってのは述語論理式やラムダ計算の式とかを
扱うんだけど、当然そういった式をデータ構造で表さなくちゃいけない。

述語論理には∀x.P(x)とか∃x.P(x)の∀、∃みたいなquontifierって記号があって、
∀x.∀y.∀z.P(x, y, z)を∀xyz.P(x, y, z)って略記したりするらしい。
ラムダ計算にもλx.λy.λz.f(x, y, z)って式をλxyz.f(x, y, z)って表記したりする。

そこで、∀xyz.P(x, y, z)やλxyz.f(x, y, z)の「xyz」と「(x, y, z)」の部分をリストで
実装することにした。んだけど今は後悔している。

リストってのは0個以上のオブジェクトの並びだからデータ構造自体は∀.P()なんて
おかしな形もとれてしまう。もちろんこういった不正なオブジェクトができないように
手続きで保障するんだけど、すべての手続きの中で「∀.P()の形だったら……」なんて
書くのがめんどくさくなってきた。

Ocamlではリストは次のように定義されているんだけど、

type 'a list = [] | :: of 'a * 'a list

こういった、非Nilリストが欲しいなぁと。

type 'a nnlist = Only of 'a | :: of 'a * 'a nnlist

これが[1; 2; 3]みたいなシンタックスシュガー付きであったら……。

……要らないか。