Search code examples
haskellhaskell-lens

Is making this `getIndex` optic possible?

Is it possible to make an optic with the following type:

getIndex :: Lens.IndexedGetter i a i

I couldn't find an existing one and in unsuccessfully trying to write one I got a feeling that it can't be done, but if that's the case I would like to know the explanation for why that is.

Solution

  • The index is defined arbitrarily by the getter, so there is no universal way to create one.

    IndexedGetter i s i is isomorphic to s -> (i, i), via the following bijection:

    ito   :: (s -> (i, a)) -> IndexedGetter i s a
iview :: IndexedGetter i s a -> s -> (i, a)

    forall s i. IndexedGetter i s i (the fully quantified type of getIndex) would be isomorphic to forall s i. s -> (i, i), but that's not inhabited (it would imply () -> (Void, Void) with s ~ () and i ~ Void).