4cc2db3 · generic-lens

src/Data/Generics/Internal/Families/Changing.hs+39−5

compare with master

unifiedsplit

@@ -41,18 +41,52 @@ type family Proxied' (t :: k) (next :: Nat) :: k where

41 Proxied' t _ = t

42

43type family UnProxied (t :: k) :: k where

44+ UnProxied (P _ a) = a

44 UnProxied (t (P _ a) :: k) = UnProxied t a

45 UnProxied (t (P _ a) :: k) = UnProxied t a

45 UnProxied t = t

46 UnProxied t = t

46

47

47type family Change (t :: k) (target :: Nat) (to :: j) :: k where

48type family Change (t :: k) (target :: Nat) (to :: j) :: k where

49+ Change (P target _) target to = (P target to)

48 Change (t (P target _) :: k) target to = t (P target to)

50 Change (t (P target _) :: k) target to = t (P target to)

49 Change (t a :: k) target to = Change t target to a

51 Change (t a :: k) target to = Change t target to a

50 Change t _ _ = t

52 Change t _ _ = t

51

53

52−type family IsParam a where

54+-- TODO: document this

53− IsParam (P _ _) = 'True

55+data Skolem

54− IsParam _ = 'False

55

56

56−type family IndexOf a where

57+type family Generalise (t :: k) (w :: *) :: k where

57− IndexOf (P i a) = i

58+ Generalise Skolem w = w

59+ Generalise (t Skolem :: k) w = t w

60+ Generalise (t a) w = (Generalise t w) a

61+ Generalise t _ = t

58

62

63+type family UnApply (a :: k) :: [*] where

64+ UnApply (f x) = x ': UnApply f

65+ UnApply x = '[]

66+

67+type family Unify a b :: [(*, *)] where

68+ Unify (P n a') a = '[ '(P n a', a)]

69+ Unify a b = Zip (UnApply a) (UnApply b)

70+

71+type family PSub (subs :: [(*, *)]) :: [(Nat, *)] where

72+ PSub '[] = '[]

73+ PSub ('(P n _, b) ': xs) = '(n, b) ': PSub xs

74+ PSub (_ ': xs) = PSub xs

75+

76+type family Fst (a :: (k, l)) :: k where

77+ Fst '(f, _) = f

78+

79+type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where

80+ Zip '[] '[] = '[]

81+ Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys

82+

83+type family IsSingleton (xs :: [k]) :: Bool where

84+ IsSingleton '[_] = 'True

85+ IsSingleton _ = 'False

86+

87+type family Head (xs :: [k]) :: k where

88+ Head (x ': _) = x

89+

90+type family IfEq a b t f where

91+ IfEq a a t _ = t

92+ IfEq _ _ _ f = f

src/Data/Generics/Internal/Void.hs+2

@@ -14,3 +14,5 @@ module Data.Generics.Internal.Void where

14 machinery has sufficient information to reduce to sensible types.

15-}

16data Void

17+data Void1 a

18+data Void2 a b

src/Data/Generics/Product/Any.hs+1−1

@@ -52,7 +52,7 @@ import Data.Generics.Product.Typed

52-- :}

53

54-- |Records that have generic lenses.

55−class HasAny (sel :: k) s t a b | s sel k -> a, s sel k b -> t where

55+class HasAny (sel :: k) s t a b | s sel k -> a where

56 -- |A lens that focuses on a part of a product as identified by some

57 -- selector. Currently supported selectors are field names, positions and

58 -- unique types. Compatible with the lens package's 'Control.Lens.Lens'

src/Data/Generics/Product/Fields.hs+7−4

@@ -68,7 +68,7 @@ import Data.Type.Bool (If)

68-- :}

69

70-- |Records that have a field with a given name.

71−class HasField (field :: Symbol) s t a b | s field b -> t, s field -> a where

71+class HasField (field :: Symbol) s t a b | s field -> a where

72 -- |A lens that focuses on a field with a given name. Compatible with the

73 -- lens package's 'Control.Lens.Lens' type.

74 --

@@ -107,14 +107,17 @@ instance -- see Note [Changing type parameters]

107 , GHasField' field (Rep s) a

108 , GHasField' field (Rep s') a'

109 , GHasField field (Rep s) (Rep t) a b

110− , '(t', b') ~ If (IsParam a') '(Change s' (IndexOf a') b, P (IndexOf a') b) '(s', b)

110+ , aa ~ PSub (Unify a' a)

111+ , '(t', b') ~ If (IsSingleton aa) '(Change s' (Fst (Head aa)) Skolem, Change a' (Fst (Head aa)) Skolem) '(s', a')

112+ , t'' ~ UnProxied t'

111− , t ~ UnProxied t'

113+ , b'' ~ UnProxied b'

114+ , '(b, t) ~ If (IsSingleton aa) '(Generalise b'' p, Generalise t'' p) '(b'', t'')

112 ) => HasField field s t a b where

115 ) => HasField field s t a b where

113

116

114 field f s = ravel (repLens . gfield @field) f s

117 field f s = ravel (repLens . gfield @field) f s

115

118

116-- See Note [Uncluttering type signatures]

119-- See Note [Uncluttering type signatures]

117−instance {-# OVERLAPPING #-} HasField f Void Void Void Void where

120+instance {-# OVERLAPPING #-} HasField f (Void2 t a) t a b where

118 field = undefined

121 field = undefined

119

122

120type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where

123type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where

src/Data/Generics/Product/Internal/Fields.hs+1−1

@@ -49,7 +49,7 @@ instance GProductHasField field l r l' r' a b (HasTotalFieldP field l)

49

50 gfield = gproductField @field @_ @_ @_ @_ @_ @_ @(HasTotalFieldP field l)

51

52−instance (GHasField field r r a a, GHasField field l l a a, GHasField field l l' a b, GHasField field r r' a b)

52+instance (GHasField' field r a, GHasField' field l a, GHasField field l l' a b, GHasField field r r' a b)

53 => GHasField field (l :+: r) (l' :+: r') a b where

54

55 gfield f (L1 s) = fmap (\a -> L1 (set (gfield @field) a s)) (f (s ^. gfield @field))

src/Data/Generics/Product/Positions.hs+7−4

@@ -66,7 +66,7 @@ import GHC.TypeLits (type (<=?), Nat, TypeError, ErrorMessage(..))

66-- :}

67

68-- |Records that have a field at a given position.

69−class HasPosition (i :: Nat) s t a b | s i -> a, s i b -> t where

69+class HasPosition (i :: Nat) s t a b | s i -> a where

70 -- |A lens that focuses on a field at a given position. Compatible with the

71 -- lens package's 'Control.Lens.Lens' type.

72 --

@@ -92,14 +92,17 @@ instance -- see Note [Changing type parameters]

92 , GHasPosition' i (Rep s) a

93 , GHasPosition' i (Rep s') a'

94 , GHasPosition 1 i (Rep s) (Rep t) a b

95− , '(t', b') ~ If (IsParam a') '(Change s' (IndexOf a') b, P (IndexOf a') b) '(s', b)

95+ , aa ~ PSub (Unify a' a)

96+ , '(t', b') ~ If (IsSingleton aa) '(Change s' (Fst (Head aa)) Skolem, Change a' (Fst (Head aa)) Skolem) '(s', a')

97+ , t'' ~ UnProxied t'

96− , t ~ UnProxied t'

98+ , b'' ~ UnProxied b'

99+ , '(b, t) ~ If (IsSingleton aa) '(Generalise b'' p, Generalise t'' p) '(b'', t'')

97 ) => HasPosition i s t a b where

100 ) => HasPosition i s t a b where

98

101

99 position f s = ravel (repLens . gposition @1 @i) f s

102 position f s = ravel (repLens . gposition @1 @i) f s

100

103

101-- See Note [Uncluttering type signatures]

104-- See Note [Uncluttering type signatures]

102−instance {-# OVERLAPPING #-} HasPosition f Void Void Void Void where

105+instance {-# OVERLAPPING #-} HasPosition f (Void2 a t) t a b where

103 position = undefined

106 position = undefined

104

107

105type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where

108type family ErrorUnless (i :: Nat) (s :: Type) (hasP :: Bool) :: Constraint where

src/Data/Generics/Sum/Constructors.hs+18−13

@@ -46,33 +46,36 @@ import Data.Type.Bool (If)

46-- >>> :set -XDeriveGeneric

47-- >>> import GHC.Generics

48-- >>> :m +Data.Generics.Internal.Lens

49+-- >>> :m +Data.Generics.Product.Fields

50+-- >>> :m +Data.Function

49-- >>> :{

51-- >>> :{

50−-- data Animal

52+-- data Animal a

51−-- = Dog Dog

53+-- = Dog (Dog a)

52-- | Cat Name Age

54-- | Cat Name Age

53-- | Duck Age

55-- | Duck Age

54-- deriving (Generic, Show)

56-- deriving (Generic, Show)

55−-- data Dog

57+-- data Dog a

56-- = MkDog

58-- = MkDog

57−-- { name :: Name

59+-- { name :: Name

58−-- , age :: Age

60+-- , age :: Age

61+-- , fieldA :: a

59-- }

62-- }

60-- deriving (Generic, Show)

63-- deriving (Generic, Show)

61-- type Name = String

64-- type Name = String

62-- type Age = Int

65-- type Age = Int

63−-- dog, cat, duck :: Animal

66+-- dog, cat, duck :: Animal Int

64−-- dog = Dog (MkDog "Shep" 3)

67+-- dog = Dog (MkDog "Shep" 3 30)

65-- cat = Cat "Mog" 5

68-- cat = Cat "Mog" 5

66-- duck = Duck 2

69-- duck = Duck 2

67-- :}

70-- :}

68

71

69-- |Sums that have a constructor with a given name.

72-- |Sums that have a constructor with a given name.

70−class AsConstructor (ctor :: Symbol) s t a b | s ctor -> a where

73+class AsConstructor (ctor :: Symbol) s t a b | ctor s -> a, ctor t -> b where

71 -- |A prism that projects a named constructor from a sum. Compatible with the

74 -- |A prism that projects a named constructor from a sum. Compatible with the

72 -- lens package's 'Control.Lens.Prism' type.

75 -- lens package's 'Control.Lens.Prism' type.

73 --

76 --

74 -- >>> dog ^? _Ctor @"Dog"

77 -- >>> dog ^? _Ctor @"Dog"

75− -- Just (MkDog {name = "Shep", age = 3})

78+ -- Just (MkDog {name = "Shep", age = 3, fieldA = 30})

76 --

79 --

77 -- >>> dog ^? _Ctor @"Cat"

80 -- >>> dog ^? _Ctor @"Cat"

78 -- Nothing

81 -- Nothing

@@ -80,7 +83,7 @@ class AsConstructor (ctor :: Symbol) s t a b | s ctor -> a where

80 -- >>> cat ^? _Ctor @"Cat"

83 -- >>> cat ^? _Ctor @"Cat"

81 -- Just ("Mog",5)

84 -- Just ("Mog",5)

82 --

85 --

83− -- >>> _Ctor @"Cat" # ("Garfield", 6) :: Animal

86+ -- >>> _Ctor @"Cat" # ("Garfield", 6) :: Animal Int

84 -- Cat "Garfield" 6

87 -- Cat "Garfield" 6

85 _Ctor :: Prism s t a b

88 _Ctor :: Prism s t a b

86

89

@@ -93,14 +96,16 @@ instance

93 , GAsConstructor' ctor (Rep s) a

96 , GAsConstructor' ctor (Rep s) a

94 , GAsConstructor' ctor (Rep s') a'

97 , GAsConstructor' ctor (Rep s') a'

95 , GAsConstructor ctor (Rep s) (Rep t) a b

98 , GAsConstructor ctor (Rep s) (Rep t) a b

96− , '(t', b') ~ If (IsParam a') '(Change s' (IndexOf a') b, P (IndexOf a') b) '(s', b)

99+ , aa ~ PSub (Unify a' a)

100+ , '(t', b') ~ IfEq a a' '(s', a') (If (IsSingleton aa) '(Change s' (Fst (Head aa)) Skolem, Change a' (Fst (Head aa)) Skolem) '(s', a'))

101+ , b ~ Generalise (UnProxied b') p

97− , t ~ UnProxied t'

102+ , t ~ Generalise (UnProxied t') p

98 ) => AsConstructor ctor s t a b where

103 ) => AsConstructor ctor s t a b where

99

104

100 _Ctor = repIso . _GCtor @ctor

105 _Ctor = repIso . _GCtor @ctor

101

106

102-- See Note [Uncluttering type signatures]

107-- See Note [Uncluttering type signatures]

103−instance {-# OVERLAPPING #-} AsConstructor ctor Void Void Void Void where

108+instance {-# OVERLAPPING #-} AsConstructor ctor (Void1 a) (Void1 b) a b where

104 _Ctor = undefined

109 _Ctor = undefined

105

110

106type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where

111type family ErrorUnless (ctor :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where

src/Data/Generics/Sum/Internal/Constructors.hs+4−2

@@ -45,10 +45,12 @@ type GAsConstructor' ctor s a = GAsConstructor ctor s s a a

45

46instance

47 ( GCollectible f as

48+ , GCollectible g bs

48 , ListTuple a as

49 , ListTuple a as

50+ , ListTuple b bs

49− ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) (M1 C ('MetaCons ctor fixity fields) f) a a where

51+ ) => GAsConstructor ctor (M1 C ('MetaCons ctor fixity fields) f) (M1 C ('MetaCons ctor fixity fields) g) a b where

50

52

51− _GCtor = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple @_ @as . gtoCollection . unM1)

53+ _GCtor = prism (M1 . gfromCollection . tupleToList) (Right . listToTuple . gtoCollection . unM1)

52

54

53instance GSumAsConstructor ctor (HasCtorP ctor l) l r l' r' a b => GAsConstructor ctor (l :+: r) (l' :+: r') a b where

55instance GSumAsConstructor ctor (HasCtorP ctor l) l r l' r' a b => GAsConstructor ctor (l :+: r) (l' :+: r') a b where

54 _GCtor = _GSumCtor @ctor @(HasCtorP ctor l)

56 _GCtor = _GSumCtor @ctor @(HasCtorP ctor l)