diff options
Diffstat (limited to 'miralib/manual/20')
| -rw-r--r-- | miralib/manual/20 | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/miralib/manual/20 b/miralib/manual/20 new file mode 100644 index 0000000..2ca09d5 --- /dev/null +++ b/miralib/manual/20 @@ -0,0 +1,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. + |