Alloy本4.2.2

4.2.2章の記法はもちろん間違いじゃないけど、理解するまで結構悩んだ。

sig A {f: e}

こう書かれるとfとeは似た種類のものだと思うじゃない？で、

f in A -> e

という制約がfactに入っているのと同じ、と続いて、さらにそれは

all this: A | this.f in e

と同じだ、と書かれている。thisが太字、つまりallなんかと同じ特殊な意味を持つ風の表現で。

僕ならこう書く。

sig A {f: E}

eはたしかに式であって、一般的にはシグニチャとは限らない。だけども、

sig Man {
  wife: Woman
}

というコードにおいてA=Man, f=wife, E=Womanなわけで。Aとeよりもeとfの方が近く見える表現はミスリーディングだ。

つぎのf in A -> eもわかりにくい。もちろん嘘ではないんだと思うけどさ、読者がinと->の優先順位を正しく把握していると仮定するのは無茶だ。f in (A -> e) であることをせめて脚注くらいには書くべきだ。

そして最後のthis、わざわざthisが太字で書かれているからには、特別な意味を持っていると思うのが普通じゃないだろうか。僕はこれをみて「all x: A | x.f in e」ではダメなのか？と疑問に思った。結局、読み進めるとp.94の「議論」で「本当はthisがキーワードだからこういう書き方はできない、all x: A | x.f in eならOK」と書いてあるわけだ。これはひどい。最初からそう書いておけばいいじゃん。

このEが式であるって話だけども、p.73から例を挙げるとaddress: Name -> Addrみたいなことができるんだね。これだけみるとHaskellの型コンストラクタ(->)と同じように見えるけど、->は単に直積の演算子ってところがすごい。Name + Addrができるのも「ああ、それHaskellでもOCamlでもできるよ」って思いがちだが、集合の和だけではなく差も積も取れる。すごい。

なんか「こんなことできるんだ、すごい」って例を考えてみよう。

んー。意外と思いつかない。フィールドの型宣言みたいなものと感じたせいで「おおお、型をこんなに加工できるなんて！」と思ったが、そもそもいくらでもfactを追加して取りうる値の範囲を好き放題加工できる言語なわけなのであった。