Chapter 5
Defining New Types


Defining Algebraic Data Types


Defining Record Types


Defining Synonym Types


Defining Abstract Data Types

Clean is a strongly typed language: every object (graph) and function (graph rewrite rule) in Clean has a type. The basic type system of Clean is based on the classical po­ly­mor­p­hic Mil­ner/Hindley/Mycroft (Milner  1978; Hindley 1969, Mycroft, 1984) type sys­tem. This type sys­tem is adapted for graph rewrit­ing sys­tems and extended with basic types, (possibly ex­is­tentially and universally quanti­fied) algebraic ty­pes, record types, ab­stract 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 im­plementation module.





// see 5.1




// see 5.2




// see 5.3




// 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 in­troduced 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 con­struc­tor must unambigu­ously have been (pre) defined in an algebraic data type definition  Sev­eral data con­struc­tors can be introduced in one al­gebraic data type defini­tion which makes it possible to define alter­native data structures of the same al­gebraic 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 quanti­fied, see below) type variables to the type constructors on the left-hand side of the algebraic data type definition. The argu­ments of the data constructor in a type definition are type instances of ty­pes (that are defined or are being de­fi­ned).

Types can be preceded by uniqueness type attributes (see Chapter 9). The argu­ments of a defined data con­structor can optionally be annotated as being strict (see 5.1.5).





= ConstructorDef




{| ConstructorDef} ;




[*] TypeConstructor {TypeVariable}









 [ExistentalQuantVariables] ConstructorName {BrackType}



 [ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}


















[UniversalQuantVariables] [Strict] [UnqTypeAttrib] SimpleType



E.{TypeVariable }+:



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 Clean ty­pes (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 in­fix­fix constructor;, in a similar way as function op­era­tors (with fixity (infixl, infixr or just infix, default infixl) and prece­dence (0 through 9, default 9). If infix construc­tors are surrounded by brackets they can also be used in prefix posi­tion (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 or­di­nary prefix construc­tors (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 de­fi­ned in the scope must have different names, to make type inferencing possible.


Scope of type definitions.


implementation module XYZ


:: Type_contructor type_vars = expression




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 op­tional ar­gu­ments which on its turn can contain sub-patterns. A constructor pattern forces evalua­tion of the cor­responding actual argument to strong root normal form since the strategy has to deter­mine whe­ther the actual ar­gument indeed is equal to the speci­fied constructor.





// Zero arity Constructor



(Constructor {Pattern})

// Constructor pattern



GraphPattern ConstructorName GraphPattern

// Infix Constructor opera­tor


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 con­structor 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 ty­pes. Higher order types can be constructed by curried applications of the type constructors. Higher or­der types can be applied in the type world in a similar way as higher order functi­ons in the function world. The use of higher order types increases the flexibility with which al­gebraic types can be defined. Predefi­ned types can also be used in curried way (see 4.5). Higher or­der 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 Clean each top-level type should have kind X. A top-level type is a type that occurs either as an argu­ment or result type of a function or as argument type of a data constructor (in some algebraic type de­finition). 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 al­ge­braic type defi­nition can contain existen­tially quantified type variable s (or, for short, existential type variables) (Läufer   1992). These special vari­a­bles are defined on the right-hand side of the type definition and are indicated by preceding them with “E..;”.   Exis­tential types are use­ful if one wants to create (recursive) data struc­tures in which objects of different ty­pes are being stored (e.g. a list with elements of different ty­pes).





= ConstructorDef




{| ConstructorDef} ;



ExistentalQuantVariables] ConstructorName {BrackType}



[ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}





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 compo­nents 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. The­re­fore, a function having an existentially quantified data structure as input is not al­lowed to make specific type assumptions on the parts that correspond to the existential type va­ri­ables. This implies that one can only instantiate an existen­tial 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 al­ge­braic type defi­nition can contain universally quantified type variables (or, for short, universal type variables) of Rank 2 (on the argument position of a data constructor). These special vari­a­bles 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).





= ConstructorDef




{| ConstructorDef} ;



[ExistentalQuantVariables] ConstructorName {BrackType}



ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}



[UniversalQuantVariables] [Strict] [UnqTypeAttrib] SimpleType



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

Functio­nal 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 chang­ing lazy data structures into strict ones. This has to be done by hand in the definition of the type.





= ConstructorDef




{| ConstructorDef} ;



[ExistentalQuantVariables] ConstructorName {BrackType}



[ExistentalQuantVariables] (ConstructorName) [Fix][Prec] {BrackType}





In the type definition of a constructor (in an algebraic data type definition or in a defini­tion of a re­cord 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 rea­son­ing 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 exam­ined. 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 cre­ated in a lazy context, the compiler will insert code that will take care of the eval­ua­tion 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 in­stances 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 ar­gument is put in a strict context while the argument is defined in terms of another strict annotated data struc­ture the latter is put in a strict context as well and there­fore also eval­uated. So, one can change the default lazy semantics of Clean into a (hyper) strict se­man­tics  as de­manded. The type system will check the consis­tency of types and ensure that the speci­fied strict­ness is maintai­ned.

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 con­struc­tor 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 con­structors can be used in a curried way in the function world, but then they have to be used as ordi­nary prefix constructors.

Type constructors can be used in a curried way in the type world; to use predefined bracket-like type construc­tors (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 argu­ments 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 con­crete type (= not a type variable) when a data struc­ture 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. Spe­cial about records is that a field name  is attached to each of the arguments of the data con­structor 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 con­ve­nience because the field names enable selection by field name instead of selection by posi­tion  When a re­cord is created all arguments of the constructor have to be defined but one can spec­ify 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 Clean in such a way that after a change in the structure of a record only those functions have to be chan­ged 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 op­tio­n­ally be annotated as being strict (see 10.1). The op­tional uni­queness at­tri­butes are treated in Chapter 9.




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

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

The se­mantic 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 ori­en­ted 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}


    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}


    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 se­lected by field name rather than by position.








         Simple Records

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




{[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 re­cord

                               , p = { x = px

                                     , y = py



A record can only be used if its type has been defined in a record type definition; the field names used must be identi­cal to the field names specified in the cor­re­spond­ing type.

When creating a record explicitly, the order in which the record fields are instantiated is irrele­vant, but all fields have to get a value; the type of these values must be an instantiation of the corre­sponding 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 speci­fied 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 up­date).




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










The record expression must yield a record.

The re­cord written to the left of the & (r & f = v is pronounced as: r with for f the value v) is the re­cord to be duplicated. On the right from the & the structures are specified in which the new record dif­fers from the old one. A structure can be any field of the record or a selection of any field or array ele­ment of a record or array stored in this record. All other fields are duplicated and cre­ated implicitly. Notice that the functional update is not an update in the classi­cal, de­struc­tive sense since a new record is cre­ated. However, when the given record is of unique type *T, the update is done de­structively (!) which in this particular case is safe since the original record is known not to be used any­more (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 ar­guments.


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




RecordExpr  [.TypeName].FieldName {Selection}



RecordExpr  [.TypeName]!FieldName {Selection}







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 selec­tion 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 con­tents one would like to use in the right-hand side need to be mentioned in the pattern.




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

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

The field names specified in the pattern must be identi­cal to the field names specified in the cor­re­spond­ing 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 speci­fied 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}




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.




::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 al­lowed.


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 Clean definition module (see Chapter 2). For soft­ware engineering reasons it sometimes better only to export the name of a type but not its con­crete de­finition (the right-hand side of the type definition). The type then becomes an abstract data type. In Clean this is done by specifying only the left-hand-side of a type in the definition mo­dule while the concrete definition (the right-hand side of the type definition) is hidden in the imple­mentation mo­d­ule. So, Clean’s module structure is used to hide the actual implementation. When one wants to do so­me­thing useful with objects of ab­stract types one needs to export func­tions that can create and mani­pu­late objects of this type as well.

Abstract data type def­initions are only allowed in definition modules, the con­crete 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 va­ri­a­ble names) the left-hand side of the abstract type definition (inclusive strictness and unique­ness type attributes).




::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 sur­rounded by brackets:




::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.