Adjunction v1 proxy

[RyanGlScott]

Before discussing the finer details, let me first pose the question: why did you pair V1 with Proxy? Given V1's generics connotation, I would have expected V1 to be paired with U1, if anything.

(I am aware that U1 doesn't currently have a Representable instance, but I can try to make a new distributive release soon to make that a possibility.)

[phadej]

yeah, I'd rather picked Void1 if one existed. U1 would work equally well.

[RyanGlScott]

If we do choose U1, it might make sense to add instances for the other types in GHC.Generics too (e.g., instance Adjunction Par1 Par1). But this of course depends on #12 being merged to get them to have Representable instances.

[RyanGlScott]

@phadej: I've pushed 12812ea8d878bb871ca5de0863046d4b76c67768, which adds Representable instances to the datatypes in GHC.Generics, so this should allow you to proceed.

[phadej]

@RyanGlScott any ideas, is there absurd :: V1 a -> b in some library already?

[RyanGlScott]

Not that I'm aware of. I'd just define it locally like so:

absurdV1 :: V1 a -> b
#if __GLASGOW_HASKELL__ >= 708
absurdV1 x = case x of {}
#else
absurdV1 !x = undefined
#endif

[ekmett]

I also prefer the V1 -| U1 notion. It is very clean.

[phadej]

green

[RyanGlScott]

Looking good. But if we really want to complete the GHC.Generics collection, there's some more sensible instances you could add that mimic existing ones:

instance Adjunction f g                     => Adjunction (Rec1 f) (Rec1 g)
instance Adjunction f g                     => Adjunction (M1 i c f) (M1 j d g)
instance (Adjunction f g, Adjunction f' g') => Adjunction (f' :.: f) (g :.: g')
instance (Adjunction f g, Adjunction f' g') => Adjunction (f :+: f') (g :*: g')

[ekmett]

Sadly, the M1 instances don't quite work due to uniqueness requirements.

[phadej]

@ekmett I have noticed that. Is M1 i c f |- M1 i c g good enough, or is it better to omit it?

[ekmett]

Wrong semantics. c is meaningful content there.

[ekmett]

It describes things like constructor names, data type names, etc.

[RyanGlScott]

Thanks, @phadej!