1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
_A_l_g_e_b_r_a_i_c_ _t_y_p_e_ _d_e_f_i_n_i_t_i_o_n_s
The simplest method of introducing a new data type into a Miranda script
is by means of an algebraic type definition. This enables the user to
introduce a new concrete data type with specified constructors. A
simple example would be
tree ::= Nilt | Node num tree tree
The `::=' sign is used to introduce an algebraic data type. This
definition introduces three new identifiers
`tree' a typename
`Nilt' a nullary constructor (i.e. an atom), of type tree
`Node' a constructor, of type num->tree->tree->tree
Now we can define trees using constructors Nilt & Node, for example
t = Node 3 Nilt Nilt
It is not necessary to have names for selector functions because the
constructors can be used in pattern matching. For example a function
for counting the number of nodes in a tree could be written
size Nilt = 0
size (Node a x y) = 1 + size x + size y
Note that the names of constructors _m_u_s_t_ _b_e_g_i_n_ _w_i_t_h_ _a_n_ _u_p_p_e_r_ _c_a_s_e_ _l_e_t_t_e_r
(and conversely, any identifier beginning with an upper case letter is
assumed to be a constructor).
An algebraic type can have any number (>=1) of constructors and each
constructor can have any number (>=0) fields, of specified types. The
number of fields taken by a constructor is called its `arity'. A
constructor of arity zero is said to be atomic. Algebraic types are a
very general idea and include a number of special cases that in other
languages require separate constructions.
One interesting case that all of the constructors can be atomic, giving
us what is called in PASCAL a `scalar enumeration type'. Example
day ::= Mon|Tue|Wed|Thu|Fri|Sat|Sun
The union of two types can also be represented as an algebraic data type
- for example here is a union of num and bool.
boolnum ::= Left bool | Right num
Notice that this is a `labelled union type' (the other kind of union
type, in which the parts of the union are not distinguished by tagging
information, is not permitted in Miranda).
An algebraic typename can take parameters, thus introducing a family of
types. This is done be using generic type variables as formal
parameters of the `::=' definition. To modify our definition of `tree'
to allow trees with different types of labels at the nodes (instead of
all `num' as above) we would write
tree * ::= Nilt | Node * (tree *) (tree *)
Now we have many different tree types - `tree num', `tree bool',
`tree([char]->[char])', and so on. The constructors `Node' and `Nilt'
are both polymorphic, with types `tree *' and `*->tree *->tree *->tree
*' respectively.
Notice that in Miranda objects of a recursive user defined type are not
restricted to being finite. For example we can define the following
infinite tree of type `tree num'
bigtree = Node 1 bigtree bigtree
_C_o_n_t_r_o_l_l_i_n_g_ _t_h_e_ _s_t_r_i_c_t_n_e_s_s_ _o_f_ _c_o_n_s_t_r_u_c_t_o_r_s
Definition - a function f is strict iff
f _| = _|
where _| is the value attributed to expressions which fail to terminate
or terminate with an error. To support non-strict functions the calling
mechanism must not evaluate the arguments before passing them to the
function - this is what is meant by "lazy evaluation".
In Miranda constructors are, by default, non-strict in all their fields.
Example
pair ::= PAIR num num
fst (PAIR a b) = a
snd (PAIR a b) = b
First note that there is a predefined identifier "undef" which denotes
undefined - evaluating "undef" in a Miranda session gives an error
message. Consider the following Miranda expressions:
fst (PAIR 1 undef)
snd (PAIR undef 1)
Both evaluate to `1', that is `PAIR' is non-strict in both arguments.
The primary reason for making constructors non-strict in Miranda is that
it is necessary to support equational reasoning on Miranda scripts. (In
the example given, elementary equational reasoning from the definition
of `fst' implies that `fst(PAIR 1 anything)' should always have the
value `1'.) It is also as a consequence of constructors being non-strict
that Miranda scripts are able to define infinite data structures.
It is, however, possible to specify that a given constructor of an
algebraic data type is strict in one or more fields by putting `!' after
the field in the `::=' definition of the type. For example we can
change the above script to make PAIR strict in both fields, thus
pair ::= PAIR num! num!
fst (PAIR a b) = a
snd (PAIR a b) = b
Now `fst (PAIR 1 undef)' and `snd (PAIR undef 1)' both evaluate to
undefined. It is a consequence of the `!' annotations that `PAIR a b'
is undefined when either a or b is undefined. It is also possible to
make PAIR strict in just one of its fields by having only one `!' in the
type definition.
In the case of a recursively defined algebraic type, if all the
constructors having recursive fields are made strict in those fields it
ceases to be possible to construct infinite objects of that type. It is
also possible to deny the possibility of certain infinite structures
while permitting others. For example if we modify the definition of the
tree type first given above as follows
tree ::= Nilt | Node num tree! tree
then it is still possible to construct trees which are infinite in their
right branch but not "left-infinite" ones.
The main reason for allowing `!' annotations on Miranda data type
definitions is that one of the intended uses of Miranda is as a SEMANTIC
METALANGUAGE, in which to express the denotational semantics of other
programming languages.
|
