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.
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
6
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
7
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
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
8
Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
9
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
10
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
11
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
12
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
13
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
14
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
15
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)
16
Data Types
Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
17
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
Show simply allows us to take a type and represent it as a string.
Haskell Definition
class Show a where
show :: a -> [Char]
This is implemented for all of the built-in types such as Int, Bool, and Char
Show
18
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
This is implemented for all of the built-in types such as Int, Bool, and Char
19
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
2 Reflexivity: x ≤ x
3 Antisymmetry: x ≤ y ∧ y ≤ x → x = y
4 Totality (total order): x ≤ y ∨ y ≤ x
20
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
4 Negation (equality): x ̸= y → ¬(x = y)
5 Substitutivity (equality): x = y → f x = f y
21
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
22
, 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
23
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
Maybe
Haskell Definition
— Maybe :: * -> *
data Maybe a = Just a
| Nothing
24
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
List
Haskell Definition
— List :: * -> *
25
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
Haskell List
Definition
— [ ] :: * -> *
data [a] = a : (List a)
| []
26
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
Tree
Haskell Definition
— Tree :: * -> *
27
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
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
1 Associativity: (a•(b•c))=((a•b)•c) Example
instance Semigroup [a] where
(<>) = (++)
28
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
1 Identity: (mempty • x) = x = (x • mempty) Example
instance Monoid [a] where
mempty = []
29
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).
30
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
31
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).
32
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)) Additionally Prove
1 forallxs: [] ++ xs == xs
2 forallxs: xs ++ [] == xs
(done in editor)
33
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)
First Prove for all ys: reverse (ys ++ [x]) = x:reverse ys (done in editor)
34
Data Types Type Clases I Type Parameters Type Classes II Inductive Proofs Homework
35
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
36
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