Hacker News new | past | comments | ask | show | jobs | submit login

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.)

I'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.

Right, 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.

You 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.

Forgot to comment yesterday: thank you! Because of this I got unstuck.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact