[ Pobierz całość w formacie PDF ]
.FURTHER ML6.4 Type de nitionsWe have promised that ML has facilities for declaring new type constructors,so that composite types can be built up out of existing ones.In fact, ML goesfurther and allows a composite type to be built up not only out of preexistingtypes but also from the composite type itself.Such types, naturally enough, aresaid to be recursive.They are declared using the type keyword followed by anequation indicating how the new type is built up from existing ones and itself.We will illustrate this by a few examples.The rst one is the de nition of a sumtype, intended to correspond to the disjoint union of two existing types.#type ('a, ' b)sum = inl of ' a | inr of ' bType sum defined.Roughly, an object of type ( ' a, ' b)sum is either something of type ' a orsomething of type ' b.More formally, however, all these things have di erenttypes.The type declaration also declares the so-called constructors inl and inr.These are functions that take objects of the component types and inject theminto the new type.Indeed, we can see their types in the ML system and applythem to objects:#inl- : ' a -> (' a, ' b) sum =#inr- : ' a -> (' b, ' a) sum =#inl 5- : (int, 'a) sum = inl 5#inr false- : (' a, bool) sum = inr falseWe can visualize the situation via the following diagram.Given two existingtypes and , the type ( )sum is composed precisely of separate copies ofand , and the two constructors map onto the respective copies:( )sumXXXXX inlXXXXXXXzX:inr 6.4.TYPE DEFINITIONS 71This is similar to a union in C, but in ML the copies of the component typesare kept apart and one always knows which of these an element of the unionbelongs to.By contrast, in C the component types are overlapped, and theprogrammer is responsible for this book-keeping.6.4.1 Pattern matchingThe constructors in such a de nition have three very important properties:They are exhaustive, i.e.every element of the new type is obtainable eitherby inl x for some x or inr y for some y.That is, the new type containsnothing besides copies of the component types.They are injective, i.e.an equality test inl x = inl y is true if and onlyif x = y, and similarly for inr.That is, the new type contains a faithfulcopy of each component type without identifying any elements.They are distinct, i.e.their ranges are disjoint.More concretely this meansin the above example that inl x = inr y is false whatever x and y mightbe.That is, the copy of each component type is kept apart in the new type.The second and third properties of constructors justify our using patternmatching.This is done by using more general varstructs as the arguments ina lambda, e.g.#fun (inl n) -> n > 6| (inr b) -> b- : (int, bool) sum -> bool =This function has the property, naturally enough, that when applied to inl n itreturns n > 6 and when applied to inr b it returns b.It is precisely because ofthe second and third properties of the constructors that we know this does givea wellde ned function.Because the constructors are injective, we can uniquelyrecover n from inl n and b from inr b.Because the constructors are distinct,we know that the two clauses cannot be mutually inconsistent, since no value cancorrespond to both patterns.In addition, because the constructors are exhaustive, we know that each valuewill fall under one pattern or the other, so the function is de ned everywhere.Actually, it is permissible to relax this last property by omitting certain patterns,though the ML system then issues a warning:#fun (inr b) -> bToplevel input:>fun (inr b) -> b>^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.- : (' a, ' b) sum -> ' b = 72 CHAPTER 6.FURTHER MLIf this function is applied to something of the form inl x, then it will notwork:#let f = fun (inr b) -> bToplevel input:>let f = fun (inr b) -> b> ^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.f : (' a, ' b) sum -> ' b =#f (inl 3)Uncaught exception: Match_failure ("", 452, 468)Though booleans are built into ML, they are e ectively de ned by a rathertrivial instance of a recursive type, often called an enumerated type, where theconstructors take no arguments:#type bool = false | trueIndeed, it is perfectly permissible to de ne things by matching over the truthvalues [ Pobierz całość w formacie PDF ]
zanotowane.pl doc.pisz.pl pdf.pisz.pl matkasanepid.xlx.pl
.FURTHER ML6.4 Type de nitionsWe have promised that ML has facilities for declaring new type constructors,so that composite types can be built up out of existing ones.In fact, ML goesfurther and allows a composite type to be built up not only out of preexistingtypes but also from the composite type itself.Such types, naturally enough, aresaid to be recursive.They are declared using the type keyword followed by anequation indicating how the new type is built up from existing ones and itself.We will illustrate this by a few examples.The rst one is the de nition of a sumtype, intended to correspond to the disjoint union of two existing types.#type ('a, ' b)sum = inl of ' a | inr of ' bType sum defined.Roughly, an object of type ( ' a, ' b)sum is either something of type ' a orsomething of type ' b.More formally, however, all these things have di erenttypes.The type declaration also declares the so-called constructors inl and inr.These are functions that take objects of the component types and inject theminto the new type.Indeed, we can see their types in the ML system and applythem to objects:#inl- : ' a -> (' a, ' b) sum =#inr- : ' a -> (' b, ' a) sum =#inl 5- : (int, 'a) sum = inl 5#inr false- : (' a, bool) sum = inr falseWe can visualize the situation via the following diagram.Given two existingtypes and , the type ( )sum is composed precisely of separate copies ofand , and the two constructors map onto the respective copies:( )sumXXXXX inlXXXXXXXzX:inr 6.4.TYPE DEFINITIONS 71This is similar to a union in C, but in ML the copies of the component typesare kept apart and one always knows which of these an element of the unionbelongs to.By contrast, in C the component types are overlapped, and theprogrammer is responsible for this book-keeping.6.4.1 Pattern matchingThe constructors in such a de nition have three very important properties:They are exhaustive, i.e.every element of the new type is obtainable eitherby inl x for some x or inr y for some y.That is, the new type containsnothing besides copies of the component types.They are injective, i.e.an equality test inl x = inl y is true if and onlyif x = y, and similarly for inr.That is, the new type contains a faithfulcopy of each component type without identifying any elements.They are distinct, i.e.their ranges are disjoint.More concretely this meansin the above example that inl x = inr y is false whatever x and y mightbe.That is, the copy of each component type is kept apart in the new type.The second and third properties of constructors justify our using patternmatching.This is done by using more general varstructs as the arguments ina lambda, e.g.#fun (inl n) -> n > 6| (inr b) -> b- : (int, bool) sum -> bool =This function has the property, naturally enough, that when applied to inl n itreturns n > 6 and when applied to inr b it returns b.It is precisely because ofthe second and third properties of the constructors that we know this does givea wellde ned function.Because the constructors are injective, we can uniquelyrecover n from inl n and b from inr b.Because the constructors are distinct,we know that the two clauses cannot be mutually inconsistent, since no value cancorrespond to both patterns.In addition, because the constructors are exhaustive, we know that each valuewill fall under one pattern or the other, so the function is de ned everywhere.Actually, it is permissible to relax this last property by omitting certain patterns,though the ML system then issues a warning:#fun (inr b) -> bToplevel input:>fun (inr b) -> b>^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.- : (' a, ' b) sum -> ' b = 72 CHAPTER 6.FURTHER MLIf this function is applied to something of the form inl x, then it will notwork:#let f = fun (inr b) -> bToplevel input:>let f = fun (inr b) -> b> ^^^^^^^^^^^^^^^^Warning: this matching is not exhaustive.f : (' a, ' b) sum -> ' b =#f (inl 3)Uncaught exception: Match_failure ("", 452, 468)Though booleans are built into ML, they are e ectively de ned by a rathertrivial instance of a recursive type, often called an enumerated type, where theconstructors take no arguments:#type bool = false | trueIndeed, it is perfectly permissible to de ne things by matching over the truthvalues [ Pobierz całość w formacie PDF ]