Understanding Curry-Howard Isomorphism exercise from Thinking With Types

235 views Asked by At

I've begun reading the book Thinking With Types which is my first foray into type level programming. The author provides an exercise and the solution, and I cannot understand how the solution provided is correct.

The exercise is

enter image description here

I attempted to solve this exercise with the following

productToRuleMine :: (b -> a, c -> a) -> Either b c -> a
productToRuleMine (f, _) (Left b) = f b
productToRuleMine (_, g) (Right c) = g c

productFromRuleMine :: (Either b c -> a) -> (b -> a, c -> a)
productFromRuleMine f = (f . Left, f . Right)

productToRuleMine . productFromRuleMine = id

I feel this is a valid solution, however the book gives a different solution that doesn't seem to type check, leading me to believe my overall understanding is flawed

productToRuleBooks :: (b -> a) -> (c -> a) -> (Either b c) -> a
productToRuleBooks f _ (Left b) = f b
productToRuleBooks _ g (Right c) = g c

productFromRuleBooks :: (Either b c -> a) -> (b -> a, c -> a)
productFromRuleBooks f = (f . Left, f . Right)

The only way I can get the books answer to type check is the following:

(uncurry productToRule1 . productFromRule1) = id

since the type signatures alone don't line up

(Either b c -> a) -> (b -> a  ,   c -> a)
                     (b -> a) -> (c -> a) -> (Either b c) -> a

So the question I have is, is my solution incorrect? Why does the books type signature for productToRuleBooks accept as it's first and second arguments the functions b -> a and c -> a when it's my understanding that x (multiplication) from algebra equates to the (,) in types, so why doesn't the books answer have (b -> a, c -> a) as the first argument?

0

There are 0 answers