Lecture - Functional Programming MT22, XI
Flashcards
What’s the difference between a $\text{data}$ decleration and a $\text{newtype}$ decleration in Haskell?
- $\text{data}$ defines lifted types
- $\text{newtype}$ defines unlifted types
What does it mean for a type to be lifted?
The type can have bottom $\bot$ as an element.
What is true about the definition of a fold on a non-recursive type?
It has no recursion.
What is true about the definition of a fold on a recursive type?
It recurses on each sub-object of the same type.
Why does $\text{data Nat = Zero \vert Succ Nat}$ not define the natural numbers?
It defines a superset of the natural numbers that includes bottom.
Rambling
What are folds – in the most general sense – all about? They’re about recursively combining some structure.
One way to write folds and unfolds is via a universal deconstructor for that type, a function that does one thing for certain subtypes, and another for different subtypes. E.g. the universal deconstrucor for Maybe is
maybe :: b -> (a -> b) -> (Maybe a) -> b
maybe nothing just Nothing = nothing
maybe nothing just (Just x) = just x
Or for lists:
list :: (a -> [a] -> b) -> b -> [a] -> b
list cons nil [] = nil
list cons nil (x:xs) = cons x xs
These translate naturally into the folds and unfolds for a type like so:
foldMaybe :: b -> (a -> b) -> Maybe a -> b
foldMaybe nothing just = rec where rec = maybe nothing (shape rec just)
where shape f x = f x
foldList cons nil = rec where rec = list (shape rec cons) nil
where shape f c x xs = c x (f xs)
How about for natural numbers?
Well a universal deconstructor could be given by
deconNat :: a -> (Nat -> a) -> Nat -> a
deconNat zero succ Zero = zero
deconNat zero succ (Succ x) = succ x
Then a fold would be
foldNat :: a -> (Nat -> a) -> Nat -> a
foldNat zero succ = rec where rec = deconNat zero (shape rec succ)
where shape f c x = c (f x)
An unfold could be
unfoldNat decon = rec where rec = decon (shape rec Succ) Zero
where shape f c x = c (f x)