Chapter 5
Defining New Types

5.1 | Defining Algebraic Data Types
5.2 | Defining Record Types
5.3 | Defining Synonym Types
5.4 | Defining Abstract Data Types

C lean is a strongly typed language: every object (graph) and function (graph rewrite rule) in C lean has a type. The basic type system of C lean is based on the classical polymorphic Milner/Hindley/Mycroft (Milner 1978; Hindley 1969, Mycroft, 1984) type system. This type system is adapted for graph rewriting systems and extended with basic types, (possibly existentially and universally quantified) algebraic types, record types, abstract types and synonym types.

New types can be defined in an implementation as well as in a definition module. Types can only be defined on the global level. Abstract types can only be defined in a definition module hiding the actual implementation in the corresponding implementation module.

TypeDef | = | AlgebraicTypeDef | // see 5.1
| | | RecordTypeDef | // see 5.2
| | | SynonymTypeDef | // see 5.3
| | | AbstractTypeDef | // see 5.4

## 5.1 Defining Algebraic Data Types

With an algebraic data type one assigns a new type constructor (a new type) to a newly introduced data structure. The data structure consists of a new constant value (called the data constructor) that can have zero or more arguments (of any type). Every data constructor must unambiguously have been (pre) defined in an algebraic data type definition Several data constructors can be introduced in one algebraic data type definition which makes it possible to define alternative data structures of the same algebraic data type. The data constructors can, just like functions, be used in a curried way. Also type constructors can be used in a curried way, albeit only in the type world of course.

Polymorphic algebraic data types can be defined by adding (possibly existentially or universally quantified, see below) type variable s to the type constructors on the left-hand side of the algebraic data type definition. The arguments of the data constructor in a type definition are type instances of types (that are defined or are being defined).

Types can be preceded by uniqueness type attributes (see Chapter 9). The arguments of a defined data constructor can optionally be annotated as being strict (see 5.1.5).

AlgebraicTypeDef | = | ::TypeLhs | = ConstructorDef
|  |  | {| ConstructorDef} ;

TypeLhs | = | [*] TypeConstructor {TypeVariable}
TypeConstructor | = | TypeName
ConstructorDef | = | [ExistentalQuantVariables] ConstructorName {BrackType}
| | | [ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}
Fix | = | infixl
| | | infixr
| | | infix
Prec | = | Digit
BrackType | = | [UniversalQuantVariables] [Strict] [UnqTypeAttrib] SimpleType
ExistentalQuantVariables | = | E.{TypeVariable }+:
UniversalQuantVariables | = | A.{TypeVariable }+:

Example of an algebraic type definition and its use.

::Day = Mon | Tue | Wed | Thu | Fri | Sat | Sun

::Tree a = NilTree

| NodeTree a (Tree a) (Tree a)

MyTree:: (Tree Int) // constant function yielding a Tree of Int

MyTree = NodeTree 1 NilTree NilTree

An algebraic data type definition can be seen as the specification of a grammar in which is specified what legal data objects are of that specific type. Notice that all other C lean types (basic, list, tuple, array, record, abstract types) can be regarded as special cases of an algebraic type.

Constructors with two arguments can be defined as infix constructor.ib.infix constructor;, in a similar way as function operators (with fixity (infixl, infixr or just infix, default infixl) and precedence (0 through 9, default 9). If infix constructors are surrounded by brackets they can also be used in prefix position (see 3.1 and 3.4). In a pattern match they can be written down in infix position as well.

When a constructor operator is used in infix position (in an expression or in a in a pattern) both arguments have to be present. Constructor operators can be used in a curried way, but then they have to be used as ordinary prefix constructors (see 3.1 and 3.4).

Algebraic type definition and constructor pattern in function definition.

::Tree2 a = (/\) infixl 0 (Tree a) (Tree a)

| Value a

Mirror:: (Tree2 a) -> Tree2 a

Mirror (left/\right) = Mirror right/\Mirror left

Mirror leaf = leaf

Example of an algebraic type defining an infix data constructor and a function on this type; notice that one cannot use a ‘:’ because this character is already reserved.

::List a = (<:>) infixr 5 a (List a)

| Nil

Head:: (List a) -> a

Head (x<:>xs) = x

All data constructors being defined in the scope must have different names, to make type inferencing possible.

Scope of type definitions.

implementation module XYZ

:: Type_contructor type_vars = expression

other_definitions

### 5.1.1 Using Constructors in Patterns

An algebraic data type can be used in a pattern. The pattern consists of the data constructor (see 3.2) with its optional arguments which on its turn can contain sub-pattern s. A constructor pattern forces evaluation of the corresponding actual argument to strong root normal form since the strategy has to determine whether the actual argument indeed is equal to the specified constructor.

GraphPattern | = | Constructor | // Zero arity Constructor
| | | (Constructor {Pattern}) | // Constructor pattern
| | | GraphPattern ConstructorName GraphPattern | // Infix Constructor operator

Example of an algebraic data type definition and its use in a pattern in function definition.

::Tree a = Node a (Tree a) (Tree a)

| Nil

Mirror:: (Tree a) -> Tree a

Mirror (Node e left right) = Node e (Mirror right) (Mirror left)

Mirror Nil = Nil

The data constructor used in a patter must have been defined in an algebraic data type definition.

### 5.1.2 Using Higher Order Types

In an algebraic type definition ordinary types can be used (such as a basic type, e.g. Int, or a list type, e.g. [Int], or an instantiation of a user defined type, e.g. Tree Int), but one can also use higher order types. Higher order types can be constructed by curried applications of the type constructors. Higher order types can be applied in the type world in a similar way as higher order functions in the function world. The use of higher order types increases the flexibility with which algebraic types can be defined. Predefined types can also be used in curried way (see 4.5). Higher order types play an important role in combination with type classes (see Chapter 6).

Of course, one needs to ensure that all types are applied in a correct way. To be able to specify the rules that indicate whether a type itself is correct, we introduce the notion of kind. A kind can be seen as the ‘type of a type‘. In our case, the kind of a type expresses the number of type arguments this type may have. The kind X stands for any so-called first-order type: a type expecting no further arguments ((Int, Bool, [Int], etcetera). All function arguments are of kind X. The kind X -> X stands for a type that can be applied to a (first-order) type, which then yields another first-order type, X -> X -> X expects two type arguments, and so on.

In C lean each top-level type should have kind X. A top-level type is a type that occurs either as an argument or result type of a function or as argument type of a data constructor (in some algebraic type definition). The rule for determining the kinds of the type variables (which can be of any order) is fairly simple: The kind of a type variable directly follows from its use. If a variable has no arguments, its kind is X. Otherwise its kind corresponds to the number of arguments to which the variable is applied. The kind of type variable determines its possible instantiations, i.e. it can only be instantiated with a type, which is of the same kind as the type variable itself.

Example of an algebraic type using higher order types; the type variable t in the definition of Tree2 s of kind X -> X. Tree2 is instantiated with a list (also of kind X -> X) in the definition of MyTree2.

::Tree2 t = NilTree

| NodeTree (t Int) (Tree2 t) (Tree2 t)

MyTree2:: Tree2 []

MyTree2 = NodeTree [1,2,3] NilTree NilTree

### 5.1.3 Defining Algebraic Data Types with Existentially Quantified Variables

An algebraic type definition can contain existentially quantified type variable s (or, for short, existential type variables) (Läufer 1992). These special variables are defined on the right-hand side of the type definition and are indicated by preceding them with “E..;”. Existential types are useful if one wants to create (recursive) data structures in which objects of different types are being stored (e.g. a list with elements of different types).

AlgebraicTypeDef | = | ::TypeLhs | = ConstructorDef
|  |  | {| ConstructorDef} ;
ConstructorDef | = | ExistentalQuantVariables] ConstructorName {BrackType}
| | | [ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}
ExistentalQuantVariables | = | E.{TypeVariable}+:

Example of the use of an existentially quantified type. In this example a record (see 5.2) is defined containing an existentially quantified state s, a method to change this state s, and a method to convert the state s into a String. Notice that upon creation of the record MyObject the type of the internal state and the methods defined on the state are consistent (in this case the state is of type Int). The methods stored in the object Object can (only) be applied on the state of that object thus enabling an object-oriented style of programming. The concrete type of the state hidden in the object is not visible from outside. To show it to the outside world one has to convert the state, which can be of any type, to an ordinary not existentially quantified type. For instance, PrintState converts the any state into a String. Objects that have states of different type are considered to be of the same type and can for instance be part of the same list.

::Object = E.s: {state::s, method::s->s, tostring:: s -> String }

MyObject = { state = 3

, method = (+) 1

, tostring = toString

}

IncrementObject obj=:{method,state} = {obj & state = method state}

PrintState obj=:{tostring,state} = tostring state

Start = PrintState (IncrementObject MyObject) // the result will be 4

To ensure correctness of typing, there is a limitation imposed on the use of existentially quantified data structures.

Once a data structure containing existentially quantified parts is created the type of these components are forgotten. This means that, in general, if such a data structured is passed to another function it is statically impossible to determine the actual types of those components: it can be of any type. Therefore, a function having an existentially quantified data structure as input is not allowed to make specific type assumptions on the parts that correspond to the existential type variables. This implies that one can only instantiate an existential type variable with a concrete type when the object is created. In all other cases it can only be unified with a universally quantified type.

Counter Example. Illegal use of an object with existentially quantified components.

Start = (IncrementObject MyObject).state

### 5.1.4 Defining Algebraic Data Types with Universally Quantified Variables

An algebraic type definition can contain universally quantified type variable s (or, for short, universal type variables) of Rank 2 (on the argument position of a data constructor). These special variables are defined on the right-hand side of a type definition on the arguments position of the data constructor being defined and have to be preceded by an “A..;” (meaning: "for all"). It can be used to store polymorphic functions that work on arguments of 'any' type. The universal type is very useful for constructing dictionaries for overloaded functions (see Chapter 6).

AlgebraicTypeDef | = | ::TypeLhs | = ConstructorDef
|  |  | {| ConstructorDef} ;
ConstructorDef | = | [ExistentalQuantVariables] ConstructorName {BrackType}
| | | ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}
BrackType | = | [UniversalQuantVariables] [Strict] [UnqTypeAttrib] SimpleType
UniversalQuantVariables | = | A.{TypeVariable }+:

Counter Example. The following program is ill typed. Although an identity function is stored in T2, T2 can contain any function that can be unified with b -> b (for instance Int -> Int will do). Therefore a type error is given for f2 since g is applied to both an Int and a Char.

:: T2 b = C2 (b -> b)

f2:: (T2 b) -> (Int,Char)

f2 (C2 g) = (g 1, g 'a')

Id::a -> a

Id x = x

Start = f2 (C2 Ids)

Example of the use of a universally quantified type. In contrast with the example above it is now specified that T must contain a universally quantified function b -> b. The identity function Id can be stored in T, since its type Id::a -> a is actually a shorthand for Id::A.a:a -> a. A function from Int -> Int cannot be stored in T since this type is not unifiable with A.a:a -> a.

:: T = C (A.b: b -> b)

f:: (T b) -> (Int,Char)

f (C g) = (g 1, g 'a')

Id::a -> a

Id x = x

Start = f (C Ids)

### 5.1.5 Strictness Annotations in Type Definitions

Functional programs will generally run much more efficient when strict data structures are being used instead of lazy ones. If the inefficiency of your program becomes problematic one can think of changing lazy data structures into strict ones. This has to be done by hand in the definition of the type.

AlgebraicTypeDef | = | ::TypeLhs | = ConstructorDef
|  |  | {| ConstructorDef} ;
ConstructorDef | = | [ExistentalQuantVariables] ConstructorName {BrackType}
| | | [ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}
Strict | = | ! |

In the type definition of a constructor (in an algebraic data type definition or in a definition of a record type) the arguments of the data constructor can optionally be annotated as being strict. So, some arguments can be defined strict while others can be defined as being lazy. In reasoning about objects of such a type it will always be true that the annotated argument will be in strong root normal form when the object is examined. Whenever a new object is created in a strict context, the compiler will take care of the evaluation of the strict annotated arguments. When the new object is created in a lazy context, the compiler will insert code that will take care of the evaluation whenever the object is put into a strict context. If one makes a data structure strict in a certain argument, it is better not define infinite instances of such a data structure to avoid non-termination.

So, in a type definition one can define a data constructor to be strict in zero or more of its arguments. Strictness is a property of data structure that is specified in its type.

In general (with the exceptions of tuples) one cannot arbitrary mix strict and non-strict data structures because they are considered to be of different type.

When a strict annotated argument is put in a strict context while the argument is defined in terms of another strict annotated data structure the latter is put in a strict context as well and therefore also evaluated. So, one can change the default lazy semantics of C lean into a (hyper) strict semantics as demanded. The type system will check the consistency of types and ensure that the specified strictness is maintained.

There is no explicit notation for creating unboxed versions of an algebraic data type. The compiler will automatically choose the most efficient representation for a given data type. For algebraic data type definitions containing strict elements of basic type, record type and array type an unboxed representation will be chosen.

Example: both integer values in the definition of Point are strict and will be stored unboxed since they are known to be of basic type. The integer values stored in MyPoint are strict as well, but will be stored unboxed since MyTuple is polymorphic.

::Point = (!Int,!Int)

::MyTuple a = Pair !a !a

::MyPoint :== MyTuple Int

A user defined lazy list similar to type [a] could be defined in algebraic type definition as follows:

::LazyList a = LazyCons a (LazyList a)

| LazyNil

A head strict list similar to type [!a] could be defined in algebraic type definition as follows:

::HeadSList a = HeadSCons !a (HeadSList a)

| HeadSNil

A tail strict list similar to type [a!] could be defined in algebraic type definition as follows:

::TailSList a = TailSCons a !(TailSList a)

| TailSNil

A strict listssimilar to type [!a!] could be defined in algebraic type definition as follows:

::StrictList a = StrictCons !a !(StrictList a)

| StrictNil

An unboxed list similar to type [#Int] could be defined in algebraic type definition as follows:

::UnboxedIList = UnboxedICons !Int UnboxedIList

| UnboxedINil

An unboxed list similar to type [#Int!] could be defined in algebraic type definition as follows:

::UnboxedIList = UnboxedICons !Int !UnboxedIList

| UnboxedINil

### 5.1.6 Semantic Restrictions on Algebraic Data Types

Other semantic restrictions on algebraic data types:

The name of a type must be different from other names in the same scope and name space (see 2.1).

The name of a type variable must be different from other type variable names in the same scope and name space

All type variables used on the right-hand side are bound, i.e. must either be introduced on the left-hand side of the algebraic type being defined, or they must be bound by an existential quantifier on the right-hand side, or, they must be bound by a universal quantifier specified on the corresponding argument.

A data constructor can only be defined once within the same scope and name space. So, each data constructor unambiguously identifies its type to make type inferencing possible.

When a data constructor is used in infix position both arguments have to be present. Data constructors can be used in a curried way in the function world, but then they have to be used as ordinary prefix constructors.

Type constructors can be used in a curried way in the type world; to use predefined bracket-like type constructors (for lists, tuples, arrays) in a curried way they must be used in prefix notation.

The right-hand side of an algebraic data type definition should yield a type of kind X, all arguments of the data constructor being defined should be of kind X as well.

A type can only be instantiated with a type that is of the same kind.

An existentially quantified type variable specified in an algebraic type can only be instantiated with a concrete type (= not a type variable) when a data structure of this type is created.

## 5.2 Defining Record Types

A record type is basically an algebraic data type in which exactly one constructor is defined. Special about records is that a field name is attached to each of the arguments of the data constructor and that

records cannot be used in a curried way.

Compared with ordinary algebraic data structures the use of records gives a lot of notational convenience because the field names enable selection by field name instead of selection by position When a record is created all arguments of the constructor have to be defined but one can specify the arguments in any order. Furthermore, when pattern matching is performed on a record, one only has to mention those fields one is interested in (see 5.2.2). A record can be created via a functional update (see 5.2.1). In that case one only has to specify the values for those fields that differ from the old record. Matching and creation of records can hence be specified in C lean in such a way that after a change in the structure of a record only those functions have to be changed that are explicitly referring to the changed fields.

Existential and universal type variables (see 5.1.3 and 5.1.4) are allowed in record types (as in any other type). The arguments of the constructor can optionally be annotated as being strict (see 10.1). The optional uniqueness attributes are treated in Chapter 9.

RecordTypeDef | = | ::TypeLhs = [ExistentalQuantVariables] [Strict] {{FieldName :: [Strict] Type}-list} ;

As data constructor for a record the name of the record type is used internally.

The semantic restrictions that apply for algebraic data types also hold for record types.

The field names inside one record all have to be different. It is allowed to use the same field name in different records. If the same names are used in different records, one can explicitly specify the intended record type when the record is constructed.

Example of a record definition.

::Complex = { re :: Real

, im :: Real

}

The combination of existential type variables in record types are of use for an object oriented style of programming.

Example of the use of an existentially quantified record. One can create an object of a certain type that can have different representations.

::Object = E.x: { state :: x

, get :: x -> Int

, set :: x Int -> x

}

CreateObject1:: Object

CreateObject1 = {state = [], get = myget, set = myset}

where

myget:: [Int] -> Int

myget [i:is] = i

myget [] = 0

myset:: [Int] Int -> [Int]

myset is i = [i:is]

CreateObject2 = {state = 0.0, get = myget, set = myset}

where

myget:: Real -> Int

myget r = toInt r

myset:: Real Int -> Real

myset r i = r + toReal i

Get:: Object -> Int

Get {state,get} = get state

Set:: Object Int -> Object

Set o=:{state,set} i = {o & state = set state i}

Start:: [Object]

Start = map (Set 3) [CreateObject1,CreateObject2]

Example of a complex number as record type with strict components.

::Complex = { re:: !Real

, im:: !Real

}

(+) infixl 6:: !Complex !Complex -> Complex

(+) {re=r1,im=i1} {re=r2,im=i2} = {re=r1+r2,im=i1+i2}

The compiler often unboxes records to make the generated code more efficient. However in some cases this is less efficient, for example for abstract data types, large unique records that can be updated in place, or when records are shared. Therefore unboxing can be prevented by adding an ! before the { in the record type definition.

### 5.2.1 Creating Records and Selection of Record Fields

A record is a tuple-like algebraic data structure that has the advantage that its elements can be selected by field name rather than by position.

Record | = | RecordDenotation
| | | RecordUpdate

#### Simple Records

The first way is to create a record is by explicitly defining a value for each of its fields.

RecordDenotation | = | {[TypeName|] {FieldName = GraphExpr}-list]}

Creation of a record.

::Point = { x:: Real // record type definition

, y:: Real

}

::ColorPoint = { p:: Point // record type definition

, c:: Color

}

::Color = Red | Green | Blue // algebraic type definition

CreateColorPoint:: (Real,Real) Color -> ColorPoint // type of function

CreateColorPoint (px,py) col = { c = col // function creating a new record

, p = { x = px

, y = py

}

}

A record can only be used if its type has been defined in a record type definition; the field name s used must be identical to the field names specified in the corresponding type.

When creating a record explicitly, the order in which the record fields are instantiated is irrelevant, but all fields have to get a value; the type of these values must be an instantiation of the corresponding type specified in record type definition. Curried use of records is not possible.

When creating a record, its type constructor that can be used to disambiguate the record from other records; the type constructor can be left out if there is at least one field name is specified which is not being defined in some other record.

#### Record Update

The second way is to construct a new record out of an existing one (a functional record update).

RecordUpdate | = | {[TypeName|][RecordExpr &][{FieldName {Selection} = GraphExpr}-list]}
Selection | = | .FieldName
| | | .ArrayIndex
RecordExpr | = | GraphExpr

The record expression must yield a record.

The record written to the left of the & (r & f = v is pronounced as: r with for f the value v) is the record to be duplicated. On the right from the & the structures are specified in which the new record differs from the old one. A structure can be any field of the record or a selection of any field or array element of a record or array stored in this record. All other fields are duplicated and created implicitly. Notice that the functional update is not an update in the classical, destructive sense since a new record is created. However, when the given record is of unique type *T, the update is done destructively (!) which in this particular case is safe since the original record is known not to be used anymore (see 9.2). The functional update of records is performed very efficient such that we have not added support for destructive updates of records of unique type. The &-operator is strict in its arguments.

Updating a record within a record using the functional update.

MoveColorPoint:: ColorPoint (Real,Real) -> ColorPoint

MoveColorPoint cp (dx,dy) = {cp & p.x = cp.p.x + dx, p.y = c.p.y + dy}

#### Selection of a Record Field

RecordSelection | = | RecordExpr [.TypeName].FieldName {Selection}
| | | RecordExpr [.TypeName]!FieldName {Selection}
Selection | = | .FieldName
| | | .ArrayIndex

With a record selection (using the ‘.’ symbol) one can select the value stored in the indicated record field. A “unique” selection using the ‘!’ symbol returns a tuple containing the demanded record field and the original record. This type of record selection can be very handy for destructively updating of uniquely typed records with values that depend on the current contents of the record. Record selection binds more tightly (priority 11) than application (priority 10).

Record selection.

GetPoint:: ColorPoint -> Point

GetPoint cp = cp.p // selection of a record field

GetXPoint:: ColorPoint -> Real

GetXPoint cp = cp.p.x // selection of a record field

GetXPoint2:: *ColorPoint -> (Real,.ColorPoint)

GetXPoint2 cp = cp!p.x // selection of a record field

### 5.2.2 Record Patterns

An object of type record can be specified as pattern. Only those fields which contents one would like to use in the right-hand side need to be mentioned in the pattern.

RecordPattern | = | {[TypeName |] {FieldName [= GraphPattern]}-list}

The type of the record must have been defined in a record type definition.

The field name s specified in the pattern must be identical to the field names specified in the corresponding type.

When matching a record, the type contructor which can be used to disambiguate the record from other records, can only be left out if there is at least one field name is specified which is not being defined in some other record.

Use of record patterns.

::Tree a = Node (RecTree a)

| Leaf a

::RecTree a = { elem :: a

, left :: Tree a

, right :: Tree a

}

Mirror:: (Tree a) -> Tree a

Mirror (Node tree=:{left=l,right=r}) = Node {tree & left=r,right=l}

Mirror leaf = leaf

The first alternative of function Mirror defined in another equivalent way.

Mirror (Node tree) = Node {tree & left=tree.right,right=tree.left}

or

Mirror (Node tree=:{left,right}) = Node {tree & left=right,right=left}

## 5.3 Defining Synonym Types

Synonym types permit the programmer to introduce a new type name for an existing type.

SynonymTypeDef | = | ::TypeLhs :== [UniversalQuantVariables]Type ;

For the left-hand side the same restrictions hold as for algebraic types.

Cyclic definitions of synonym types (e.g. ::T a b :== G a b; ::G a b :== T a b) are not allowed.

Example of a type synonym definition.

::Operator a :== a a -> a

map2:: (Operator a) [a] [a] -> [a]

map2 op [] [] = []

map2 op [f1:r1] [f2:r2] = [op f1 f2 :map2 op r1 r2]

Start:: Int

Start = map2 (*) [2,3,4,5] [7,8,9,10]

## 5.4 Defining Abstract Data Types

A type can be exported by defining the type in a C lean definition module (see Chapter 2). For software engineering reasons it sometimes better only to export the name of a type but not its concrete definition (the right-hand side of the type definition). The type then becomes an abstract data type. In C lean this is done by specifying only the left-hand-side of a type in the definition module while the concrete definition (the right-hand side of the type definition) is hidden in the implementation module. So, C lean’s module structure is used to hide the actual implementation. When one wants to do something useful with objects of abstract types one needs to export functions that can create and manipulate objects of this type as well.

Abstract data type definitions are only allowed in definition module s, the concrete definition has to be given in the corresponding implementation module.i.implementation module;.

The left-hand side of the concrete type should be identical to (modulo alpha conversion for variable names) the left-hand side of the abstract type definition (inclusive strictness and uniqueness type attributes).

AbstractTypeDef | = | ::TypeLhs ;

Example of an abstract data type.

definition module stack

::Stack a

Empty :: (Stack a)

isEmpty :: (Stack a) -> Bool

Top :: (Stack a) -> a

Push :: a (Stack a) -> Stack a

Pop :: (Stack a) -> Stack a

implementation module stack

::Stack a :== [a]

Empty:: (Stack a)

Empty = []

isEmpty:: (Stack a) -> Bool

isEmpty [] = True

isEmpty s = False

Top:: (Stack a) -> a

Top [e:s] = e

Push:: a (Stack a) -> Stack a

Push e s = [e:s]

Pop:: (Stack a) -> Stack a

Pop [e:s] = s

### 5.4.1 Defining Abstract Data Types with Synonym Type Definition

Because the concrete definition of an abstract data type does not appear in the definition module, the compiler cannot generate optimal code. Therefore, if the concrete type is a synonym type, the right-hand-side of the definition may be included surrounded by brackets:

AbstractSynonymTypeDef | = | ::TypeLhs ( :== [UniversalQuantVariables] Type ) ;

The type of the implementation is still hidden as for other abstract data types, except that the compiler uses it only to generate the same code as for a synonym type.