Ad
  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    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.

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

    This comment is hidden because it contains spoiler information about the solution

  • Custom User Avatar

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

  • Custom User Avatar

    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

  • Custom User Avatar

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

  • Custom User Avatar

    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?