程序代写代做代考 compiler flex graph Haskell Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
1
Software System Design and Implementation
Induction, Data Types and Type Classes Practice
Curtis Millar
CSE, UNSW (and Data61) 10 June 2020

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
2
data Point = Point Float Float
deriving (Show, Eq)
data Vector = Vector Float Float
deriving (Show, Eq)
movePoint :: Point -> Vector -> Point
movePoint (Point x y) (Vector dx dy)
= Point (x + dx) (y + dy)
Product Types

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
3
data Colour = Colour { redC
, greenC
:: Int
:: Int
:: Int
Records
, blueC
, opacityC :: Int
} deriving (Show, Eq)

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
4
data LineStyle = Solid
| Dashed
| Dotted
deriving (Show, Eq)
data FillStyle = SolidFill | NoFill
deriving (Show, Eq)
Sum Types

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
5
Constructors are how an value of a particular type is created.
Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
6
Constructors are how an value of a particular type is created.
data Bool = True | False
Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
7
Constructors are how an value of a particular type is created.
data Bool = True | False
data Int = .. | -1 | 0 | 1 | 2 | 3 | ..
Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
8
Constructors are how an value of a particular type is created.
data Bool = True | False
data Int = .. | -1 | 0 | 1 | 2 | 3 | ..
data Char = ‘a’ | ‘b’ | ‘c’ | ‘d’ | ‘e’ | ..
Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
9
data Point = Point Float Float
deriving (Show, Eq)
data Vector = Vector Float Float
deriving (Show, Eq)
Custom Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
10
data Point = Point Float Float
deriving (Show, Eq)
data Vector = Vector Float Float
deriving (Show, Eq)
Here, Point and Vector are both constructors.
Custom Constructors

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
11
Algebraic Data Types
Just as the Point constructor took two Float arguments, constructors for sum types can take parameters too, allowing us to model different kinds of shape:
data PictureObject
= Path [Point] Colour LineStyle
| Circle Point Float Colour LineStyle FillStyle
| Polygon [Point] Colour LineStyle FillStyle
| Ellipse Point Float Float Float
Colour LineStyle FillStyle
deriving (Show, Eq)
type Picture = [PictureObject]
Here, type creates a type alias which provides only an alternate name that refers to an existing type.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
12
Patterns in Function Definitions

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
13
Patterns in Function Definitions
1 Patterns are used to deconstruct an value of a particular type.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
1
2
Patterns are used to deconstruct an value of a particular type.
A pattern can be a binding to a hole ( ), a name, or a constructor of the type.
Patterns in Function Definitions
14

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
1
2 3
Patterns are used to deconstruct an value of a particular type.
A pattern can be a binding to a hole ( ), a name, or a constructor of the type. When defining a function, each argument is bound using a separate pattern.
Patterns in Function Definitions
15

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
16
if’ :: Bool -> a -> a -> a
if’ True then’ _ = then’
if’ False _ else’ = else’
Patterns in Function Definitions

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
17
Patterns in Function Definitions
factorial :: Int -> Int
factorial 0 = 1
factorial n = n * factorial (n – 1)

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
18
isVowel :: Char -> Bool
isVowel ‘a’ = True
isVowel ‘e’ = True
isVowel ‘i’ = True
isVowel ‘o’ = True
isVowel ‘u’ = True
isVowel _ = False
Patterns in Function Definitions

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs
Homework
19
Records and Accessors
data Colour = Colour { redC :: Int, greenC :: Int
, blueC :: Int, opacityC :: Int
}
— Is equivalent to
data Color = Color Int Int Int Int
redC
greenC
blueC
opacityC (Color _ _ _ o) = o
(Color r _ _ _) = r
(Color _ g _ _) = g
(Color _ _ b _) = b

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
20
factorial :: Int -> Int
factorial x =
case x of 0 -> 1
n -> n * factorial (n – 1)
Patterns in Expressions

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
21
Newtype
newtype allows you to encapsulate an existing type to add constraints or properties without adding runtime overhead.
newtype Kilometers = Kilometers Float
newtype Miles = Miles Float
kilometersToMiles :: Kilometers -> Miles
kilometersToMiles (Kilometers kms) = Miles $ kms / 1.60934
milesToKilometers :: Miles -> Kilometers
milesToKilometers (Miles miles) = Kilometers $ miles * 1.60934

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
22
data Nat = Zero
| Succ Nat
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ a) b = add a (Succ b)
zero = Zero
one = Succ Zero
two = add one one
Natural Numbers

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
23
data Nat = Zero
| Succ Nat
Natural Numbers
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ a) b = add a (Succ b)
zero = Zero
one = Succ Zero
two = add one one
1 Nat is recursive as it has the (Succ) constructor which takes a Nat.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
24
data Nat = Zero
| Succ Nat
Natural Numbers
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ a) b = add a (Succ b)
zero = Zero
one = Succ Zero
two = add one one
1 Nat is recursive as it has the (Succ) constructor which takes a Nat.
2 Nat has the Zero constructor which does not recurse and acts like a base case.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
More Cool Graphics
Example (Live Coding of Fractal Trees)
25

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
26
Type Classes

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
27
Type Classes
1 A type class has nothing to do with OOP classes or inheritance.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
28
1
2
Type Classes
A type class has nothing to do with OOP classes or inheritance.
Type classes describe a set of behaviours that can be implemented for any type.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
29
1
2 3
Type Classes
A type class has nothing to do with OOP classes or inheritance.
Type classes describe a set of behaviours that can be implemented for any type.
A function or type class instance can operate on a type variable constrained by a type class instead of a concrete type.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
30
1
2 3
4
Type Classes
A type class has nothing to do with OOP classes or inheritance.
Type classes describe a set of behaviours that can be implemented for any type.
A function or type class instance can operate on a type variable constrained by a type class instead of a concrete type.
A type class is similar to an OOP interface.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
31
1
2 3
4 5
Type Classes
A type class has nothing to do with OOP classes or inheritance.
Type classes describe a set of behaviours that can be implemented for any type.
A function or type class instance can operate on a type variable constrained by a type class instead of a concrete type.
A type class is similar to an OOP interface.
When creating an instance of a type class with laws, you must ensure the laws are held manually (they cannot be checked by the compiler).

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
32
1
2 3
4 5
6
Type Classes
A type class has nothing to do with OOP classes or inheritance.
Type classes describe a set of behaviours that can be implemented for any type.
A function or type class instance can operate on a type variable constrained by a type class instead of a concrete type.
A type class is similar to an OOP interface.
When creating an instance of a type class with laws, you must ensure the laws are held manually (they cannot be checked by the compiler).
When using a type class with laws you can assume that all laws hold for all instances of the type class.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
33
Show simply allows us to take a type and represent it as a string.
Show

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Show simply allows us to take a type and represent it as a string.
Haskell Definition
class Show a where
show :: a -> [Char]
Show
34

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
36
Read
Effectively the ’dual’ of Show, Read allows us to take a string representation of a value and decode it.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Read
Effectively the ’dual’ of Show, Read allows us to take a string representation of a value and decode it.
You can think of read as having the following definition, but it is actually somewhat more complex.
Definition
class Read a where
read :: [Char] -> a
37

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
39
Ord
Ord allows us to compare two values of a type for a partial or total inequality.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Ord
Ord allows us to compare two values of a type for a partial or total inequality.
Haskell Definition
class Ord a where
(<=) :: a -> a -> Bool
1 Tranisitivity: x ≤ y ∧ y ≤ z → x ≤ z
41

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
45
Eq
Eq allows us to compare two values of a type for an equivalence or equality.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Eq
Eq allows us to compare two values of a type for an equivalence or equality.
Haskell Definition
class Eq a where
(==) :: a -> a -> Bool
1 Reflexivity: x = x
2 Symmetry: x =y →y =x
3 Tranisitivity: x = y ∧ y = z → x = z
49

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
52
Derived Instances
When defining a new type we can have the compiler generate instances of Show, Read, Ord, or Eq with the deriving statement at the end of the definition.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Derived Instances
When defining a new type we can have the compiler generate instances of Show, Read, Ord, or Eq with the deriving statement at the end of the definition.
Haskell Example
data Colour = Colour { redC
, greenC
:: Int
:: Int
:: Int
54
, blueC
, opacityC :: Int
} deriving (Show, Eq)
Derived instances of Ord will be total orders and will order by fields in the order they appear in a product type and will order constructors in the same order they are defined.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Derived Instances
When defining a new type we can have the compiler generate instances of Show, Read, Ord, or Eq with the deriving statement at the end of the definition.
Haskell Example
data Colour = Colour { redC
, greenC
:: Int
:: Int
:: Int
55
, blueC
, opacityC :: Int
} deriving (Show, Eq)
Derived instances of Ord will be total orders and will order by fields in the order they appear in a product type and will order constructors in the same order they are defined. Derived instances of Eq will be strict equalities.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
56
Kinds of Types

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
57
Kinds of Types
1 Just as values and functions in the runtime language of Haskell have types, types in the type language of Haskell have kinds.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
58
1
2
Just as values and functions in the runtime language of Haskell have types, types in the type language of Haskell have kinds.
The kind of a concrete type is *.
Kinds of Types

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
59
1
2 3
Just as values and functions in the runtime language of Haskell have types, types in the type language of Haskell have kinds.
The kind of a concrete type is *.
Just as functions exist over values (with the type a -> b), type constructors exist for types.
Kinds of Types

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
60
1
2 3
4
Just as values and functions in the runtime language of Haskell have types, types in the type language of Haskell have kinds.
The kind of a concrete type is *.
Just as functions exist over values (with the type a -> b), type constructors exist
for types.
* -> * is a type constructor that takes a concrete type and produces a concrete type.
Kinds of Types

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
61
Maybe

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Haskell Definition
— Maybe :: * -> *
data Maybe a = Just a
| Nothing
Maybe
62

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Maybe
Haskell Definition
— Maybe :: * -> *
data Maybe a = Just a
| Nothing
63
1 Maybe is a type constructor that takes a type and produces a type that may or may not hold a value.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Maybe
Haskell Definition
— Maybe :: * -> *
data Maybe a = Just a
| Nothing
64
1 Maybe is a type constructor that takes a type and produces a type that may or may not hold a value.
2 Maybe Int is a concrete type that may or may not hold an Int.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
65
List

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Haskell Definition
— List :: * -> *
data List a = Cons a (List a)
| Nil
List
66

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List
Haskell Definition
— List :: * -> *
67
data List a = Cons a (List a)
| Nil
1 List a is recursive as it has the (Cons) constructor which takes a List a.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List
Haskell Definition
— List :: * -> *
68
data List a = Cons a (List a)
| Nil
1 List a is recursive as it has the (Cons) constructor which takes a List a.
2 List a has the Nil constructor which does not recurse and acts like a base case.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List
Haskell Definition
— List :: * -> *
69
data List a = Cons a (List a)
| Nil
1 List a is recursive as it has the (Cons) constructor which takes a List a.
2 List a has the Nil constructor which does not recurse and acts like a base case.
3 List is a type constructor that takes a type and produces a type that holds zero or more of a value.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List
Haskell Definition
— List :: * -> *
70
data List a = Cons a (List a)
| Nil
1 List a is recursive as it has the (Cons) constructor which takes a List a.
2 List a has the Nil constructor which does not recurse and acts like a base case.
3 List is a type constructor that takes a type and produces a type that holds zero or more of a value.
4 List Int is a concrete type that zero or more values of type Int.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
71
Haskell List

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Definition
— [ ] :: * -> *
data [a] = a : (List a)
| []
Haskell List
72

Data Types Type Clases I Type Parameters Type Classes II
Inductive Proofs
Homework
Haskell List
Definition
— [ ] :: * -> *
data [a] = a : (List a)
| []
73
1 [a, b, c] is syntactic sugar for the constructor (a :
(b :
(c :
[]))).

Data Types Type Clases I Type Parameters Type Classes II
Inductive Proofs
Homework
Haskell List
Definition
— [ ] :: * -> *
data [a] = a : (List a)
| []
74
1 [a, b, c] is syntactic sugar for the constructor (a :
2 “abc” is syntactic sugar for the constructor (’a’ :
(b : (’b’ :
[]))).
(c :
(’c’ : []))).

Data Types Type Clases I Type Parameters Type Classes II
Inductive Proofs
Homework
Haskell List
Definition
— [ ] :: * -> *
data [a] = a : (List a)
| []
75
1 [a, b, c] is syntactic sugar for the constructor (a :
2 “abc” is syntactic sugar for the constructor (’a’ :
3 Both can also be used as patterns.
(b : (’b’ :
[]))).
(c :
(’c’ : []))).

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
76
Tree

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Tree
Haskell Definition
— Tree :: * -> *
77
data Tree a = Node a (Tree a) (Tree a)
| Leaf

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Tree
Haskell Definition
— Tree :: * -> *
78
data Tree a = Node a (Tree a) (Tree a)
| Leaf
1 Tree a is recursive in the same manner as List a.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Tree
Haskell Definition
— Tree :: * -> *
79
data Tree a = Node a (Tree a) (Tree a)
| Leaf
1 Tree a is recursive in the same manner as List a.
2 Tree is a type constructor that takes a type and produces a type that holds zero or more of a value in a tree.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Tree
Haskell Definition
— Tree :: * -> *
80
data Tree a = Node a (Tree a) (Tree a)
| Leaf
1 Tree a is recursive in the same manner as List a.
2 Tree is a type constructor that takes a type and produces a type that holds zero
or more of a value in a tree.
3 Tree Int is a concrete type that holds zero or more values of type Int in a tree.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
81
Semigroup
A semigroup is a pair of a set S and an operation • : S → S → S where the operation • is associative.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
82
Semigroup
A semigroup is a pair of a set S and an operation • : S → S → S where the operation • is associative.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Semigroup
A semigroup is a pair of a set S and an operation • : S → S → S where the operation • is associative.
Haskell Definition
class Semigroup a where
(<>) :: a -> a -> a
83

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
86
Monoid
A monoid is a semigroup (S,•) equipped with a special identity element.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Monoid
A monoid is a semigroup (S,•) equipped with a special identity element.
Haskell Definition
class (Semigroup a) => Monoid a where
mempty :: a
87

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
90
Inductive Proofs
Suppose we want to prove that a property P(n) holds for all natural numbers n.

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Inductive Proofs
Suppose we want to prove that a property P(n) holds for all natural numbers n. Remember that the set of natural numbers N can be defined as follows:
Definition of Natural Numbers
1 0 is a natural number.
2 For any natural number n, n + 1 is also a natural number.
Therefore, to show P(n) for all n, it suffices to show:
1 P (0) (the base case), and
2 assuming P(k) (the inductive hypothesis), ⇒ P(k + 1) (the inductive case).
92

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
93
data Nat = Zero
| Succ Nat
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ a) b = add a (Succ b)
one = Succ Zero
two = Succ (Succ Zero)
Natural Numbers Example

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
data Nat = Zero
| Succ Nat
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ a) b = add a (Succ b)
one = Succ Zero
two = Succ (Succ Zero)
Example (1 + 1 = 2)
Prove one ‘add‘ one = two (done in editor)
Natural Numbers Example
94

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
Induction on Lists
Haskell lists can be defined similarly to natural numbers.
Definition of Haskell Lists
1 [] is a list.
2 For any list xs, x:xs is also a list (for any item x).
This means, if we want to prove that a property P(ls) holds for all lists ls, it suffices to show:
1 P([]) (the base case)
2 P(x:xs) for all items x, assuming the inductive hypothesis P(xs).
96

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
97
List Monoid Example
(++) :: [a] -> [a] -> [a]
(++) [] ys = ys — 1 (++)(x:xs)ys=x:xs++ys –2

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List Monoid Example
(++) :: [a] -> [a] -> [a]
(++) [] ys = ys — 1 (++)(x:xs)ys=x:xs++ys –2
Example (Monoid)
Prove for all xs, ys, zs: ((xs ++ ys) ++ zs) = (xs ++ (ys ++ zs))
98

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
List Reverse Example
(++) :: [a] -> [a] -> [a]
(++) [] ys = ys — 1 (++) (x:xs) ys = x : xs ++ ys — 2
reverse :: [a] -> [a]
reverse [] =[] –A reverse (x:xs) = reverse xs ++ [x] — B
Example
To Prove for all ls: reverse (reverse ls) == ls (done in editor)
100

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
102
Graphics and Artwork
data PictureObject
= Path [Point] Colour LineStyle
| Circle Point Float Colour LineStyle FillStyle
| Polygon [Point] Colour LineStyle FillStyle
| Ellipse Point Float Float Float
Colour LineStyle FillStyle
deriving (Show, Eq)
type Picture = [PictureObject]

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
103
Homework

Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
104
Homework
1 Last week’s quiz is due before on Friday. Make sure you submit your answers.

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
105
1
2
Last week’s quiz is due before on Friday. Make sure you submit your answers.
Do the first programming exercise, and ask us on Piazza if you get stuck. It is due by the start if my next lecture (in 7 days).
Homework

Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
106
1
2
3
Last week’s quiz is due before on Friday. Make sure you submit your answers.
Do the first programming exercise, and ask us on Piazza if you get stuck. It is due by the start if my next lecture (in 7 days).
This week’s quiz is also up, it’s due next Friday (in 9 days).
Homework

Related Posts