Hmm, I assume then it has to do with kinds and why dependently typed languages exist for actual proofs, but take anything I write with a grain of salt as I'm also learning haskell and mostly speculate.

If I understand correctly, the eq function is only partially defined on the cases when a and b are actually equal.

How is it legit to use eq in a more general case as in eq (plus a b) (plus b a)?

Thanks for the hint, it's very helpful. I was finally able to finish this Kata.

I personally think the description on this particular proposition is a bit confusing, at least to me. In the beginning I didn't even know I'm suppose implement this function at all. Perhaps we can add a little bit more elaboration on how this is supposed to be done and add a placeholder on the implementation indicating this is meant to be completed by the reader.

Anyway it's a very interesting Kata, thank you and lolisa for your work :p

You missed one very obvious case. Don't forget that it's a Maybe a -> Maybe b, not a -> Maybe b ;-)

It's not an issue, a question ;-)

Hi folks. I'm playing with this Kata and have no idea how to implement the false proposition:

isoUnMaybe :: ISO (Maybe a) (Maybe b) -> ISO a b

It cannot be proven, which is obvious: if we get Nothing by feeding Just a to the Maybe a -> Maybe b part of the isomorphism, we have no way to retrieve a b.

Leaving isoUnMaybe = undefined doesn't seem to pass the final tests. Neither does this work:

isoUnMaybe :: ISO (Maybe a) (Maybe b) -> ISO a b
isoUnMaybe (mab, mba) = (ab, ba)
  where ab a = fromJust $ mab (Just a)
        ba b = fromJust $ mba (Just b)

The error says it panicked by calling fromJust on Nothing. Perhaps I should return some specific error message?