Introduction
Tuples are very versatile in Modern Eiffel. This is due to the possibility
that tuples and sequences of expressions can be freely mixed as long as the
corresponding types match.
In the following tuples and the possible use of tuples in expressions and
functions is shown.
Tuples
Tuples are product types. If you have the types A and B, then the type [A,B]
is a tuple where the first component is of type A and the second is of type
B.
You can construct tuples with more components as [A,B,C,...].
The special case of an empty tuple type [] (i.e. a tuple with no component) is
possible as well.
If “e” is an expression of type [A,B,...] you can access the components by
“e.1″, “e.2″, …
A tuple object of type [A,B] can be created with the expression “[a,b]” where
“a” is an expression of type A and “b” is an expression of type B.
Tuple types are immutable. Two objects of tuple type are equal if and only
if their corresponding components are identical.
In order to access the components by name it is possible to label the tuple
type. The type [a:A,b:B] is semantically the same type as [A,B]. If “e” is an
expression of type [a:A,b:B] then the components can be accessed by “e.a” and
“e.b”.
-- tuple type
[A,B] -- tuple type with two components
[a:A,b:B] -- labelled tuple type
[] -- empty tuple type
[a,b] -- expression of tuple type [A,B],
-- if "a" has type A and "b" has type B
[a,b].1 ~ a -- component access
[a,b].2 ~ b -- Note: the identity operator has to be used, because
-- A and B might be mutable
A tuple of type [A,B,...] is semantically equivalent to the inductive type
case class SOME_TUPLE[A,B,...] create
tuple(a:A; b:B; ...)
end
i.e. the proof engine infers automatically the rules for equality
all(x,y:SOME_TUPLE[A,B,...]) check
elim_1: (x=y) => (x.a~y.a)
elim_2: (x=y) => (x.b~y.b)
...
intro: (x.a~y.a) => (x.b~y.n) => ... => (x=y)
end
Nesting and conversion of tuples
Tuples can be nested to arbitrary depth.
[A,B] [A,[B,C],D] [[[A]]]
For each tuple type there is a corresponding sequence of types which is
obtained if all square brackets are ommitted
tuple type sequence of types [A,B] A,B [A,[B,C],D] A,B,C,D [[[A]]] A
An object of tuple type T1 can be converted into an object of tuple type T2 if
the corresponding sequences of types are identical.
All of the following tuples are mutually convertible.
[A,B,C,D,E] [[A,B],C,D,E] [A,[B,C],D,E] [A,[B,[C,D]],E] ...
Furthermore any sequence of expressions can be converted into a tuple and vice
versa as long as the sequence of their types is identical to the sequence of
types of the tuple.
These conversion rules give enormous flexibility with function calls and
variable initializations. This will be demonstrated with some examples in the
following chapters.
Function calls with tuples
Consider a function with the declaration
f(a:A, b:B, c:C, ...): RT
then
f(a,b,c,...)
is a valid expression if the expression “a” is of type A and the expression
“b” is of type B …
Lets assume further that we have a function “g” returning an object of tuple
type [A,B] i.e. it has the signature
g(x:X): [A,B]
In this case the expression
f(g(x),c,...)
is valid as long as “x” is an expression of type “X”.
I.e. a tuple can replace a sequence of arguments in expressions as long as the
types match.
Variable initialization with tuples
Modern Eiffel has let expressions (i.e. expressions with local variables)
local
a:A, b:B, c:C,... := aexp, bexp, cexp
then
f(a,b)
end
with the obvious meaning.
Any sequence of expressions can be replaced by a tuple expression with
consistent types. With the above function “g” which returns a tuple of type
[A,B] the following is valid as well.
local
a:A, b:B, c:C,... := g(xexp), cexp
then
f(a,b,c,...)
end
Tuple initialization with variables
The last two chapters have shown that a tuple expression can initialize a
sequence of variables as long as the corresponding types match.
The reverse is useful as well. We can call functions which expect tuple
arguments with a corresponding sequence of expressions.
-- signature of function "h" h(a:A, t:[X,Y], b:B): RT -- valid expressions h(aexp, [xexp,yexp], bexp) h(aexp, xexp, yexp, bexp)
The same applies to tuple initialization in let expressions
local
t:[X,Y] := xexp, yexp
then
...
end
Functions with multiple return values
A function returning a tuple type returns implicitly multiple values. E.g.
tup_func(x:X): [A,B]
require
...
ensure
Result = [aexp, bexp]
end
In Modern Eiffel we can define a function which explicitly returns multiple
values.
mr_func(x:X): a:A, b:B
require
...
ensure
a = aexp
b = bexp
end
With that definition the function “mr_func” can be used in exactly the same
places as “tup_func”.
