Add ApSingle

Data/Row/Dictionaries.hs

@@ -21,9 +21,9 @@
 
 
 module Data.Row.Dictionaries
-  ( uniqueMap, uniqueAp, uniqueZip
-  , extendHas, mapHas, apHas
-  , mapExtendSwap, apExtendSwap, zipExtendSwap
+  ( uniqueMap, uniqueAp, uniqueApSingle, uniqueZip
+  , extendHas, mapHas, apHas, apSingleHas
+  , mapExtendSwap, apExtendSwap, apSingleExtendSwap, zipExtendSwap
   , FreeForall
   , FreeBiForall
   , freeForall
@@ -93,14 +93,22 @@ mapHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ t)
 apHas :: forall ϕ ρ l f t. (ϕ .! l ≈ f, ρ .! l ≈ t) :- (Ap ϕ ρ .! l ≈ f t, Ap ϕ ρ .- l ≈ Ap (ϕ .- l) (ρ .- l))
 apHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(ϕ .! l ≈ f, ρ .! l ≈ t)
 
+-- | This allows us to derive `ApSingle r x .! l ≈ f x` from `r .! l ≈ f`
+apSingleHas :: forall r l f x. (r .! l ≈ f) :- (ApSingle r x .! l ≈ f x, ApSingle r x .- l ≈ ApSingle (r .- l) x)
+apSingleHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ f)
+
 -- | Proof that the 'Map' type family preserves labels and their ordering.
 mapExtendSwap :: forall ℓ τ r f. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
 mapExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
 
 -- | Proof that the 'Ap' type family preserves labels and their ordering.
-apExtendSwap :: forall k ℓ (τ :: k) r (f :: k -> *) fs. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
+apExtendSwap :: forall ℓ (τ :: k) r (f :: k -> *) fs. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
 apExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
 
+-- | Proof that the 'ApSingle' type family preserves labels and their ordering.
+apSingleExtendSwap :: forall k ℓ (τ :: k) r (f :: k -> *). Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
+apSingleExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
 -- | Proof that the 'Ap' type family preserves labels and their ordering.
 zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
 zipExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
@@ -113,6 +121,10 @@ uniqueMap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
 uniqueAp :: forall r fs. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
 uniqueAp = UNSAFE.unsafeCoerce $ Dict @Unconstrained
 
+-- | ApSingle preserves uniqueness of labels.
+uniqueApSingle :: forall r x. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
+uniqueApSingle = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
 -- | Zip preserves uniqueness of labels.
 uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
 uniqueZip = UNSAFE.unsafeCoerce $ Dict @Unconstrained

Data/Row/Internal.hs

@@ -49,7 +49,7 @@ module Data.Row.Internal
   , FrontExtends(..)
   , FrontExtendsDict(..)
   , WellBehaved, AllUniqueLabels
-  , Ap, Zip, Map, Subset, Disjoint
+  , Ap, ApSingle, Zip, Map, Subset, Disjoint
   -- * Helper functions
   , Labels, labels, labels'
   , show'
@@ -398,6 +398,14 @@ type family ApR (fs :: [LT (a -> b)]) (r :: [LT a]) :: [LT b] where
   ApR (l :-> f ': tf) (l :-> v ': tv) = l :-> f v ': ApR tf tv
   ApR _ _ = TypeError (TL.Text "Row types with different label sets cannot be App'd together.")
 
+-- | Take a row of type operators and apply each to the second argument.
+type family ApSingle (fs :: Row (a -> b)) (x :: a) :: Row b where
+  ApSingle (R fs) x = R (ApSingleR fs x)
+
+type family ApSingleR (fs :: [LT (a -> b)]) (x :: a) :: [LT b] where
+  ApSingleR '[] _ = '[]
+  ApSingleR (l ':-> f ': fs) x = l ':-> f x ': ApSingleR fs x
+
 -- | Zips two rows together to create a Row of the pairs.
 --   The two rows must have the same set of labels.
 type family Zip (r1 :: Row *) (r2 :: Row *) where

Data/Row/Variants.hs

@@ -60,6 +60,8 @@ module Data.Row.Variants
   , compose, uncompose
   -- ** labels
   , labels
+  -- ** ApSingle functions
+  , eraseSingle, mapSingle, eraseZipSingle
   -- ** Coerce
   , coerceVar
   )
@@ -72,6 +74,7 @@ import Control.Arrow       ((+++), left, right)
 import Control.DeepSeq     (NFData(..), deepseq)
 
 import Data.Coerce
+import Data.Constraint                (Constraint)
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Functor.Product
@@ -408,6 +411,111 @@ fromLabels mk = getCompose $ metamorph @_ @ρ @c @FlipConst @(Const ()) @(Compos
         doCons l (FlipConst (Compose v)) = Compose $ IsJust l <$> mk l <|> extend @τ l <$> v
           \\ extendHas @ρ @ℓ @τ
 
+{--------------------------------------------------------------------
+  Functions for variants of ApSingle
+--------------------------------------------------------------------}
+
+newtype VApS x (fs :: Row (* -> *)) = VApS { unVApS :: Var (ApSingle fs x) }
+newtype FlipApp (x :: *) (f :: * -> *) = FlipApp (f x)
+
+eraseSingle
+  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
+   . (Forall fs c)
+  => (forall f . (c f) => f x -> y)
+  -> Var (ApSingle fs x)
+  -> y
+eraseSingle f =
+  getConst
+    . metamorph @_ @fs @c @Either @(VApS x) @(Const y) @(FlipApp x)
+        Proxy
+        doNil
+        doUncons
+        doCons
+    . VApS
+ where
+  doNil = impossible . unVApS
+
+  doUncons
+    :: forall l f fs
+      . ( c f
+        , fs .! l ≈ f
+        , KnownSymbol l
+        )
+    => Label l
+    -> VApS x fs
+    -> Either (FlipApp x f) (VApS x (fs .- l))
+  doUncons l = (FlipApp +++ VApS) . (flip trial l \\ apSingleHas @fs @l @f @x) . unVApS
+
+  doCons
+    :: forall l f fs
+     . (c f)
+    => Label l
+    -> Either (FlipApp x f) (Const y fs)
+    -> Const y (Extend l f fs)
+  doCons _ (Left (FlipApp v)) = Const (f v)
+  doCons _ (Right (Const  y)) = Const y
+
+mapSingle
+  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
+   . (Forall fs c)
+  => (forall f . (c f) => f x -> f y)
+  -> Var (ApSingle fs x)
+  -> Var (ApSingle fs y)
+mapSingle f = unVApS . metamorph @_ @fs @c @Either @(VApS x) @(VApS y) @(FlipApp x)
+             Proxy doNil doUncons doCons . VApS
+ where
+  doNil = impossible . unVApS
+
+  doUncons :: forall l f fs
+           .  ( c f, fs .! l ≈ f, KnownSymbol l)
+           => Label l -> VApS x fs -> Either (FlipApp x f) (VApS x (fs .- l))
+  doUncons l = (FlipApp +++ VApS)
+             . flip (trial \\ apSingleHas @fs @l @f @x) l
+             . unVApS
+
+  doCons :: forall l f fs. (KnownSymbol l, c f)
+         => Label l
+         -> Either (FlipApp x f) (VApS y fs)
+         -> VApS y (Extend l f fs)
+  doCons (toKey -> l) (Left (FlipApp x)) = VApS . OneOf l . HideType $ f x
+  doCons l (Right (VApS v)) = VApS $
+    extend @(f y) l v
+      \\ apSingleExtendSwap @_ @l @y @fs @f
+
+eraseZipSingle :: forall c fs (x :: *) (y :: *) z
+                . (Forall fs c)
+               => (forall f. c f => f x -> f y -> z)
+               -> Var (ApSingle fs x) -> Var (ApSingle fs y) -> Maybe z
+eraseZipSingle f x y = getConst $ metamorph @_ @fs @c @Either
+    @(Product (VApS x) (VApS y)) @(Const (Maybe z)) @(Const (Maybe z))
+    Proxy doNil doUncons doCons (Pair (VApS x) (VApS y))
+
+  where doNil :: Product (VApS x) (VApS y) Empty
+              -> Const (Maybe z) (Empty :: Row (* -> *))
+        doNil (Pair (VApS z) _) = Const (impossible z)
+
+        doUncons :: forall l f ρ
+                  . (KnownSymbol l, c f, ρ .! l ≈ f)
+                 => Label l
+                 -> Product (VApS x) (VApS y) ρ
+                 -> Either (Const (Maybe z) f)
+                           (Product (VApS x) (VApS y) (ρ .- l))
+        doUncons l (Pair (VApS r1) (VApS r2)) =
+          case (
+            trial r1 l \\ apSingleHas @ρ @l @f @x,
+            trial r2 l \\ apSingleHas @ρ @l @f @y
+          ) of
+            (Left u, Left v)     -> Left $ Const $ Just $ f @f u v
+            (Right us, Right vs) -> Right (Pair (VApS us) (VApS vs))
+            _                    -> Left $ Const Nothing
+
+        doCons :: forall l (τ :: * -> *) ρ
+                . Label l
+               -> Either (Const (Maybe z) τ) (Const (Maybe z) ρ)
+               -> Const (Maybe z) (Extend l τ ρ)
+        doCons _ (Left (Const w))  = Const w
+        doCons _ (Right (Const w)) = Const w
+
 {--------------------------------------------------------------------
   Generic instance
 --------------------------------------------------------------------}