|
|
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 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 variables 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 Clean 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, 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-patterns. 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 Clean 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 variables (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 Clean 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 Clean 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 names 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. 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 names 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 Clean 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 Clean 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, Clean’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
modules, the concrete definition has to be given in the corresponding
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
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.