-
-
Save mperry/8534788 to your computer and use it in GitHub Desktop.
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
commented
Jan 21, 2014
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
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.
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?
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!
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?