@@ -64,3 +64,60 @@ instance (FIndex r (s ': rs) ~ 'S i, FElem r rs i) => FElem r (s ': rs) ('S i) w
6464
6565 fput y = getIdentity . flens Proxy (\_ -> Identity y)
6666 {-# INLINE fput #-}
67+
68+-- This is an internal convenience stolen from the @lens@ library.
69+lens
70+ :: Functor f
71+ => (t -> s)
72+ -> (t -> a -> b)
73+ -> (s -> f a)
74+ -> t
75+ -> f b
76+lens sa sbt afb s = fmap (sbt s) $ afb (sa s)
77+{-# INLINE lens #-}
78+
79+-- | A partial relation that gives the indices of a sublist in a larger list.
80+type family FImage (rs :: [(Symbol, Schema)]) (ss :: [(Symbol, Schema)]) :: [Nat] where
81+ FImage '[] ss = '[]
82+ FImage ('(fn,s) ': rs) ss = FIndex fn ss ': FImage rs ss
83+
84+class is ~ FImage rs ss
85+ => FSubset (rs :: [(Symbol, Schema)]) (ss :: [(Symbol, Schema)]) is where
86+ -- | This is a lens into a slice of the larger record. Morally, we have:
87+ --
88+ -- > fsubset :: Lens' (Rec FieldRepr ss) (Rec FieldRepr rs)
89+ fsubset
90+ :: Functor g
91+ => (Rec FieldRepr rs -> g (Rec FieldRepr rs))
92+ -> Rec FieldRepr ss
93+ -> g (Rec FieldRepr ss)
94+
95+ -- | The getter of the 'fsubset' lens is 'fcast', which takes a larger record
96+ -- to a smaller one by forgetting fields.
97+ fcast
98+ :: Rec FieldRepr ss
99+ -> Rec FieldRepr rs
100+ fcast = getConst . fsubset Const
101+ {-# INLINE fcast #-}
102+
103+ -- | The setter of the 'fsubset' lens is 'freplace', which allows a slice of
104+ -- a record to be replaced with different values.
105+ freplace
106+ :: Rec FieldRepr rs
107+ -> Rec FieldRepr ss
108+ -> Rec FieldRepr ss
109+ freplace rs = getIdentity . fsubset (\_ -> Identity rs)
110+ {-# INLINE freplace #-}
111+
112+instance FSubset '[] ss '[] where
113+ fsubset = lens (const RNil) const
114+
115+instance
116+ ( ByRevision fn ss i ~ s
117+ , FElem fn ss i
118+ , FSubset rs ss is
119+ ) => FSubset ( '(fn,s) ': rs) ss (i ': is) where
120+ fsubset = lens (\ss -> fget Proxy ss :& fcast ss) set
121+ where
122+ set :: Rec FieldRepr ss -> Rec FieldRepr ( '(fn,s) ': rs) -> Rec FieldRepr ss
123+ set ss (r :& rs) = fput r $ freplace rs ss