Skip to content

Instantly share code, notes, and snippets.

@mperry
Created January 21, 2014 05:15
Show Gist options
  • Save mperry/8534788 to your computer and use it in GitHub Desktop.
Save mperry/8534788 to your computer and use it in GitHub Desktop.
This is an attempt to explore the duality of fold and unfold
Haskell definitions:
unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
foldr :: (a -> b -> b) -> b -> [a] -> b
If I reverse the arrows on unfoldr
dual(unfoldr) :: [a] -> (Maybe (a, b) -> b) -> b
I think I need to show the type isomorphism (a -> b -> b) -> b is equivalent to Maybe (a, b) -> b, which is equivalent to
(a -> b -> b) == Maybe(a, b)
Now I am stuck
These slides on slide 15 seems to show this transformation (http://conal.net/talks/folds-and-unfolds.pdf), but I don't understand the steps.
Any help on understanding (a -> b -> b) == Maybe(a, b)?
@tonymorris
Copy link

(a -> b -> b) -> b  -> [a] -> b
((a, b) -> b,    b) -> [a] -> b -- uncurry
(Maybe (a, b) -> b) -> [a] -> b -- ((a, b) -> b, b) ≅ (Maybe (a, b) -> b)

@tonymorris
Copy link

f :: 
  (Maybe (a, b) -> b) -> ((a, b) -> b, b)
f k =
  (k . Just, k Nothing)

g :: 
  ((a, b) -> b, b) -> (Maybe (a, b) -> b)
g (j, k) =
  maybe k j

@mbrcknl
Copy link

mbrcknl commented Jan 21, 2014

Mark, think of (a -> b) as the exponential b^a, (a,b) as the product a*b, and (Maybe a) as 1+a, since that's exactly what they are.

@mperry
Copy link
Author

mperry commented Jan 21, 2014

Ok, I understand Tony's definition of f and g, although I have difficulty reading pointfree style fluently.

It took me a long time to get Tony's transform in the first comment:
((a, b) -> b, b) ≅ (Maybe (a, b) -> b)

My reasoning was:
((a, b) -> b, b)
= ((a, b) -> b, () -> b)
= ((a, b) / () ) -> b
= Maybe (a, b) -> b

Matt, how is (a -> b) the exponential b^a?

@mperry
Copy link
Author

mperry commented Jan 21, 2014

I think I have how function types are exponential types now after reading http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/. Thanks Matt!

@mperry
Copy link
Author

mperry commented Jan 22, 2014

What is the process for "reversing the arrows"? E.g. we derived
unfoldr:: (Maybe (a, b) -> b) -> [a] -> b
foldr:: (b -> Maybe (a, b)) -> b -> [a]

If we simplify the types to remove some noise we get:

unfoldr :: (m -> b) -> la -> b
foldr :: (b -> m) -> b -> la

If we work on unfoldr, what is the process from here? Do we put in explicit parenthesis for unfoldr?
(m -> b) -> (la -> b)
(m <- b) <- (la <- b) -- reverse arrows
(b -> la) -> (b -> m) -- rearrange terms

Which is not what we want from the simplified types:
foldr :: (b -> m) -> b -> la

Does the process of reversing the arrows depend on whether a type is in the domain or co-domain?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment