Add tuple -- an isomorphism between a product type and a flat tuple

[cblp]

Close #106

[kcsongor]

Thanks! My plan is to first finish off and merge #104 then I'll add this one on top.

[cblp]

👍

[kcsongor]

I've thought about this, and I think a nicer general solution would be deriving an Iso between more general product types.

So

data T1 a b c = T1 a b c
data T2 = T2 Int Bool Char

here, we could derive an Iso' (T1 Int Bool Char) T2. It would be possible to try and reorder the fields as well (like the subtype lens does for records), but in this case I think the type-based reordering would be too magical (and would require that each field's type is unique).

So if we go with deriving an Iso where the ordering matters, it should be quite simple, because the generic representations of the product types will be the same modulo metadata.

[phadej]

Why stop at product types, Iso between SOP's which are equal. Yet that's just

generic . stripMedatata . from generic -- isn't it?

EDIT: reference generic

[kcsongor]

@phadej quite right!

[scott-fleischman]

It would be possible to try and reorder the fields as well (like the subtype lens does for records), but in this case I think the type-based reordering would be too magical (and would require that each field's type is unique).

I for one would love this magic (and it's corresponding uniqueness requirement). Even better if it supported equivalent trees of products and sums.

Iso' (Int, (Bool, Char)) (Bool, (Int, Char))
Iso' (Either Int (Either Bool Char)) (Either (Either Char Int) Bool)

[cblp]

The problem is generic . stripMedatata . from generic doesn't direct type inference. tuple does.

[kcsongor]

The problem is generic . stripMedatata . from generic doesn't direct type inference. tuple does.

Right, but tuple could then be an alias for the more general version. I think we could also experiment with incoherent instances to provide a type defaulting mechanism (something I've been meaning to write about for a while anyway).

[kcsongor]

Even better if it supported equivalent trees of products and sums.

Iso' (Int, (Bool, Char)) (Bool, (Int, Char))
Iso' (Either Int (Either Bool Char)) (Either (Either Char Int) Bool)

in principle I agree that this would be quite neat, but it does get tricky. For example, should we have Iso (Int, Bool, (Int, Bool)) ((Int, Bool), Int, Bool)? All 3 fields of the tuple are unique if you look at it only at a shallow layer, but if you look deep enough, the "4" fields are no longer unique.

I would like to find a solution that is predictable and allows these transformations, even if at the cost of some hints to the compiler on how to reorganise the fields. That being said, it would also be nice if a large set of "straightforward" (whatever that means) cases could be done automatically.

[scott-fleischman]

For example, should we have Iso (Int, Bool, (Int, Bool)) ((Int, Bool), Int, Bool)?

For what I have in mind for using the Isos, I would say no. I would like a function that navigates down probably to a newtype layer, requiring a conversion or coercion for those.

However, I could imagine that doing a single-layer conversion would be useful. Perhaps even multiple layers? Could there be an interface where you specify how many layers down you would want it to go?

Also if records are involved, it might be nice to consider uniqueness of the pair of field name and field type. It would be interesting to consider converting various trees of records as well. Maybe even giving a suggestion if field names are close but not exact. Maybe you could even pass in an argument saying that certain field name/type pairs should be considered the same.

So it sounds like there may be a few different interfaces that could be useful in different scenarios.

[kcsongor]

I would like a function that navigates down probably to a newtype layer, requiring a conversion or coercion for those.

I suppose the general principle of “don’t look into newtypes” could work. It would be good to find some motivating examples where this kind of Iso is useful.

However, I could imagine that doing a single-layer conversion would be useful. Perhaps even multiple layers? Could there be an interface where you specify how many layers down you would want it to go?

I think between single and multiple, the other options would be too brittle, as they would be very sensitive to the precise nesting of the types on both sides.

So it sounds like there may be a few different interfaces that could be useful in different scenarios.

I agree, and I’m hoping to find something that isn’t too ad-hoc, and is easily predictable. Something I find easy to understand is “there is a unique isomorphism between these two types”. But this is not general enough, because it would disallow any type with non-trivial automorphisms, so the Iso between a product type and a flat tuple (suggested in this issue) would only be possible between types with strictly unique fields, whereas if we respect the ordering, it could work with more generally.
But maybe that’s fine... I’ve already found by using generic-lens that it’s a lot more predictable when each field in a product has a distinct type (by using newtypes).

[phadej]

Just a small comment, when you have

data P a b = P a b

and you try to iso between

magical :: Iso (P a b) (c, d)

then if you don't try to shuffle values, but only require that there's 2 on the right and 2 on the left, then you can tell GHC to unify a ~ c and b ~ d. This is somewhat important for type-inference, I suspect quite important in example like

p ^. magical . _1 -- note that `d` is ambiguous unless, `b ~ d`

(EDIT: that example is bad for various reasons, but hopefully illustrative enough).