[Haskell-cafe] How to define classy lenses for polymorphic types that involve singletons?

[Li-yao Xia]

Hi Peter,

 > In theory, I should be able to make
 > SomePerson an instance of HasPerson, define
 >
 >    person :: Lens' SomePerson (Person sex)


I wonder what you mean by that, since you highlight the issue just 
after. Another way to look at the problem is that this type is 
implicitly universally quantified (unless that's not what you had in mind):

     person :: forall sex. Lens' SomePerson (Person sex)

which can thus be specialized to

     person :: Lens' SomePerson (Person Male)
     person :: Lens' SomePerson (Person Female)

Those two lenses tell us that any `SomePerson` contains both a `Male` 
and `Female` person, while the definition of `SomePerson` contains only 
one. So the types alone reveal a design flaw, and any attempt to inhabit 
them is thus doomed.

Perhaps you could flip the dependency between `SomePerson` and `Person`. 
Move the singleton to a new field of Person, and generalize it so you 
can not only instantiate it with a singleton, but also an existentially 
quantified singleton:

     data Person' (s :: Type) = Person' { _sex :: s, _name, _email :: 
String }
     type Person (sex :: Sex) = Person' (SSex sex)
     type SomePerson = Person' SomeSex


Cheers,
Li-yao



On 6/4/19 8:15 AM, Peter Simons wrote:
> Hi,
> 
> I am trying to combine the lens library's 'makeClassy' feature with a
> type that's polymorphic over a singleton type:
> 
>> {-# LANGUAGE DataKinds, FlexibleInstances, FunctionalDependencies, GADTs,
>>      KindSignatures, RankNTypes, TemplateHaskell, TypeFamilies
>>    #-}
>>
>> import Control.Lens
>> import Data.Singletons
>> import Data.Singletons.TH
>>
>> data Sex = Male | Female
>>    deriving (Show, Eq, Ord, Bounded, Enum)
>>
>> genSingletons [''Sex]
>>
>> data Person (sex :: Sex) = Person { _name :: String, _email :: String }
>>    deriving (Show, Eq)
>>
>> makeClassy ''Person
> 
> Lens generates a class definition that looks sensible to me:
> 
>    class HasPerson a (sex :: Sex) | a -> sex where
>      person :: Lens' a (Person sex)
>      email :: Lens' a String
>      name :: Lens' a String
>      {-# MINIMAL person #-}
> 
> Furthermore, I also need a type SomePerson to hide the phantom type so
> that I can store people of different sexes in the same container, i.e.
> [SomePerson]:
> 
>> data SomePerson where
>>    SomePerson :: Sing sex -> Person sex -> SomePerson
>>
>> fromPerson :: SingI sex => Person sex -> SomePerson
>> fromPerson p = SomePerson Sing p
>>
>> toPerson :: SomePerson -> (forall sex. Sex -> Person sex -> a) -> a
>> toPerson (SomePerson s p) f = f (fromSing s) p
> 
> Here is where I've run into trouble. In theory, I should be able to make
> SomePerson an instance of HasPerson, define
> 
>    person :: Lens' SomePerson (Person sex)
> 
> to access the Person type inside of it, and that would allow me to use
> 'name' and 'email' for SomePerson just the same as for Person. However,
> it seems impossible to define that function because it leaks the
> universally quantified 'sex', so function does not type-check.
> 
> I have a somewhat awkward work-around that translates lenses on Person
> to SomePerson
> 
>> somePerson :: (forall sex. Lens' (Person sex) a) -> Lens' SomePerson a
>> somePerson l = lens (\(SomePerson _ p) -> view l p)
>>                      (\(SomePerson s p) x -> SomePerson s (set l x p))
> 
> and that allows me to define:
> 
>> type SomePerson' (sex :: Sex) = SomePerson
>>
>> instance HasPerson (SomePerson' sex) sex where
>>    person = undefined -- cannot type check because 'sex' would leak
>>    name = somePerson name
>>    email = somePerson email
> 
> I'm not particularly happy with that solution, though. Is there maybe a
> way to make this work such that I can avoid defining 'name' and 'email'
> manually? Or is there a clever alternative way to define HasPerson such
> a 'person' method for SomePerson is possible?
> 
> Best regards
> Peter
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>