let x = expr1 in expr2
This expression evaluates to expr2, with all references to the variable x in expr2 evaluating to expr1. Each of expr1 and expr2 must have some type Π, but the types of these expressions need not be the same. That is, if expr1 has type Π1 and expr2 has type Π2, then it is not necessary for Π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
The value of this expression depends on the value of test. If test evaluates to true, then the whole expression evaluates to expr1. Otherwise, the whole expression evaluates to expr2. The type of test must be boolean, and the type of both expr1 and expr2 must be some Π. The types of expr1 and expr2 must be the same. That is, if expr1 has type Π1 and expr2 has type Π2, then it must be the case that Π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)
These expressions evaluate to the assertions ∀xεocoll (predicate(x)) and ∃xεocoll (predicate(x)). That is, for_all returns true if, and only if, either is empty or every object in satisfies the predicate. And there_exists returns true if, and only if, there is at least one object in ocoll which satisfies predicate.
The actual evaluation of these expressions occurs in the following way. For both for_all and there_exists, the variable x is bound in turn to each object in ocoll, and predicate is evaluated in the context of such a binding of x. If predicate evaluates to false, then for_all evaluates to false. If predicate evaluates to true, then there_exists evaluates to true. If neither condition occurs before all objects in ocoll have been tested, then for_all evaluates to true, while there_exists evaluates to false. These expressions also bind the pervasive variable current to x at each binding of x.
The type of the expression ocoll must be object collection, and the type of predicate must be boolean (which we interpret as object → boolean, with x being the implicit parameter to predicate).
In the following examples, suppose that there are three classes, named Tree, Branch, and Leaf.
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