User defined data types – part 1 Level of difficulty of this handout
This handout includes material of easy, medium, hard and advanced level. If some of the material feels difficult, it is probably because it is difficult rather than your fault. This means you have to work hard if you want to achieve a high mark in the module, as is the case for all modules.
Video lectures for this handout
The following videos are also linked at appropriate points of this handout for your convenience.
Copyright By PowCoder代写 加微信 powcoder
1. Introduction, the booleans revisited, isomorphisms, Weekdays and the new Maybe type constructor (35 min) 2. Type retracts (13 min)
3. Either and And and pairs (9 min)
4. Lists revisited (9 min)
5. Binary trees (12 min)
6. Directions, addresses and paths in binary trees (15 min) 7. Traversals in binary trees (10 min)
8. Inverting traversals (18 min)
Total 2hrs.
Experimenting with the Haskell code included here
You should experiment with the Haskell code in theses notes in order to achieve full understanding. This means running the code and adding things to it, such as solutions of exercises and puzzles, or your own brilliant ideas.
These lecture notes are in markdown format including Haskell code. To get the Haskell code out of the markdown code, we can use the program mdtohs.hs included in the Resources directory, as follows in a Unix/Linux terminal:
$ cat Data1.md | runhaskell ../../Resources/mdtohs.hs > Data1.hs
This means “copy the contents of the file Data1.md to the standard input of the Haskell program mdtohs.hs and store the output of the program in the file Data1.hs”. This can be equivalently written as
$ runhaskell ../../Resources/mdtohs.hs < Data1.md > Data1.hs
This removes all the markdown code and keeps only the Haskell code, so that we can work with it.
We have already run this for you, and the file Data1.hs is available in this GitLab repository. Make your own copy of this file to avoid conflicts when we update it.
How to run Data1.hs with ghci
The import System.Random will fail if we don’t specify which package it comes from, which is random. You specify this as follows: $ ghci -package random Data1.hs
Haskell imports in these lecture notes
Any needed library imports should be mentioned here at the top of the file. We need the following for generating random inputs for testing:
module Data1 where
import System.Random
Type synonyms
User defined data types The booleans revisited Type isomorphisms
Some important type constructors
The Maybe type constructor Type retracts
The Either type constructor
The And type constructor, defined by ourselves Lists revisited
Implementing some basic operations on lists An aside on accumulators
Binary trees
Basic functions on binary trees
Directions, addresses and paths in binary trees Proofs on binary trees by induction
Traversals in binary trees
Inverting traversals (generating trees)
Type synonyms
A video discussing the next few sections is available on Canvas.
Sometimes, mainly for the sake of clarity, we may wish to give a new name to an existing type. For example, the Haskell prelude defines a
string to be a list of characters:
type String = [Char]
Since String is just a type synonym, operations such as list concatenation and reverse (++) :: [a] -> [a] -> [a]
reverse :: [a] -> [a]
can be freely applied to strings:
> “abc” ++ reverse “def”
Type synonyms can also have parameters, as in e.g.
type Lst a = [a]
User defined data types
The booleans revisited
The booleans are defined as follows in Haskell, in the prelude:
data Bool = False | True
This defines a new type, called Bool, with two elements (or constructors), called False and True: False :: Bool
True :: Bool
Functions over a data type can be conveniently defined by pattern-matching on its constructors. For example, in the prelude, the conjunction operation
(&&) :: Bool -> Bool -> Bool
is defined as follows:
False && _ = False True &&x=x
A slightly subtle aspect of the semantics of pattern-matching in Haskell is that:
1. the different pattern-matching clauses are tried in order from top to bottom, and
2. the input arguments of the function are only evaluated to the extent needed to check whether they match the current pattern.
A consequence of this semantics is that the above definition of conjunction implements short-circuit evaluation: if the first argument is False,
then the function returns False without even evaluating the second argument.
In contrast, consider the following alternative definition of conjunction:
conj :: Bool -> Bool -> Bool
conj False False = False
conj False True = False
conj True False = False
conj True True = True
This version does not implement short-circuit evaluation: the second argument will always be evaluated regardless of the value of the first. We can observe the difference between these two versions of conjunction by running the following experiment in the GHC interpreter:
> False && undefined
> False `conj` undefined
*** Exception: Prelude.undefined
#CallStack (from HasCallStack):
error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
undefined, called at
Type isomorphisms
Let’s introduce another data type BW defined by data BW = Black | White
This type is isomorphic to the type Bool, via the type-conversion functions
bw2bool :: BW -> Bool
bw2bool Black = False
bw2bool White = True
bool2bw :: Bool -> BW
bool2bw False = Black
bool2bw True = White
That the pair of functions (bw2bool,bool2bw) is an isomorphism means that they are mutually inverse, in the sense that bw2bool(bool2bw b) = b
forallb :: Bool,and bool2bw(bw2bool c) = c
forallc :: BW.
Type isomorphisms should not be confused with type synonyms. For example, if we try to directly use a value of type BW where a value of type
Bool is expected, we get a type error: > let test = Black && True
• Couldn’t match expected type ‘Bool’ with actual type ‘BW’
• In the first argument of ‘(&&)’, namely ‘Black’
In the expression: Black && True
In an equation for ‘it’: it = Black && True
On the other hand, if we wrap up the values using the explicit coercions bw2bool and bool2bw, then everything checks: > let test = bool2bw (bw2bool Black && True)
Of course, the names Black and White are arbitrary, and there is another isomorphism between BW and Bool that swaps Black with True and White with False instead.
bw2bool’ :: BW -> Bool
bw2bool’ Black = True
bw2bool’ White = False
bool2bw’ :: Bool -> BW
bool2bw’ False = White
bool2bw’ True = both of the types Bool and BW are of course isomorphic (again in two different ways each) to the type data Bit = Zero | One
of binary digits. One of the isomorphisms is the following:
bit2Bool :: Bit -> Bool
bool2Bit :: Bool -> Bit
bit2Bool Zero = False
bit2Bool One = True
bool2Bit False = Zero
bool2Bit True = One
Another one is the following:
bit2Bool’ :: Bit -> Bool
bool2Bit’ :: Bool -> Bit
bit2Bool’ Zero = True
bit2Bool’ One = False
bool2Bit’ False = One
bool2Bit’ True = Zero
Note: The syntax rules of Haskell require that both type names (here Bool, BW, Bit) and constructor names (here False, True, Black, White, Zero, One) should start with a capital letter.
Another example of a data type is
data WeekDay = Mon | Tue | Wed | Thu | Fri | Sat | Sun
We can ask Haskell to do some jobs for free for us (there are alternative ways of doing them ourselves with our own sweat, using type class instances, which we will discuss later):
data WeekDay = Mon | Tue | Wed | Thu | Fri | Sat | Sun
deriving (Show, Read, Eq, Ord, Enum)
This automatically adds the type WeekDay to the type classes with these five names, which give functions
show :: WeekDay -> String
read :: String -> WeekDay
(==) :: WeekDay -> WeekDay -> Bool
(<), (>), (<=), (>=) :: WeekDay -> WeekDay -> Bool
succ, pred :: WeekDay -> WeekDay
Look this up in our adopted textbook. Notice that show is the counterpart of Java’s toString, and read does the opposite. Some examples are:
> show Tue
> read “Tue” :: WeekDay — (the type annotation tells Haskell to try to parse the string as a WeekDay)
> read “Dog” :: WeekDay
*** Exception: Prelude.read: no parse
> Mon == Tue
> Mon < Tue
> succ Mon
> pred Tue
> [Mon .. Fri]
[Mon,Tue,Wed,Thu,Fri]
Monday doesn’t have a predecessor, and Sunday doesn’t have a successor:
> pred Mon
*** Exception: pred{WeekDay}: tried to take `pred’ of first tag in enumeration
CallStack (from HasCallStack):
error, called at Data1.hs:20:47 in main:Main
> succ Sun
*** Exception: succ{WeekDay}: tried to take `succ’ of last tag in enumeration
CallStack (from HasCallStack):
error, called at Data1.hs:20:47 in main:Main
Notice that the choice of names in the type of weekdays is arbitrary. An equally good, isomorphic definition is
data WeekDay’ = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday
Some important type constructors The Maybe type constructor
Sometimes a function may not be able to give a result, in which case we would like it to say explicitly that it cannot. We use the Maybe type from the prelude for that purpose:
data Maybe a = Nothing | Just a
Here a is a type parameter, and we have the following types for Nothing and Just:
Nothing :: Maybe a
Just :: a -> Maybe a
ThismeansthattheconstructorJustisafunction.ItconvertsanelementoftypeaintoanelementoftypeMaybe a.SothisfunctionJustis a so-called type coercion, also known as a type cast.
For example:
Just 17 :: Maybe Integer
Insummary,theonlypossibleelementsofthetypeMaybe aareNothingandJust xwherexhastypea.
In Java the Maybe type constructor is called Optional. Example: integer computations that may give errors
In the following definition of division, if the denominator is zero, then division is impossible, and so the result is Nothing. If it is possible, we simplyperformthedivision,andweconverttheresultingInttoMaybe IntusingthetypeconversionfunctionJust,whichthengivesthe result of the function dive:
dive :: Int -> Int -> Maybe Int
x `dive` y = if y == 0 then Nothing else Just (x `div` y)
For example, we get
> 10 `dive` 2
> 10 `dive` 0
Butnowsupposeyouwanttodo3 + (10 `dive` 0).YouwouldexpectNothingbutinsteadthisexpressiondoesn’teventypecheck: > 3 + (10 `dive` 0)
• No instance for (Num (Maybe Int)) arising from a use of ‘+’
• In the expression: 3 + (5 `dive` 0)
In an equation for ‘it’: it = 3 + (5 `dive` 0)
Whatthisissayingisthat(10 `div` 0)isexpectedtobeanInt,because+expectsanIntasitsrightargument,butitisn’t.That’sbecause
itisaMaybe Int.Soweneedaversionofadditionthatcancopewitherrorsasitspossibleinputs:
adde :: Maybe Int -> Maybe Int -> Maybe Int
adde Nothing Nothing = Nothing
adde Nothing (Just y) = Nothing
adde (Just x) Nothing = Nothing
adde (Just x) (Just y) = Just (x + y)
Nowtofix3 + (5 `dive` 0)wereplace+byadde,butalsoweneedtoconvertthenumber3tothetypeMaybe Intwiththetype
coercion or type cast Just.
> Just 3 `adde` (10 `dive` 2)
> Just 3 `adde` (10 `dive` 0)
A more concise definition of adde:
adde’ :: Maybe Int -> Maybe Int -> Maybe Int
adde’ (Just x) (Just y) = Just (x+y)
adde’ _ _ = Nothing
This works because the execution of Haskell programs tries patterns from top to bottom, and the last pattern catches all remaining possibilities.
A definition using cases is also possible:
adde” :: Maybe Int -> Maybe Int -> Maybe Int
adde” xm ym = case xm of
Nothing -> Nothing Justx ->caseymof
Nothing -> Nothing
Just y -> Just (x+y)
Later we will see that there is a much more concise way of making such definitions using monads. But for now we will stick to pattern matching and cases.
Example: find the first position an element occurs in a list
Since the first position is undefined if the element doesn’t occur in the list, in that case we answer Nothing:
firstPosition :: Eq a => a -> [a] -> Maybe Integer
firstPosition x [] = Nothing
firstPosition x (y:ys)
For example:
| x == y = Just 0
| otherwise = case firstPosition x ys of
Nothing -> Nothing
Just n -> Just(n+1)
> firstPosition ‘a’ [‘a’..’z’]
> firstPosition ‘b’ [‘a’..’z’]
> firstPosition ‘z’ [‘a’..’z’]
> firstPosition ‘!’ [‘a’..’z’]
which we summarize as
firstPosition ‘a’ [‘a’..’z’] = Just 0
firstPosition ‘b’ [‘a’..’z’] = Just 1
firstPosition ‘z’ [‘a’..’z’] = Just 25
firstPosition ‘!’ [‘a’..’z’] = Nothing
You are required to use the book to find out what case is and how it works in general, but in this example it should be clear. You are also required to use the book to find out about conditional definitions using | to indicate guards for equations.
We will use the Maybe type constructor very often, because there are many occasions in which some inputs are invalid. Task.DefineafunctionallPositions :: Eq a => a -> [a] -> [Int]thatfindsallpositionsinwhichanelementelementoccursina
list.Forexample,weshouldhaveallPositions 17 [13,17,17,666] = [1,2]andallPositions 17 [1,2,3] = [].
Type retracts
A video discussing this section is available.
This section may be rather hard at your current level. Consider it as a challenge. If you get lost, feel free to skip it at a first reading, go to the next section, and come back to it later. This is important because it deals with data coding, which is a crucial, aspect of Computer Science. What we say here is in Haskell, but it actually applies to any programming language.
We have already seen examples of type isomorphisms. For example, the type Bool is isomorphic to the type BW of black-and-white colours, and also to the type Bit of binary digits Zero and One.
More generally, an isomorphism of types a and b is a pair of functions f :: a -> b
g :: b -> a
suchthat*f (g y) = yforally :: b,and*g (f x) = xforallx :: a.
We summarize these two equations by saying that these two functions are mutually inverse. This means that we can convert back and forth between elements of the type a and elements of the type b, like we did when we converted False to Zero and True to One. You can think of fandgasrenamingfunctions:thefunctionf = bit2Boolrenamesabittoaboolean,andthefunctiong = bool2Bitrenamesaboolean to a bit.
In practice, this means that it doesn’t matter whether we work with the type Bool with elements True and False, or the type Bit with elements Zero and One. In fact, computers work by exploting this identification of booleans with binary digits.
There is another relationship between types that is also useful in practice: a type b can “live” inside another type a, in the sense of having a “copy” in the type a. A simple example is that the type Bool has a copy inside the type Int:
bool2Int :: Bool -> Int
bool2Int False = 0
bool2Int True = 1
Not only do we have a copy of Bool inside Int, but also we can go back, so that we get False and True from 0 and 1:
int2Bool :: Int -> Bool
int2Bool n | n == 0 = False
| otherwise = True
However, notice that not only 1 is converted back to True, but also everything other than 0 is converted to True. We have
int2Bool (bool2Int y) = y
foreveryy :: Bool,butwedon’thavebool2Int (int2Bool x) = xforallx :: Int,asthisfailsfore.g.x = 17becausebool2Int
(int2Bool 17)is1ratherthan17.
We can say that there is enough room in the type integers for it to host a copy of the type of booleans, but there isn’t enough room in the type
of booleans for it to host a copy of the type of integers.
When there are functions
f :: a -> b
g :: b -> a
suchthat*f (g y) = yforally :: b,
butnotnecessarilyg (f x) = xforallx :: a,wesaythatthetypebisaretractofthetypea
Our discussion above shows that the type Bool is a retract of the type Int. This retraction is the same as that performed in the programming
language C, where the integer 0 codes False and everything else codes True.
But notice that there are other ways in which the type Bool lives inside the type Int as a retract: for example, we can send False to 13 and
True to 17, and then send back everything bigger than 15 to True and everything else to False. We are free to code things as we wish.
Task.ShowthatthetypeMaybe aisaretractofthetype[a].TheideaisthatNothingcorrespondstotheemptylist[]andthatJust x corresponds to the one-element list [x]. Make this idea precise by writing back and forth functions between these types so that they exhibit Maybe aasaretractof[a].Ouradoptedtextbookexploitssucharetractionoften,albeitwithoutmakingitexplicit.Infact,whatthebook doesveryoftenistoavoidthetypeMaybe aandinsteadworkwiththetype[a],consideringonlythelist[](correspondingtoNothing)and singletonlists[x](correspondingtoJust x),andignoringlistsoflength2orgreater.(Thereasonthebookdoesthatistoavoidmonads (before they are taught) in favour of list comprehensions (which are taught early on), as list comprehensions happen to accomplish the same thing as “do notation” for monads, in the particular case of the list monad. So this coding is done for pedagogical purposes in this case.)
If we have a type retraction (f,g) as above, then: * f is a surjection.
This means that for every `y :: b` there is __at least one__ `x :: a` with `f x = y`.
For example, in the case of the booleans as a retract of the
integers, this means that every boolean is coded by at least one integer.
g is an injection.
Thismeansthatforeveryx :: athereisatmostoney :: bwithg y = x.
Inthefirstexampleofthebooleansasaretractoftheintegers,thisisthecase:*Forx = 0wehaveexactlyoneywithbool2Int y = x, namelyy=False.*Forx = 1wehaveexactlyoneywithbool2Int y = x,namelyy=True.*Forxdifferentfrom0and1wehavenoy withbool2Int y = x.
So for every x there is at most one such y (i.e. exactly one or none). Task. Define
data WorkingWeekDay = Mon’ | Tue’ | Wed’ | Thu’ | Fri’
We add primes to the names because the names without prime are already used as elements of the type WeekDay defined above. Show that the type WorkingWeekDay is a retract of the type WeekDay. Arbitrary choices will need to be performed in one direction, like e.g. the
language C arbitrarily decides that any integer other than 0 codes true. Puzzle. Consider the function
g :: Integer -> (Integer -> Bool)
g y = \x -> x == y
We can visualize g in the following table:
… -5 -4 … -1 0 1 … 4 5 …
g(-5)= … True False … False False False … False False … g(-4)= … False True … False False False … False False … …
g(-1)= … False False … True False False … False False …
g(0)= … False False … False True False … False False …
g(1)= … False False … False False True … False False …
g(4)= … False False … False False False … True False …
g(5)= … False False … False False False … False True …
Thatis,thefunctiongcodestheintegeryasthefunctionhsuchthath y = Trueandh x = Falseforxotherthany.Convinceyourself thatthefunctiongisaninjection.Inthissense,thetypeIntegerlivesinsidethefunctiontypeInteger -> Bool.Doyouthinkghasa companionf : (Integer -> Bool) -> Integerthat”decodes”functionsInteger -> Boolbacktointegers,suchthatforanycodeg yoftheintegerywegettheintegerbackasf (g y) = y?Ifyes,thengiveaHaskelldefinitionofsuchanfandconvinceyourselfthat indeedf (g y) = yforallintegersy.Ifnot,why?Thispuzzleisrathertricky,andnoneofthepossibleanswers”yes”or”no”tothequestion is obvious.
The Either type constructor
A video discussing the next few sections is available on Canvas.
It is defined in the prelude as follows:
data Either a b = Left a | Right b
Then we have
Left ::a->Eitherab Right :: b -> Either a b
For example:
Left 17 :: Either Integer String
Right “abd” :: Either Integer String
TheideaisthatthetypeEither a bisthedisjointunionofthetypesaandb,wherewetagtheelementsofawithLeftandthoseofbwith Right in the union type. An example of its use is given below.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com