Add type families for concrete optics

[treeowl]

It's occasionally useful to get one's hands on the concrete Functor or
Profunctor of an ALens, APrism, etc., to use in constraints. Currently,
the only built-in option is to import the relevant .Internal module and use
the right one. But since these types are all concrete and transparent, it's
actually possible to write type families to extract the relevant types.
So let's do that, purely for convenience.

Note: I believe it must be possible to use TypeInType to make the kinds
of the results depend on the arguments. So we should be able to ask for
something like GetConcreteFunctor (AnEquality 'True 0 'False' 1).
But I don't yet know enough about TypeInType to be able to do that myself.

[treeowl]

(Sorry for the churn. I got mixed up a couple times.)

[ekmett]

p and q change in things like indexed optics. e.g. p a (f b) -> s -> f t so it may be worth changing those instances to p a (f b) -> q s (f t) to pick out f. or even to something like type instance Foo (pafb -> q s (f t)) = f.

Not entirely sold one way or the other on the utility provided here.

[treeowl]

@ekmett I just got the TypeInType thing working, BTW. Good point about that generalization; I could even add extractors for the two possibly-distinct profunctors. The reason I was thinking about this had to do with GHC proposal 5. I was imagining it might be interesting to have a pattern synonym like

import Control.Lens
import Control.Lens.Reified

pattern Package :: Lens s t a b -> ReifiedLens s t a b
pattern Package f <- Lens f
  where
    Package :: ALens s t a b -> ReifiedLens s t a b
    Package f = Lens $ cloneLens f

Unfortunately, if the committee sticks to its guns and requires that the pattern signature and builder signature are the same modulo constraints, this will have to be expressed something like

import Control.Lens.Internal.Context -- additionally

pattern Package :: c ~ Functor
               => (forall f. c f => LensLike f s t a b)
               -> ReifiedLens s t a b
pattern Package f <- Lens f
  where
    Package :: c ~ ((~) (Pretext (->) a b))
           => (forall f. c f => LensLike f s t a b)
           -> ReifiedLens s t a b
    Package f = Lens $ cloneLens f

The proposed type families allow this to be written without the .Internal import:

    Package :: c ~ ((~) (GetConcreteFunctor (ALens s t a b)))
            => ....

Yes, the whole thing is horrible...

[bennofs]

Wouldn't the better solution here be to just re-export the types from non-Internal modules?

[treeowl]

@bennofs, that was my first thought, and may very well be the right one, but what if the definition of ALens changes? Keeping Pretext internal offers a bit of abstraction there.

[bennofs]

@treeowl What would a possible change of ALens that would break code using the types directly but not break code using these synonyms?

[treeowl]

@bennofs,

1. Changing to use a type that's specialized to (->).
2. Changing to use a type parametrized by s and/or t as well as a and b.

I don't know if either of these could ever actually be good ideas; I'm just thinking hypothetically.

[treeowl]

@bennofs, note that the type families leave the current abstraction barrier in exactly the same place; they're the most conservative way to solve the problem. That doesn't mean they're the right way!

[treeowl]

I can't begin to understand the errors CI is getting on GHC 7.8 and 7.10. Was that a now-fixed GHC bug?

[RyanGlScott]

@treeowl, you can work around one occurrence of that bug by sufficient kind monomorphization:

type instance GetConcreteFunctor (pafb -> (p :: * -> * -> *) s (f t)) = f

I'm not sure if you intended for it to actually be p :: k -> * -> *, however. (I'm not aware of a way to backport that kind signature while avoiding that old bug.)

[treeowl]

I need to fix up the documentation to reflect the split into GetConcreteArgProfunctor and GetConcreteTransformedProfunctor.

[ekmett]

You could delegate to another type family recursively to handle (p s (f t)) which delegates to another to force p to have kind * -> * -> *. This would likely require ~3 type families though.

[treeowl]

Why would I want to do that?

…

On May 25, 2017 11:07 PM, "Edward Kmett" ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In src/Control/Lens/Type.hs <#736 (comment)>: > +-- GetConcreteFunctor (ALens s t a b) = Pretext (->) a b +-- GetConcreteFunctor (AnIso s t a b) = Identity +-- @ +#if __GLASGOW_HASKELL__ >= 800 +type family GetConcreteFunctor (x :: *) :: GetConcreteFunctorKind x +type instance GetConcreteFunctor x = GetConcreteFunctorType (GetConcreteFunctorKind x) x +type family GetConcreteFunctorKind (x :: *) :: * +type instance GetConcreteFunctorKind (pafb -> p s ((f :: j -> k) t)) = j -> k +type family GetConcreteFunctorType (k :: *) (x :: *) :: k +type instance GetConcreteFunctorType (i -> o) (pafb -> p s ((f :: i -> o) t)) = f +#else +type family GetConcreteFunctor (x :: *) :: * -> * +type instance GetConcreteFunctor (pafb -> (p :: * -> * -> *) s ((f :: * -> *) t)) = f +#endif + +-- | Extract the concrete 'Profunctor' from a concrete 'ALens', 'AnIso', etc. You could delegate to another type family recursively to handle (p s (f t)) which delegates to another to force p to have kind * -> * -> *. This would likely require ~3 type families though. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#736 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABzi_cGQ4nhLqkba_1qliwQdpH9Y2xS-ks5r9kHigaJpZM4Nmv8E> .