# IDP4 playground

IngmarDasseville
2,841 views

## 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.
Tuples
1
2
3
4
5
6
7
8
9
10
11
12
13
14
tup := (2,(3,4)).
(a,b) := tup.
x := case b of
(a,b) -> a+b;.
f (a,b) := a*b.
fb := f b.
relevant tup.
relevant a.
relevant b.
relevant x.
relevant fb.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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.

Constructors
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
s/1 :: constructor.
nil/0 :: constructor.
two := s (s ( nil )).
s [one] := two.
minusOne x := case x of
s [ a ] -> a;
nil [] -> nil;.
anotherOne := minusOne two.
zero := minusOne one.
anotherZero := minusOne zero.
relevant two.
relevant one.
relevant anotherOne.
relevant zero.
relevant anotherZero.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

### More cases

The case-construct can be used in even more circumstances. In the matching part of a case expression you can also write a fixed number or string. An underscore is handled as a don't care-pattern and matches everything.

You can split definitions in to multiple lines as syntactical sugar for a case-construct. This allows us to for example define the factorial function.

More Patterns
1
2
3
4
5
6
factorial 0 := 1.
factorial x := x*(factorial (x-1)).
x := factorial 4.
x = 24.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Open Source Your Knowledge: become a Contributor and help others learn.