on master help sign in
Regain `field s b -> t` functional dependency
commit904a9ae75af5269971aec00e1abb90ad0e940d34 authorCsongor Kiss <kiss.csongor.kiss@gmail.com> dateMon 4 Dec 2017, 00:50 (9 years ago) parentc08ec77
8 files changed+55−31
examples/Examples.hs+21−3 examples/StarWars.hs+1−1 src/Data/Generics/Internal/Families/Changing.hs+7 src/Data/Generics/Product.hs+10−13 src/Data/Generics/Product/Fields.hs+5−2 src/Data/Generics/Product/Positions.hs+2−2 src/Data/Generics/Sum.hs+8−9 src/Data/Generics/Sum/Constructors.hs+1−1
examples/Examples.hs+21−3
@@ -1,3 +1,7 @@
1+{-# LANGUAGE GADTs #-}
2+{-# LANGUAGE ScopedTypeVariables #-}
3+{-# LANGUAGE Rank2Types #-}
4+{-# LANGUAGE AllowAmbiguousTypes #-}
15{-# LANGUAGE DataKinds #-}
26{-# LANGUAGE DeriveGeneric #-}
37{-# LANGUAGE DuplicateRecordFields #-}
@@ -76,11 +80,25 @@ data Dog a
7680 deriving (Generic, Show)
7781type Name = String
7882type Age = Int
79−dog, cat, duck :: Animal2 Int
83+dog :: Animal2 Int
8084dog = Dog (MkDog "Shep" 3 30)
81−cat = Cat "Mog" 5
82−duck = Duck 2
8385
86+-- TODO: the error message for this case is ugly
87+-- data Dog a
88+-- = MkDog
89+-- { name :: Name
90+-- , age :: Age
91+-- , fieldA :: a
92+-- , fieldA' :: a
93+-- }
94+-- deriving (Generic, Show)
8495
8596--dog' :: Animal2 String
8697dog' = dog & _Ctor @"Dog" . field @"fieldA" .~ "now it's a String"
98+
99+stuff ::
100+ ( HasPosition 15 s t a String
101+ , HasField "test" s' t' a' b'
102+ , HasField "bar" a' b' s t
103+ ) => s' -> t'
104+stuff r = r & field @"test" . field @"bar" . position @15 .~ "hello"
examples/StarWars.hs+1−1
@@ -59,7 +59,7 @@ c3po = Droid
5959 , primaryFunction = "protocol and human relations"
6060 }
6161
62−getName :: HasField "name" a r => r -> a
62+getName :: HasField' "name" r a => r -> a
6363getName = getField @"name"
6464
6565-- upcast :: Subtype a b => a -> b
src/Data/Generics/Internal/Families/Changing.hs+7
@@ -1,3 +1,6 @@
1+{-# LANGUAGE AllowAmbiguousTypes #-}
2+{-# LANGUAGE FlexibleInstances #-}
3+{-# LANGUAGE FunctionalDependencies #-}
14{-# LANGUAGE DataKinds #-}
25{-# LANGUAGE PolyKinds #-}
36{-# LANGUAGE TypeFamilies #-}
@@ -91,3 +94,7 @@ type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
9194 Infer' s' a' _ _
9295 = '(UnProxied s', UnProxied a')
9396
97+type family PickTv (a :: k) (b :: k) :: * where
98+ PickTv (P _ _) b = b
99+ PickTv (f (P _ _)) (g b) = b
100+ PickTv (f a) (g b) = PickTv f g
src/Data/Generics/Product.hs+10−13
@@ -17,18 +17,15 @@
1717
1818module Data.Generics.Product
1919 ( -- *Lenses
20− HasAny (..)
21−
22− , HasField (..)
23− , HasPosition (..)
24− , HasType (..)
25−
26− -- *Subtype relationships
27− , Subtype (..)
20+ module Any
21+ , module Field
22+ , module Positions
23+ , module Subtype
24+ , module Typed
2825 ) where
2926
30−import Data.Generics.Product.Any
31−import Data.Generics.Product.Fields
32−import Data.Generics.Product.Positions
33−import Data.Generics.Product.Subtype
34−import Data.Generics.Product.Typed
27+import Data.Generics.Product.Any as Any
28+import Data.Generics.Product.Fields as Field
29+import Data.Generics.Product.Positions as Positions
30+import Data.Generics.Product.Subtype as Subtype
31+import Data.Generics.Product.Typed as Typed
src/Data/Generics/Product/Fields.hs+5−2
@@ -67,7 +67,7 @@ import GHC.TypeLits (Symbol, ErrorMessage(..), TypeError)
6767-- :}
6868
6969-- |Records that have a field with a given name.
70−class HasField (field :: Symbol) s t a b | s field -> a where
70+class HasField (field :: Symbol) s t a b | s field -> a, s field b -> t where
7171 -- |A lens that focuses on a field with a given name. Compatible with the
7272 -- lens package's 'Control.Lens.Lens' type.
7373 --
@@ -106,7 +106,7 @@ instance -- see Note [Changing type parameters]
106106 , GHasField' field (Rep s) a
107107 , GHasField' field (Rep s') a'
108108 , GHasField field (Rep s) (Rep t) a b
109− , '(t, b) ~ Infer s' a' a p
109+ , '(t, b) ~ Infer s' a' a (PickTv a' b)
110110 ) => HasField field s t a b where
111111
112112 field f s = ravel (repLens . gfield @field) f s
@@ -115,6 +115,9 @@ instance -- see Note [Changing type parameters]
115115instance {-# OVERLAPPING #-} HasField f (Void2 t a) t a b where
116116 field = undefined
117117
118+instance {-# OVERLAPPING #-} HasField f (Void1 a) (Void1 b) a b where
119+ field = undefined
120+
118121type family ErrorUnless (field :: Symbol) (s :: Type) (contains :: Bool) :: Constraint where
119122 ErrorUnless field s 'False
120123 = TypeError
src/Data/Generics/Product/Positions.hs+2−2
@@ -66,7 +66,7 @@ import GHC.TypeLits (type (<=?), Nat, TypeError, ErrorMessage(..))
6666-- :}
6767
6868-- |Records that have a field at a given position.
69−class HasPosition (i :: Nat) s t a b | s i -> a where
69+class HasPosition (i :: Nat) s t a b | s i -> a, s i b -> t where
7070 -- |A lens that focuses on a field at a given position. Compatible with the
7171 -- lens package's 'Control.Lens.Lens' type.
7272 --
@@ -92,7 +92,7 @@ instance -- see Note [Changing type parameters]
9292 , GHasPosition' i (Rep s) a
9393 , GHasPosition' i (Rep s') a'
9494 , GHasPosition 1 i (Rep s) (Rep t) a b
95− , '(t, b) ~ Infer s' a' a p
95+ , '(t, b) ~ Infer s' a' a (PickTv a' b)
9696 ) => HasPosition i s t a b where
9797
9898 position f s = ravel (repLens . gposition @1 @i) f s
src/Data/Generics/Sum.hs+8−9
@@ -17,14 +17,13 @@
1717
1818module Data.Generics.Sum
1919 ( -- *Prisms
20− AsAny (..)
21−
22− , AsConstructor (..)
23− , AsSubtype (..)
24− , AsType (..)
20+ module Any
21+ , module Constructors
22+ , module Subtype
23+ , module Typed
2524 ) where
2625
27−import Data.Generics.Sum.Any
28−import Data.Generics.Sum.Constructors
29−import Data.Generics.Sum.Subtype
30−import Data.Generics.Sum.Typed
26+import Data.Generics.Sum.Any as Any
27+import Data.Generics.Sum.Constructors as Constructors
28+import Data.Generics.Sum.Subtype as Subtype
29+import Data.Generics.Sum.Typed as Typed
src/Data/Generics/Sum/Constructors.hs+1−1
@@ -95,7 +95,7 @@ instance
9595 , GAsConstructor' ctor (Rep s) a
9696 , GAsConstructor' ctor (Rep s') a'
9797 , GAsConstructor ctor (Rep s) (Rep t) a b
98− , '(t, b) ~ Infer s' a' a p
98+ , '(t, b) ~ Infer s' a' a (PickTv a' b)
9999 ) => AsConstructor ctor s t a b where
100100
101101 _Ctor = repIso . _GCtor @ctor