Choice

[benjaminselfridge]

I found a use for this; it's a sum type to List's product.

Don't know if it should be in a separate module, like Data.Choice.List or Data.List.Choice (since it relies on Data.List, and we might want to make another version that uses Assignments at some point).

Not sure if it needs to be in parameterized-utils at all, but it would seem strange to omit it, since it is dual to List.

This should not be merged until the ShowF type synonym change is merged; this kind of relies on that. I think the only way to derive a Show instance for this data type is using quantified constraints (otherwise we'd have to do ShowF f => Show (Choice f tps), which I don't think is derivable since you have to use showF instead of show).

[masaeedu]

Hi @benjaminselfridge. I think there's a slightly different tack we could take here as well.

In this PR, we express Choice in terms of Index. But an alternate perspective is that an Index is merely a specialization of Choice. Specifically, we can write:

type Choice :: (k -> Type) -> [k] -> Type
data Choice f as
  where
  Here :: f x -> Choice f (x ': xs)
  There :: Choice f xs -> Choice f (x ': xs)

and then we can recover Index as:

type Index xs x = Choice ((:~:) x) xs

The benefit is that many operations for Indices can be recovered as mere specializations of abstract operations that Choice has instances of (contingent on instances for (:~:) a).

We can go further, in fact. In particular, there is an involutive relationship between n-ary products and n-ary coproducts. So we can write the following newtype:

type Summary :: Type -> (k -> Type) -> k -> Type
newtype Summary r f i = Summary { summarize :: f i -> r }

type Co :: ((k -> Type) -> [k] -> Type) -> (k -> Type) -> [k] -> Type
newtype Co p f as = Co { runCo :: forall r. p (Summary r f) as -> r }

and a fun result is that Co List calculates (a type constructor naturally isomorphic to) Choice. Analogously, Co Choice calculates List.