The Eiffel Compiler / Interpreter (tecomp)

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 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

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.

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.

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

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

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".

Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: