A.1.4 Function Types

A.1.4 Function Types

Synopsis

Description

The type TA -> TR denotes the domain of unary functions with argument type TA and result type TR; every such function f takes an argument a from TA and returns a result f(a) from TR.

The type (T1, T2, ..., Tn) -> TR denotes the domain of n-ary functions with argument types T1, T2, ..., Tn and result type TR; every such function f takes n arguments a₁ from T1, a₂ from T2, ..., a_n from Tn and returns a result f(a₁,a₂,...,a_n) from TR.

Pragmatics

Because of a deficiency of the underlying decision procedure, the system does currently not understand that, if two functions are equal, also their function values are equal, i.e. it does not implement the following derivation rule:

[E] |- T_1: type
[E] |- T_2: type
[E] |- I_1: T_1->T_2
[E] |- I_2: T_1->T_2
[E] |- V: T_1
[E] ... |- I_1 = I_2
--------------------------
[E] ... |- I_1(V) = I_2(V) 

To overcome this problem, one may instead use an array type (which implements the corresponding rule for array access) or explicitly introduce corresponding axioms on demand.

The type (T1, T2, ..., Tn) -> TR is different from the type [T1, T2, ..., Tn] -> TR. While the former denotes a domain of n-ary functions, the later denotes a domain of unary functions whose argument type is a tuple type; each such a function f takes an n-ary tuple t=(a₁,a₂,...,a_n) and returns a result f(t)=f((a₁,a₂,...,a_n)).

Function values can be constructed as described in Section A.2.7.

A.1.4 Function Types