| 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)? |
This comment has been minimized.
This comment has been minimized.
|
This comment has been minimized.
This comment has been minimized.
|
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. |
This comment has been minimized.
This comment has been minimized.
|
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: My reasoning was: Matt, how is (a -> b) the exponential b^a? |
This comment has been minimized.
This comment has been minimized.
|
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! |
This comment has been minimized.
This comment has been minimized.
|
What is the process for "reversing the arrows"? E.g. we derived If we simplify the types to remove some noise we get: unfoldr :: (m -> b) -> la -> b If we work on unfoldr, what is the process from here? Do we put in explicit parenthesis for unfoldr? Which is not what we want from the simplified types: Does the process of reversing the arrows depend on whether a type is in the domain or co-domain? |
This comment has been minimized.