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.
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
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
ato be the first component of the binary tuple
bto 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*bis 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
xand locally introduces the new variables
bto 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.
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
f [x] := y. which declares the new symbol
x as removing the outer constructor
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.