Open Source Your Knowledge, Become a Contributor

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

Create Content

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. Create New Content