4 ms·
9.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a neg
by Twisol 8y ago
9.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a negation operator.
(EDIT: Looks like some of the exercises are getting shuffled between versions -- 9.3(d) is the one I meant as of v1.2, but that might change over time. At least the type signature is a clue about which one I mean.)
- GolDDranks 8y agoI'm totally stuck. I would write an exhaustive pattern match to implement that function, but I have no clue how to do that in logic, without using negation.
- mbrock 8y agoYou know A|B and A|C. Prove A|(B&C) by assuming A and separately by assuming B, then use case analysis (by dragging the first conclusion onto the second). To prove A|(B&C) assuming B, you have to use A|C and yet another (nested) case analysis.
- GolDDranks 8y agoForgot to comment yesterday: thank you! Because of this I got unstuck.
- Twisol 8y agoRight, here's my implementation in Haskell: f x y = case x of Left a -> Left a Right b -> case y of Left a -> Left a Right c -> Right (b, c) Each `case` represents a couple of hypothetical contexts, applying case analysis to the Either (the OR). You're going to have to duplicate some work, since the `Left a` branch appears twice and you're getting the `a` from different places.