let x = expr1 in expr2
この式は、expr2 内の変数 x へのすべての参照は、expr1 を評価した状態で行い、expr2 を評価します。 expr1 と expr2 はそれぞれ Π タイプである必要がありますが、これらの式のタイプを同じにする 必要はありません。つまり、expr1 のタイプが Π1 で、expr2 の タイプが Π2 の場合、Π1 = Π2 である必要はありません。
let x = 5 in x + 7 ⇒ 12 (let x = 5 in x + 7) + 3 ⇒ 15 let x = 5 in let y = 7 in x + y ⇒ 12 let x = 5 + 7 in x + 3 ⇒ 15 let x = 5 in let x = x * x in x ⇒ 25 let x = model in class x ⇒ Model let x = all "Class" in size x <> 0 ⇒ true let x = all "Class" in size x <> 0 implies (there_exists y in x => $name of y = "Dishwasher") ⇒ true let x = all "Class" in size x <> 0 implies (there_exists y in x => $name of y = "FooBar") ⇒ false
if test then expr1 else expr2
この式の値は、test の 値に依存します。test が true と評価した場合、式全体は expr1 と評価します。それ以外の場合、式全体は expr2 と 評価します。test の型はブール である必要があります。 また、expr1 と expr2 のタイプは両方とも Π である必要があります。 expr1 と expr2 のタイプは同じでなければなりません。 つまり、expr1 のタイプが Π1 で、expr2 の タイプが Π2 の場合、Π1 = Π2 である必要があります。
if true then 1 else 0 => 1 if class x = "Operation" then "Found Operation" else "Found " + class x => Found Model (if false then "abc" else "123") + "def" => 123def
for_all x in ocoll => predicate ≡ not (there_exists x in ocoll => not predicate)
there_exists x in ocoll => predicate ≡ not (for_all x in ocoll => not predicate)
これらの式は、アサーション ∀xεocoll (predicate(x)) および ∃xεocoll (predicate(x)) と評価します。 つまり、for_all は、ocoll が空であるか、あるいは、ocoll 内のすべてのオブジェクトが predicate を満たす場合、かつ その場合に限り、true を返します。さらに、there_exists は、ocoll 内に predicate を 満たすオブジェクトが少なくとも 1 つある場合かつその場合に限り、true を返します。
これらの式の実際の評価は、以下のように行われます。 for_all および there_exists の両方について、 変数 x は ocoll 内の各オブジェクトに順番にバインドされ、predicate は、 そのような x のバインディングのコンテキスト内で評価されます。predicate が false と評価された場合、for_all が false と 評価されます。predicate が true と評価された場合は、there_exists が true と評価されます。ocoll 内のすべての オブジェクトがテストされる前にいずれの条件にもならなかった場合は、for_all が true に評価され、there_exists が false に評価されます。これらの式は、x の各バインディングで、パーベイシブ変数 current も x にバインドします。
式のタイプ ocoll はオブジェクト・コレクション、タイプ predicate はブール となります (オブジェクト → ブール と解釈します。x は predicate の暗黙のパラメーター)。
以下の例で、Tree、Branch、および Leaf と いう 3 つのクラスがあると仮定します。
for_all x in all "Class" => class x = "Class" ≡
for_all x in all "Class" => class current = "Class" ⇒ true
there_exists x in all "Class" => $name = "Leaf" ⇒ true
for_all x in all "Class" => $name = "Leaf" ⇒ false
not (for_all x in all "Class" => $name <> "Leaf") ⇒ true
for_all x in anEmptyCollection => false ⇒ true
for_all x in anyCollection => current = x ≡ true ⇒ true
for_all class in all "Class" =>
there_exists op in class->[operation] =>
$name of op = "grow" ⇒ false