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.