SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/tuples and functions

Tuples and functions

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

Emacs suffix

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

- Introduction

- Tuples

- Nesting and conversion of tuples

- Function calls with tuples

- Variable initialization with tuples

- Tuple initialization with variables

- Functions with multiple return values

- Emacs suffix


ip-location