ErlangだってブレイクしたのだからCafeOBJだって…… って、それはないか。
Diaconescuの論文*1にあった例：
mod R2VECT {
pr(FLOAT *{sort Float -> Real}) -- FloatをRealとリネーム
[Vect] -- R×Rで定義されるベクトル空間（のつもり）
op 0 : -> Vect
op <_,_> : Real Real -> Vect
op _+_ : Vect Vect -> Vect
op -_ : Vect -> Vect
op _*_ : Real Vect -> Vect
vars a b a' b' k : Real
eq 0 = < 0 , 0 > .
eq < a , b > + < a' , b' > = < a + a' , b + b' > .
eq - < a , b > = < (0 - a) , (0 - b) > .
eq k * < a , b > = < k * a , k * b > .
}
CafeOBJ（に限らずOBJファミリー）は、予約文字が少ないので自由に文字／記号が使えるのだけど、区切り記号（delimiter, self terminating character）を指定できないので、空白の挿入が必要です。つまり、<a, b> とは書けなくて < a , b > と間延びする。アー残念。
それはともかく、上の例は、Rを実数として R×R = R2を台（underlying set）とするベクトル空間の定義です。本物のRは扱えないけど、組み込みの型（ソート）FloatをRealにリネームして雰囲気を出してます。これで、普通の計算は普通にできます。
だけどこの定義だと、実はR2を特定できるわけではなくて、意図しないモデルも存在します。Vectを（R2ではなくて）R、< a, b > を a + b （実数の足し算）と解釈してもすべての等式（公理系）を満たすんですね。ほんとにR2だと主張したいなら、<_,_> が直積のペアリングであることを明示するとか、次元の概念を導入しないとダメのようです。
