My previous post, Another lovely example of type class morphisms, placed some standard structure around Max Rabkin’s Beautiful folding, using type class morphisms to confirm that the
Applicative instances agreed with their inevitable meanings.
In the process of working out the
Applicative case, I realized the essence of fold zipping was getting a bit obscured.
This post simplifies Max’s
Fold data type a bit and shows how to zip strict left folds in the simpler setting.
You can get the code described here.
- 2008-11-15: I renamed the
A simpler fold
The strict left-folding functional is
foldl' :: (a -> b -> a) -> a -> [b] -> a
Max’s fold type packages up the first two arguments of
foldl' and adds on an post-fold step, as needed for
data Fold b c = forall a. F (a -> b -> a) a (a -> c) -- clever version
A simpler, less clever version just has the two
foldl' arguments, and no
data Fold b a = F (a -> b -> a) a -- simple version
I’ll use this simpler version for zipping and later enhance it for
The strict interpretation of
Fold simply unpacks and folds:
cfoldl' :: Fold b a -> [b] -> a cfoldl' (F op e) = foldl' op e
Zipping is then just a simplification of the
(<*>) definition in the previous post.
P is a type and constructor of strict pairs.
data P c c' = P !c !c' zipF' :: Fold b a -> Fold b a' -> Fold b (P a a') F op e `zipF'` F op' e' = F op'' (P e e') where P a a' `op''` b = P (a `op` b) (a' `op'` b)
We can also define non-strict counterparts:
cfoldl :: Fold b a -> [b] -> a cfoldl (F op e) = foldl op e zipF :: Fold b a -> Fold b a' -> Fold b (a,a') F op e `zipF` F op' e' = F op'' (e,e') where (a,a') `op''` b = (a `op` b, a' `op'` b)
More type classes …
A previous post suggested a criterion for inevitability of interpretation functions like
Whatever class instances exists for the source type (
Fold here), interpretation functions should be
“type class morphisms” for those classes, which loosely means that the meaning of a method is the same method on the meaning.
Where’s the type class for our simplified
It lacks the magic ingredient Max added to make it a
Functor and an
Applicative, namely the post-fold step.
However, there’s another class that’s just the thing:
class Zip f where zip :: f a -> f b -> f (a,b)
(I’ve used this class with type representations and user interfaces.)
Zip class from
TypeCompose is almost identical to the
Zip class in
The latter class requires
Functor, however, which is too restrictive for the simplified
Our non-strict left folds have a
instance Zip (Fold b) where zip = zipF
For strict folds, define a strict variant on
class Zip' f where zip' :: f a -> f b -> f (P a b)
Zip' instance for
instance Zip' (Fold b) where zip' = zipF'
… and more morphisms
These zipping classes have associated morphism properties.
q mapping from one
Zip instance to another is a “
Zip morphism” when
q (f `zip` g) == q f `zip` q g
for all folds
q (f `zip'` g) == q f `zip'` q g
In other words,
q distributes over
As I’ll show in another post, the two interpretation functions
Zip' morphisms, respectively, i.e.,
cfoldl (f `zip` g) == cfoldl f `zip` cfoldl g cfoldl' (f `zip'` g) == cfoldl' f `zip'` cfoldl' g
which means that zip folding as defined above works correctly.
I like to keep blog posts fairly short, so I’ll share two more pieces of this story in upcoming blog posts:
- Regaining the lost
Zip'morphism proofs for zip folding.