5.3 User Defined Types

In Type Definitions we described the user defined types. Here we discuss the pragmatic constraints on these types.

To simplify type inference we insist that each term has a unique minimal type. This constraint has consequences for the various user defined enumerated types.

For example if we allowed the definitions

def range1 ::= 0..20
def range2 ::= -10..10

then numbers like 0 do not have a unique minimal type.

To compensate for this constraint we can use the union type to get the same effect as the above (invalid) declaration as below.

def range11 ::= 0..10
def range12 ::= 11..20
def range21 ::= -10..-1
def range1 == range11 || range12
def range2 == range21 || range11

The first three of the above type definitions ensure that every integer between -10 and 20 has a unique minimal type, range11, range12 or range21. However, range1 and range2, now union types, capture the required range of integers. If range1 is given as a ? moded argument type of a relation any integer in either of its minimal subtypes range11 and range12 may be given or returned as a call value.

For constructor enumerator types the problem is worse. Consider the following example where the first enumeration is completely contained in the second.

def constr1(T) ::= f(T) | g(T)
def constr2(T) ::= f(T) | g(T) | h(T)

Which of constr1(int) and constr2(nat) is the smaller type?

For this reason we do not allow any overlaps in constructor type enumerations.

Again, for pragmatic reasons, we also do not allow the constructor functors to be members of atom enumeration types as this can easily lead to confusion.

For similar reasons we also do not allow the union of parameterised types as in the (invalid) example below.

def constr1(T) ::= f(T) | g(T)
def constr2(T) ::=  h(T)
def constr3(T) == constr1(T) || constr2(T)

We feel that it is unlikely that a programmer will need to have constructor types that violate the above constraints but in the situation where they need such types we suggest using constuctors with similarly named functors and then defining a relation that maps between terms of each type.