# 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”.