# IDP4 playground

### Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

## Tuples and Constructors

IDP4 can handle more data than just numbers, strings and Booleans. In this section we introduce more advanced types.

### Tuples

Constructing tuples is straightforward: just write a tuple of expressions like this: `(x,y,z)`

. Tuples of any arity (except 1) are supported. This means that the empty tuple `()`

exists. As wel as the 8-ary tuple `(0,3,4,9,7,6,1,5)`

exists.

When you get a tuple as input you should also be able to deconstruct it. You can do this in a number of ways.

- The simplest one is to use the tuple notation at the lefthand side of a definition.
`(a,b) := x`

. This means that you define`a`

to be the first component of the binary tuple`x`

and`b`

to be the second one. - Tuple deconstruction is also possible as locally scoped argument of a function definiton, in which case you assume a function to take tuples as its input. For instance,
`f (a,b) := a*b`

is a unary function which takes a binary tuple and multiplies its components. This also works with anonymous functions`\(a,b) -> a * b`

. - You can use a
*case*-construct to deconstruct the tuple.`case x of (a,b) -> a+b;`

. This expressions deconstructs the tuple`x`

and locally introduces the new variables`a`

and`b`

to evaluate the expression`a+b`

, which is the evaluation of this tuple.

**Warning:** Tuple deconstructions are always definitions, which never form constraints on their own. As such, you can not deconstruct a tuple with `(a,a) := x`

to enforce that the components of `x`

are equal. Use `(a,b) := x`

and `a = b`

instead.

### Constructors

It is easy to get lost in the data when a lot of tuples are nested. For this reason we can use constructors. They are declared like this: `s\1 :: constructor`

for a unary constructor named `s`

. Constructors without arguments are also supported `nil\0 :: constructor`

.

All the techniques for deconstructing tuples generalize to constructors, except that you need to use square brackets `[`

`]`

instead of round brackets `(`

`)`

.

- You can pattern match the left side of the definition like this:
`s [x] := y.`

- Using patterns in the function definition is also allowed.
- Case-constructs also work for constructed types, it is even possible to match multiple patterns in one case like this
`case x of s[y] -> y ; nil [] -> z;.`

Patterns are handled top to bottom, and the first pattern that matches corresponds to the value of the case expression. So the expression`case x of s[s[nil []]] -> 5 ; s[x] -> 2 ; x -> 0;.`

will map the Peano representation of 2 to 5, all other successors to 2, and everything which is not a successor of something to 0.

Note again that square brackets are used when deconstructing constructors. This serves to differentiate between `f x := y.`

which declares a new function `f`

which is the constant function to `y`

and `f [x] := y.`

which declares the new symbol `x`

as removing the outer constructor `f`

from `y`

.

Using `s`

and `nil`

we can now do some Peano arithmetic.

### Cases of integers

The case-construct can be used in even more circumstances. In the matching part of a case expression you can also write comparisons with a fixed number (something like `=< 0 -> 5;`

). An underscore is handled as a *don't care*-pattern and matches everything.
This allows us to for example define the factorial function.