establish class hierarchy

[jdegoes]

A bunch of random ideas / suggestions since I actually wanted to create this library myself: :laughing:

I'd suggest that Iso be a type class, and not a data declaration. The reason is you can generalize the arrow, e.g.:

class Iso p where
  forward :: forall a b. p a b -> a -> b
  backward :: forall a b. p a b -> b -> a

data IsoF a b = IsoF (a -> b) (b -> a)

instance isoIsoF ...

Further, I'd suggest that Iso actually extend something called Equiv, which would be an isomorphism between sets having an equivalence relation. This is useful for invertible parsers, etc., where you only have isomorphism up to 'canonical elements'.

The laws are weaker:

-- | forward <<< backward <<< forward << backward = forward << backward
-- | backward <<< forward <<< backward << forward = backward <<< forward
class Equiv p where
  forward :: forall a b. p a b -> a -> b
  backward :: forall a b. p a b -> b -> a

These laws basically say there exists canonical elements in each set (for all members of the sets), and there exists an isomorphism on sets of these canonical elements.

Finally, every Iso a b forms an invariant functor in a and an invariant functor in b. These newtypes could be called Forward and Backward or something.

[paf31]

I'd rather use data than classes because I worry type inference is going to become problematic with MPTCs and flexible instances. We can still generalize Iso over different profunctors, arrows, whatever:

data Iso p a b = Iso (p a b) (p b a)

I'm not sure I understand your Iso class though. I want to capture an isomorphism between two types, so surely those need to appear in the instance head? Right now, you only have p. I was going for something closer to Haskell's partial-isomorphisms library, rather than lenses. The idea was to establish the category first, and then to integrate things into lens-land.

Your Equiv class sounds an awful lot like an adjunction between discrete categories (or even a Galois connection), in which case you would have

forward <<< backward <<< forward = forward
backward <<< forward <<< backward = backward

Is there a difference?

[jdegoes]

Is there a difference?

No, it looks like it's the same idea to me.

We can still generalize Iso over different profunctors, arrows, whatever:

:+1: If they are not type classes, how would we model the fact that Iso is not required in all cases (Equiv is enough)? In fact, it seems rare for data declarations to have any laws at all.

[paf31]

I always wondered about that. I don't see any reason why data declarations can't have laws. We often create structures which are "correct by construction", so we obviously have some set of laws in mind.