row-types 0.2.3.0 → 0.3.0.0

raw patch · 9 files changed

+767/−146 lines, 9 filesdep +generic-lensdep +profunctorsPVP ok

version bump matches the API change (PVP)

Dependencies added: generic-lens, profunctors

API changes (from Hackage documentation)

Files

• CHANGELOG.md +25/−7
• Data/Row.hs +6/−8
• Data/Row/Internal.hs +133/−55
• Data/Row/Records.hs +203/−23
• Data/Row/Variants.hs +236/−13
• README.md +6/−0
• benchmarks/perf/Main.hs +73/−11
• examples/Examples.lhs +79/−28
• row-types.cabal +6/−1

@@ -1,14 +1,32 @@+## 0.3.0.0 [2019-05-28]+- Added `HasField` and `AsConstructor` instances (from generic-lens) for `Rec` and `Var` respectively.+- Added record-overwrite function `.//`.+- Added `Generic` instances for Rec and Var.+- Added mapHas entailment connecting `Map f r .! l` to `r .! l`.+- Changed `Forall2` to `BiForall`.+  - Added `BiConstraint` type class for use  with `BiForall`.+- Added `Ap` type family that functions as `ap` over rows using zipping.+  - Added `mapF` to map a function over a record with an `Ap` row.+- Added `toDynamicMap` and `fromDynamicMap` as functions to convert between `Rec`s and  `HashMap Text Dynamic`s.+- Added `toNativeExact` to convert a `Rec` to a native Haskell type without losing any fields.+- Added `toNative`, `fromNative`, and `fromNativeExact` for `Var`s.+- Added `unSingleton` for `Var`s.+  - Removed `unSingleton` from `Data.Row` export list.+- Tightened the type signatures of `focus` (for both `Rec` and `Var`) to improve type inference when using `focus` in lens-like situations. +## 0.2.3.1 [2018-07-11]+- Fix a bug in the `Show` instance for `Rec`.+ ## 0.2.3.0 [2018-07-02]-- Update the Show instance to render valid code.-- Add 'toNative' and 'fromNative' functions for records to easily convert between Haskell records and row-types records.-- Make type families in Data.Row.Internal polykinded (thanks James Yu!)+- Update the `Show` instance for `Rec` to render valid code.+- Add `toNative` and `fromNative` functions for records to easily convert between Haskell records and row-types records.+- Make type families in `Data.Row.Internal` polykinded (thanks James Yu!)  ## 0.2.1.0 [2018-03-20]-- Bug Fix: The type of 'update' for both Record and Variant now enforce the newly inserted type is correct.-- New: Add 'restrict' and 'split' for Variants.  -- - Removed 'restrict' from Data.Row export list.-- New: Added support for universally quantified rows: 'mapForall' and 'uniqueMap'.+- Bug Fix: The type of `update` for both `Rec` and `Var` now enforce the newly inserted type is correct.+- New: Add `restrict` and `split` for `Var`s.  +  - Removed `restrict` from `Data.Row` export list.+- New: Added support for universally quantified rows: `mapForall` and `uniqueMap`. - Added very simple test suite.  ## 0.2.0.0 [2018-02-12]

@@ -28,23 +28,24 @@   , KnownSymbol, AllUniqueLabels, WellBehaved   , Var, Rec, Row, Empty, type (≈)   , HasType, Lacks, type (.\), type (.+)+  , type (.\/), type (.\\), type (.//)   , Forall, Switch(..)   -- * Record Construction   , empty-  , type (.==), (.==), pattern (:==), unSingleton+  , type (.==), (.==), pattern (:==)   -- ** Restriction   , type (.-), (.-)   -- ** Query   , type (.!), (.!)-  -- ** Disjoint union+  -- ** Union   , (.+), Disjoint, pattern (:+)+  , (.//)   -- * Variant construction   , pattern IsJust-  -- ** Restriction-  , diversify, type (.\/)+  -- ** Expansion+  , diversify   -- ** Destruction   , impossible, trial, trial', multiTrial-  , type (.\\)   -- * Labels   , labels   )@@ -53,6 +54,3 @@ import Data.Row.Variants import Data.Row.Records import Data.Row.Switch---

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE UndecidableSuperClasses #-} ----------------------------------------------------------------------------- -- | -- Module      :  Data.Row.Internal@@ -19,26 +20,30 @@   , HideType(..)   -- * Row Operations   , Extend, Modify, Rename-  , type (.\), type (.!), type (.-), type (.+), type (.\\), type (.==)-  , type (.\/)-  , Lacks, HasType-  -- * Row Classes-  , Labels, labels, labels'-  , Forall(..), Forall2(..)+  , type (.==), type (.!), type (.-), type (.\\)+  -- $merges+  , type (.+), type (.\/), type (.//)+  -- * Row Constraints+  , Lacks, type (.\), HasType+  , Forall(..)+  , BiForall(..)+  , BiConstraint   , Unconstrained1+  , Unconstrained2+  , WellBehaved, AllUniqueLabels+  , Ap, Zip, Map, Subset, Disjoint   -- * Helper functions+  , Labels, labels, labels'   , show'   , toKey   , type (≈)-  , WellBehaved, AllUniqueLabels, Zip, Map, Subset, Disjoint    , mapForall   , freeForall   , uniqueMap+  , mapHas   , IsA(..)   , As(..)--  , FoldStep   ) where @@ -76,6 +81,7 @@  -- | A label data Label (s :: Symbol) = Label+  deriving (Eq)  instance KnownSymbol s => Show (Label s) where   show = symbolVal@@ -135,23 +141,50 @@ type family (r :: Row k) .- (s :: Symbol) :: Row k where   R r .- l = R (Remove l r) -infixl 6 .+--- | Type level Row append-type family (l :: Row k) .+ (r :: Row k) :: Row k where-  R l .+ R r = R (Merge l r)- infixl 6 .\\ {- This comment needed to appease CPP -}--- | Type level Row difference.  That is, @l .\\\\ r@ is the row remaining after+-- | Type level Row difference.  That is, @l '.\\' r@ is the row remaining after -- removing any matching elements of @r@ from @l@. type family (l :: Row k) .\\ (r :: Row k) :: Row k where   R l .\\ R r = R (Diff l r) +-- $merges+-- == Various row-type merges+-- The difference between '.+' (read "append"), '.\/' (read "min-join"), and+-- '.\\' (read "const-union") comes down to how duplicates are handled.+-- In '.+', the two given row-types must be entirely unique.  Even the same+-- entry in both row-types is forbidden.  In '.\/', this final restriction is+-- relaxed, allowing two row-types that have no conflicts to be merged in the+-- logical way.  The '.\\' operator is the most liberal, allowing any two row-types+-- to be merged together, and whenever there is a conflict, favoring the left argument.+--+-- As examples of use:+--+-- - '.+' is used when appending two records, assuring that those two records are+--   entirely disjoint.+--+-- - '.\/' is used when diversifying a variant, allowing some extension to the+--   row-type so long as no original types have changed.+--+-- - './/' is used when doing record overwrite, allowing data in a record to+-- totally overwrite what was previously there.++infixl 6 .++-- | Type level Row append+type family (l :: Row k) .+ (r :: Row k) :: Row k where+  R l .+ R r = R (Merge l r)+ infixl 6 .\/ -- | The minimum join of the two rows. type family (l :: Row k) .\/ (r :: Row k) where   R l .\/ R r = R (MinJoinR l r) +infixl 6 .//+-- | The overwriting union, where the left row overwrites the types of the right+-- row where the labels overlap.+type family (l :: Row k) .// (r :: Row k) where+  R l .// R r = R (ConstUnionR l r) + {--------------------------------------------------------------------   Syntactic sugar for record operations --------------------------------------------------------------------}@@ -175,11 +208,6 @@   Constrained record operations --------------------------------------------------------------------} --- | Proof that the given label is a valid candidate for the next step--- in a metamorph fold, i.e. it's not in the list yet and, when sorted,--- will be placed at the head.-type FoldStep ℓ τ ρ = Inject (ℓ :-> τ) ρ ≈ ℓ :-> τ ': ρ- -- | Any structure over a row in which every element is similarly constrained can --   be metamorphized into another structure over the same row. class Forall (r :: Row k) (c :: k -> Constraint) where@@ -191,7 +219,7 @@                -- ^ The way to transform the empty element             -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> (h τ, f ('R ρ)))                -- ^ The unfold-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))                -- ^ The fold             -> f r  -- ^ The input structure             -> g r@@ -204,7 +232,7 @@                -- ^ The way to transform the empty element             -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> Either (h τ) (f ('R ρ)))                -- ^ The unfold-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))                -- ^ The fold             -> f r  -- ^ The input structure             -> g r@@ -236,12 +264,10 @@                => Label l -> Const () ('R (l :-> t ': r)) -> (Const () t, Const () ('R r))         uncons _ _ = (Const (), Const ()) -        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ)+        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)              => Label ℓ -> Const () τ -> MapForall c f ('R ρ)              -> MapForall c f ('R (ℓ :-> τ ': ρ))-        cons _ _ (MapForall Dict) =-           case UNSAFE.unsafeCoerce @(Dict Unconstrained) @(Dict (FoldStep ℓ (f τ) (MapR f ρ))) Dict of-             Dict -> MapForall Dict+        cons _ _ (MapForall Dict) = MapForall Dict  -- | Map preserves uniqueness of labels. uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)@@ -251,20 +277,24 @@ freeForall :: forall r c. Forall r c :- Forall r Unconstrained1 freeForall = Sub $ UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict +-- | This allows us to derive `Map f r .! l ≈ f t` from `r .! l ≈ t`+mapHas :: forall f r l t. (r .! l ≈ t) :- (Map f r .! l ≈ f t)+mapHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ t)+ instance Forall (R '[]) c where   {-# INLINE metamorph #-}   metamorph _ empty _ _ = empty   {-# INLINE metamorph' #-}   metamorph' _ empty _ _ = empty -instance (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ, Forall ('R ρ) c) => Forall ('R (ℓ :-> τ ': ρ) :: Row k) c where+instance (KnownSymbol ℓ, c τ, Forall ('R ρ) c) => Forall ('R (ℓ :-> τ ': ρ) :: Row k) c where   metamorph :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).                Proxy h             -> (f Empty -> g Empty)                -- ^ The way to transform the empty element             -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> (h τ, f ('R ρ)))                -- ^ The unfold-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))                -- ^ The fold             -> f ('R (ℓ :-> τ ': ρ))  -- ^ The input structure             -> g ('R (ℓ :-> τ ': ρ))@@ -277,43 +307,59 @@                -- ^ The way to transform the empty element             -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> Either (h τ) (f ('R ρ)))                -- ^ The unfold-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))                -- ^ The fold             -> f ('R (ℓ :-> τ ': ρ))  -- ^ The input structure             -> g ('R (ℓ :-> τ ': ρ))   {-# INLINE metamorph' #-}   metamorph' _ empty uncons cons r = cons Label $ metamorph' @_ @('R ρ) @c @_ @_ @h Proxy empty uncons cons <$> uncons Label r --- | Any structure over two rows in which every element of both rows satisfies the---   given constraint can be metamorphized into another structure over both of the+-- | Any structure over two rows in which the elements of each row satisfy some+--   constraints can be metamorphized into another structure over both of the --   rows.--- TODO: Perhaps it should be over two constraints?  But this hasn't seemed necessary---  in practice.-class Forall2 (r1 :: Row k) (r2 :: Row k) (c :: k -> Constraint) where-  -- | A metamorphism is a fold followed by an unfold.  Here, we fold both of the inputs.-  metamorph2 :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: Row k -> Row k -> *)-                       (f' :: k -> *) (g' :: k -> *).-                Proxy f' -> Proxy g'-             -> (f Empty -> g Empty -> h Empty Empty)-             -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2)-                 => Label ℓ-                 -> f ('R (ℓ :-> τ1 ': ρ1))-                 -> g ('R (ℓ :-> τ2 ': ρ2))-                 -> ((f' τ1, f ('R ρ1)), (g' τ2, g ('R ρ2))))-             -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1, c τ2)-                 => Label ℓ -> f' τ1 -> g' τ2 -> h ('R ρ1) ('R ρ2) -> h ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)))-             -> f r1 -> g r2 -> h r1 r2+class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) where+  -- | A metamorphism is a fold followed by an unfold.  This one is for+  -- product-like row-types.+  biMetamorph :: forall (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)+                        (h :: k1 -> k2 -> *).+                 Proxy h+              -> (f Empty Empty -> g Empty Empty)+              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)+                  => Label ℓ+                  -> f ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))+                  -> (h τ1 τ2, f ('R ρ1) ('R ρ2)))+              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)+                  => Label ℓ -> h τ1 τ2 -> g ('R ρ1) ('R ρ2) -> g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)))+              -> f r1 r2 -> g r1 r2 -instance Forall2 (R '[]) (R '[]) c where-  {-# INLINE metamorph2 #-}-  metamorph2 _ _ empty _ _ = empty+  -- | A metamorphism is a fold followed by an unfold.  This one is for+  -- sum-like row-types.+  biMetamorph' :: forall (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)+                         (h :: k1 -> k2 -> *).+                  Proxy h+               -> (f Empty Empty -> g Empty Empty)+               -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)+                   => Label ℓ+                   -> f ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))+                   -> Either (h τ1 τ2) (f ('R ρ1) ('R ρ2)))+               -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)+                   => Label ℓ -> Either (h τ1 τ2) (g ('R ρ1) ('R ρ2)) -> g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)))+               -> f r1 r2 -> g r1 r2 -instance (KnownSymbol ℓ, c τ1, c τ2, Forall2 ('R ρ1) ('R ρ2) c)-      => Forall2 ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)) c where-  {-# INLINE metamorph2 #-}-  metamorph2 f g empty uncons cons r1 r2 = cons (Label @ℓ) t1 t2 $ metamorph2 @_ @('R ρ1) @('R ρ2) @c f g empty uncons cons r1' r2'-    where ((t1, r1'), (t2, r2')) = uncons (Label @ℓ) r1 r2+instance BiForall (R '[]) (R '[]) c1 where+  {-# INLINE biMetamorph #-}+  biMetamorph _ empty _ _ = empty+  biMetamorph' _ empty _ _ = empty +instance (KnownSymbol ℓ, c τ1 τ2, BiForall ('R ρ1) ('R ρ2) c)+      => BiForall ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)) c where+  {-# INLINE biMetamorph #-}+  biMetamorph h empty uncons cons r = cons (Label @ℓ) t $ biMetamorph @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons r'+    where (t, r') = uncons (Label @ℓ) r+  {-# INLINE biMetamorph' #-}+  biMetamorph' h empty uncons cons r =+    cons (Label @ℓ) $ biMetamorph' @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons <$> uncons (Label @ℓ) r+ -- | A null constraint class Unconstrained instance Unconstrained@@ -322,6 +368,14 @@ class Unconstrained1 a instance Unconstrained1 a +-- | A null constraint of two arguments+class Unconstrained2 a b+instance Unconstrained2 a b++-- | A pair of constraints+class (c1 x, c2 y) => BiConstraint c1 c2 x y+instance (c1 x, c2 y) => BiConstraint c1 c2 x y+ -- | The labels in a Row. type family Labels (r :: Row a) where   Labels (R '[]) = '[]@@ -394,6 +448,16 @@   MapR f '[] = '[]   MapR f (l :-> v ': t) = l :-> f v ': MapR f t +-- | Take two rows with the same labels, and apply the type operator from the+-- first row to the type of the second.+type family Ap (fs :: Row (a -> b)) (r :: Row a) :: Row b where+  Ap (R fs) (R r) = R (ApR fs r)++type family ApR (fs :: [LT (a -> b)]) (r :: [LT a]) :: [LT b] where+  ApR '[] '[] = '[]+  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.")+ -- | 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@@ -451,9 +515,13 @@                                     :<>: TL.Text " already exists in " :<>: ShowType r)   LacksR l (l' :-> _ ': x) r = Ifte (l <=.? l') Unconstrained (LacksR l x r) + type family Merge (l :: [LT k]) (r :: [LT k]) where   Merge '[] r = r   Merge l '[] = l+  Merge (h :-> a ': tl)   (h :-> a ': tr) =+    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " (of type "+          :$$: ShowType a :<>: TL.Text ") has duplicate assignments.")   Merge (h :-> a ': tl)   (h :-> b ': tr) =     TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."           :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")@@ -474,6 +542,16 @@       Ifte (CmpSymbol hl hr == 'LT)       (hl :-> al ': MinJoinR tl (hr :-> ar ': tr))       (hr :-> ar ': MinJoinR (hl :-> al ': tl) tr)++type family ConstUnionR (l :: [LT k]) (r :: [LT k]) where+  ConstUnionR '[] r = r+  ConstUnionR l '[] = l+  ConstUnionR (h :-> a ': tl)   (h :-> b ': tr) =+      (h :-> a ': ConstUnionR tl tr)+  ConstUnionR (hl :-> al ': tl) (hr :-> ar ': tr) =+      Ifte (CmpSymbol hl hr == 'LT)+      (hl :-> al ': ConstUnionR tl (hr :-> ar ': tr))+      (hr :-> ar ': ConstUnionR (hl :-> al ': tl) tr)   -- | Returns the left list with all of the elements from the right list removed.

@@ -38,12 +38,16 @@   -- * Combine   -- ** Disjoint union   , type (.+), (.+), Disjoint, pattern (:+)+  -- ** Overwrite+  , type (.//), (.//)   -- * Native Conversion   -- $native-  , toNative, fromNative+  , toNative, toNativeExact, fromNative+  -- * Dynamic Conversion+  , toDynamicMap, fromDynamicMap   -- * Row operations   -- ** Map-  , Map, map, map'+  , Map, map, map', mapF   , transform, transform'   -- ** Fold   , Forall, erase, eraseWithLabels, eraseZip, eraseToHashMap@@ -66,21 +70,24 @@  import Control.DeepSeq (NFData(..), deepseq) -import Data.Constraint ((\\))-import Data.Functor.Compose-import Data.Functor.Const-import Data.Functor.Identity-import Data.Functor.Product-import Data.Hashable-import Data.HashMap.Lazy (HashMap)-import qualified Data.HashMap.Lazy as M-import qualified Data.List as L-import Data.Proxy-import Data.String (IsString)-import Data.Text (Text)+import           Data.Constraint              ((\\))+import           Data.Dynamic+import           Data.Functor.Compose+import           Data.Functor.Const+import           Data.Functor.Identity+import           Data.Functor.Product+import           Data.Generics.Product.Fields (HasField(..), HasField'(..))+import           Data.Hashable+import           Data.HashMap.Lazy            (HashMap)+import qualified Data.HashMap.Lazy            as M+import qualified Data.List                    as L+import           Data.Monoid                  (Endo(..), appEndo)+import           Data.Proxy+import           Data.String                  (IsString)+import           Data.Text                    (Text)  import qualified GHC.Generics as G-import GHC.TypeLits+import           GHC.TypeLits  import Unsafe.Coerce @@ -102,7 +109,7 @@       xs ->         showParen           (p > 6)-          (mconcat (L.intersperse (showString " .+ ") (L.map binds xs)))+          (appEndo $ foldMap Endo (L.intersperse (showString " .+ ") (L.map binds xs)))     where       binds (label, value) =         showChar '#' .@@ -166,7 +173,14 @@ update (toKey -> l) a (OR m) = OR $ M.adjust f l m where f = const (HideType a)  -- | Focus on the value associated with the label.-focus :: (Functor f, KnownSymbol l) => Label l -> (r .! l -> f a) -> Rec r -> f (Rec (Modify l a r))+focus ::+  ( KnownSymbol l+  , r' .! l ≈ b+  , r  .! l ≈ a+  , r' ~ Modify l b r+  , r  ~ Modify l a r'+  , Functor f)+  => Label l -> (a -> f b) -> Rec r -> f (Rec r') focus (toKey -> l) f (OR m) = case m M.! l of   HideType x -> OR . flip (M.insert l) m . HideType <$> f (unsafeCoerce x) @@ -198,6 +212,20 @@ (.+) :: Rec l -> Rec r -> Rec (l .+ r) OR l .+ OR r = OR $ M.unionWith (error "Impossible") l r +-- | Record overwrite.+--+-- The operation @r .// r'@ creates a new record such that:+--+-- - Any label that is in both @r@ and @r'@ is in the resulting record with the+--   type and value given by the fields in @r@,+--+-- - Any label that is only found in @r@ is in the resulting record.+--+-- - Any label that is only found in @r'@ is in the resulting record.+--+-- This can be thought of as @r@ "overwriting" @r'@.+(.//) :: Rec r -> Rec r' -> Rec (r .// r')+OR l .// OR r = OR $ M.union l r  -- | A pattern version of record union, for use in pattern matching. {-# COMPLETE (:+) #-}@@ -287,11 +315,28 @@            => Label ℓ -> Identity τ -> RMap f ('R ρ) -> RMap f ('R (ℓ :-> τ ': ρ))     doCons l (Identity v) (RMap r) = RMap (unsafeInjectFront l (f v) r) +newtype RFMap (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1) = RFMap { unRFMap :: Rec (Ap ϕ (Map g ρ)) }+newtype RecAp (ϕ :: Row (k -> *)) (ρ :: Row k) = RecAp (Rec (Ap ϕ ρ))+newtype App (f :: k -> *) (a :: k) = App (f a)++-- | A function to map over a Ap record given constraints.+mapF :: forall c g (ϕ :: Row (k -> *)) (ρ :: Row k). BiForall ϕ ρ c+     => (forall f a. (c f a) => f a -> f (g a))+     -> Rec (Ap ϕ ρ)+     -> Rec (Ap ϕ (Map g ρ))+mapF f = unRFMap . biMetamorph @_ @_ @ϕ @ρ @c @RecAp @(RFMap g) @App Proxy doNil doUncons doCons . RecAp+  where+    doNil _ = RFMap empty+    doUncons l (RecAp r) = (App $ r .! l, RecAp $ unsafeRemove l r)+    doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)+           => Label ℓ -> App τ1 τ2 -> RFMap g ('R ρ1) ('R ρ2) -> RFMap g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))+    doCons l (App v) (RFMap r) = RFMap (unsafeInjectFront l (f @τ1 @τ2 v) r)+ -- | A function to map over a record given no constraint. map' :: forall f r. Forall r Unconstrained1 => (forall a. a -> f a) -> Rec r -> Rec (Map f r) map' = map @Unconstrained1 --- | Lifts a natrual transformation over a record.  In other words, it acts as a+-- | Lifts a natural transformation over a record.  In other words, it acts as a -- record transformer to convert a record of @f a@ values to a record of @g a@ -- values.  If no constraint is needed, instantiate the first type argument with -- 'Unconstrained1' or use 'transform''.@@ -364,15 +409,16 @@   -- | RZipPair is used internally as a type level lambda for zipping records.+newtype RecPair  (ρ1 :: Row *) (ρ2 :: Row *) = RecPair  (Rec ρ1, Rec ρ2) newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { unRZipPair :: Rec (Zip ρ1 ρ2) }  -- | Zips together two records that have the same set of labels.-zip :: forall r1 r2. Forall2 r1 r2 Unconstrained1 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)-zip r1 r2 = unRZipPair $ metamorph2 @_ @r1 @r2 @Unconstrained1 @Rec @Rec @RZipPair @Identity @Identity Proxy Proxy doNil doUncons doCons r1 r2+zip :: forall r1 r2. BiForall r1 r2 Unconstrained2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)+zip r1 r2 = unRZipPair $ biMetamorph @_ @_ @r1 @r2 @Unconstrained2 @RecPair @RZipPair @(,) Proxy doNil doUncons doCons $ RecPair (r1, r2)   where-    doNil _ _ = RZipPair empty-    doUncons l r1 r2 = ((Identity $ r1 .! l, unsafeRemove l r1), (Identity $ r2 .! l, unsafeRemove l r2))-    doCons l (Identity v1) (Identity v2) (RZipPair r) = RZipPair $ unsafeInjectFront l (v1, v2) r+    doNil _ = RZipPair empty+    doUncons l (RecPair (r1, r2)) = ((r1 .! l, r2 .! l), RecPair (unsafeRemove l r1, unsafeRemove l r2))+    doCons l (v1, v2) (RZipPair r) = RZipPair $ unsafeInjectFront l (v1, v2) r  -- | A helper function for unsafely adding an element to the front of a record. -- This can cause the resulting record to be malformed, for instance, if the record@@ -380,6 +426,7 @@ -- Realistically, this function should only be used when writing calls to 'metamorph'. unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R (l :-> a ': r)) unsafeInjectFront (toKey -> a) b (OR m) = OR $ M.insert a (HideType b) m+{-# INLINE unsafeInjectFront #-}   {--------------------------------------------------------------------@@ -421,7 +468,76 @@    where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a          inner l = case as @c @g @a of As -> f l + {--------------------------------------------------------------------+  Dynamic compatibility+--------------------------------------------------------------------}++-- | Converts a 'Rec' into a 'HashMap' of 'Dynamic's.+toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic+toDynamicMap = eraseToHashMap @Typeable @_ @Text @Dynamic toDyn++-- | Produces a 'Rec' from a 'HashMap' of 'Dynamic's.+fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable)+               => HashMap Text Dynamic -> Maybe (Rec r)+fromDynamicMap m = fromLabelsA @Typeable+  $ \ (toKey -> k) -> M.lookup k m >>= fromDynamic+++{--------------------------------------------------------------------+  Generic instance+--------------------------------------------------------------------}++-- The generic structure we want Recs to have is not the hidden internal one,+-- but rather one that appears as a Haskell record.  Thus, we can't derive+-- Generic automatically.+--+-- The following Generic instance creates a representation of a Rec that is+-- very similar to a native Haskell record except that the tree of pairs (':*:')+-- that it produces will be extremely unbalanced.  I don't think this is a problem.+-- Furthermore, because we don't want Recs to always have a trailing unit on+-- the end, we must have a special case for singleton Recs.  This means that+-- we can't use metamorph and that we must use an overlappable instance for+-- larger records.++instance GenericRec r => G.Generic (Rec r) where+  type Rep (Rec r) =+    G.D1 ('G.MetaData "Rec" "Data.Row.Records" "row-types" 'False)+      (G.C1 ('G.MetaCons "Rec" 'G.PrefixI 'True)+        (RepRec r))+  from = G.M1 . G.M1 . fromRec+  to = toRec . G.unM1 . G.unM1++type family RepRec (r :: Row *) :: * -> * where+  RepRec (R '[])                 = G.U1+  RepRec (R (name :-> t ': '[])) = G.S1+    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)+    (G.Rec0 t)+  RepRec (R (name :-> t ': r))   = (G.S1+    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)+    (G.Rec0 t)) G.:*: RepRec (R r)++class GenericRec r where+  fromRec :: Rec r -> RepRec r x+  toRec   :: RepRec r x -> Rec r++instance GenericRec Empty where+  fromRec _ = G.U1+  toRec _ = empty++instance KnownSymbol name => GenericRec (R '[name :-> t]) where+  fromRec (_ :== a) = G.M1 (G.K1 a)+  toRec (G.M1 (G.K1 a)) = (Label @name) :== a++instance {-# OVERLAPPABLE #-}+    ( GenericRec (R r)+    , KnownSymbol name+    , r ~ (name' :-> t' ': r') -- r is not Empty+    ) => GenericRec (R (name :-> t ': r)) where+  fromRec r = G.M1 (G.K1 (r .! Label @name)) G.:*: fromRec (unsafeRemove @name Label r)+  toRec (G.M1 (G.K1 a) G.:*: r) = unsafeInjectFront (Label @name) a (toRec r)++{--------------------------------------------------------------------   Native data type compatibility --------------------------------------------------------------------} -- ToNative is shamelessly copied from@@ -448,6 +564,11 @@ -- Person {name = "Alice", age = 7} -- >>> fromNative $ Person "Bob" 9 -- { age=9, name="Bob" }+--+-- The 'toNativeExact' function is a more restricted version of 'toNative' that+-- does not allow fields to be dropped; in other words, the fields in the record+-- must exactly match the fields in the data type.  Because of this, 'toNativeExact'+-- and 'fromNative' compose to form the identity function.   -- | Conversion helper to bring a record back into a Haskell type. Note that the@@ -461,6 +582,9 @@ instance ToNative cs ρ => ToNative (G.C1 m cs) ρ where   toNative' xs = G.M1 $ toNative' xs +instance ToNative G.U1 ρ where+  toNative' _ = G.U1+ instance (KnownSymbol name, ρ .! name ≈ t)     => ToNative (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where   toNative' r = G.M1 $ G.K1 $ r .! (Label @name)@@ -474,6 +598,35 @@ toNative = G.to . toNative'  +-- | Conversion helper to bring a record back into a Haskell type. Note that the+-- native Haskell type must be an instance of 'Generic'.+class ToNativeExact a ρ where+  toNativeExact' :: Rec ρ -> a x++instance ToNativeExact cs ρ => ToNativeExact (G.D1 m cs) ρ where+  toNativeExact' xs = G.M1 $ toNativeExact' xs++instance ToNativeExact cs ρ => ToNativeExact (G.C1 m cs) ρ where+  toNativeExact' xs = G.M1 $ toNativeExact' xs++instance ToNativeExact G.U1 Empty where+  toNativeExact' _ = G.U1++instance (KnownSymbol name, ρ ≈ name .== t)+    => ToNativeExact (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where+  toNativeExact' r = G.M1 $ G.K1 $ r .! (Label @name)++instance (ToNativeExact l ρ₁, ToNativeExact r ρ₂, ρ ≈ ρ₁ .+ ρ₂, Disjoint ρ₁ ρ₂)+    => ToNativeExact (l G.:*: r) ρ where+  toNativeExact' r = toNativeExact' r1 G.:*: toNativeExact' r2+    where+      (r1 :: Rec ρ₁) :+ (r2 :: Rec ρ₂) = r++-- | Convert a record to an exactly matching native Haskell type.+toNativeExact :: forall t ρ. (G.Generic t, ToNativeExact (G.Rep t) ρ) => Rec ρ -> t+toNativeExact = G.to . toNativeExact'++ -- | Conversion helper to turn a Haskell record into a row-types extensible -- record. Note that the native Haskell type must be an instance of 'Generic'. class FromNative a ρ where@@ -485,6 +638,9 @@ instance FromNative cs ρ => FromNative (G.C1 m cs) ρ where   fromNative' (G.M1 xs) = fromNative' xs +instance FromNative G.U1 Empty where+  fromNative' G.U1 = empty+ instance (KnownSymbol name, ρ ≈ name .== t)     => FromNative (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where   fromNative' (G.M1 (G.K1 x)) =  (Label @name) .== x@@ -496,3 +652,27 @@ -- | Convert a Haskell record to a row-types Rec. fromNative :: forall t ρ. (G.Generic t, FromNative (G.Rep t) ρ) => t -> Rec ρ fromNative = fromNative' . G.from+++{--------------------------------------------------------------------+  Generic-lens compatibility+--------------------------------------------------------------------}++-- | Every field in a row-types based record has a 'HasField' instance.+instance {-# OVERLAPPING #-}+  ( KnownSymbol name+  , r' .! name ≈ b+  , r  .! name ≈ a+  , r' ~ Modify name b r+  , r  ~ Modify name a r')+  => HasField name (Rec r) (Rec r') a b where+  field = focus (Label @name)+  {-# INLINE field #-}++instance {-# OVERLAPPING #-}+  ( KnownSymbol name+  , r .! name ≈ a+  , r ~ Modify name a r)+  => HasField' name (Rec r) a where+  field' = focus (Label @name)+  {-# INLINE field' #-}

@@ -14,7 +14,7 @@   , KnownSymbol, AllUniqueLabels, WellBehaved   , Var, Row, Empty, type (≈)   -- * Construction-  , HasType, pattern IsJust, singleton+  , HasType, pattern IsJust, singleton, unSingleton   , fromLabels   -- ** Extension   , type (.\), Lacks, type (.\/), diversify, type (.+)@@ -25,6 +25,9 @@   , restrict, split   -- ** Types for destruction   , type (.!), type (.-), type (.\\), type (.==)+  -- * Native Conversion+  -- $native+  , toNative, fromNative, fromNativeExact   -- * Row operations   -- ** Map   , Map, map, map', transform, transform'@@ -42,21 +45,24 @@   ) where -import Prelude hiding (zip, map, sequence)+import Prelude hiding (map, sequence, zip)  import Control.Applicative-import Control.Arrow ((<<<), (+++), left, right)-import Control.DeepSeq (NFData(..), deepseq)+import Control.Arrow       ((<<<), (+++), left, right)+import Control.DeepSeq     (NFData(..), deepseq)  import Data.Functor.Compose import Data.Functor.Identity import Data.Functor.Product-import Data.Maybe (fromMaybe)+import Data.Generics.Sum.Constructors (AsConstructor(..), AsConstructor'(..))+import Data.Maybe                     (fromMaybe)+import Data.Profunctor                (Choice(..), Profunctor(..)) import Data.Proxy-import Data.String (IsString)-import Data.Text (Text)+import Data.String                    (IsString)+import Data.Text                      (Text) -import GHC.TypeLits+import qualified GHC.Generics as G+import           GHC.TypeLits  import Unsafe.Coerce @@ -112,14 +118,18 @@ singleton :: KnownSymbol l => Label l -> a -> Var (l .== a) singleton = IsJust +-- | A quick destructor for singleton variants.+unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)+unSingleton (OneOf _ (HideType x)) = (l, unsafeCoerce x) where l = Label @l+ -- | A pattern for variants; can be used to both destruct a variant -- when in a pattern position or construct one in an expression position. pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> r .! l -> Var r-pattern IsJust l a <- (unSingleton @l -> (l, Just a)) where+pattern IsJust l a <- (isJustHelper @l -> (l, Just a)) where         IsJust l a = unsafeMakeVar l a -unSingleton :: forall l r. KnownSymbol l => Var r -> (Label l, Maybe (r .! l))-unSingleton v = (l, view l v) where l = Label @l+isJustHelper :: forall l r. KnownSymbol l => Var r -> (Label l, Maybe (r .! l))+isJustHelper v = (l, view l v) where l = Label @l  -- | Make the variant arbitrarily more diverse. diversify :: forall r' r. Var r -> Var (r .\/ r')@@ -132,8 +142,25 @@  -- | If the variant exists at the given label, focus on the value associated with it. -- Otherwise, do nothing.-focus :: (Applicative f, KnownSymbol l) => Label l -> (r .! l -> f a) -> Var r -> f (Var (Modify l a r))-focus (toKey -> l') f (OneOf l (HideType x)) = if l == l' then (OneOf l . HideType) <$> f (unsafeCoerce x) else pure (OneOf l (HideType x))+focus :: forall l r r' a b p f.+  ( AllUniqueLabels r+  , AllUniqueLabels r'+  , KnownSymbol l+  , r  .! l ≈ a+  , r' .! l ≈ b+  , r' ≈ (r .- l) .\/ (l .== b)+  , Applicative f+  , Choice p+  ) => Label l -> p a (f b) -> p (Var r) (f (Var r'))+focus (toKey -> l) =+  dimap unwrap rewrap . left'+  where+    unwrap :: Var r -> Either a (Var r')+    unwrap (OneOf l' (HideType x))+      | l == l'   = Left (unsafeCoerce x)+      | otherwise = Right (OneOf l' (HideType x))+    rewrap :: Either (f b) (Var r') -> f (Var r')+    rewrap = either (fmap $ OneOf l . HideType) pure  -- | Rename the given label. rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)@@ -306,3 +333,199 @@         doCons l (Left _) = Compose $ unsafeMakeVar l <$> mk l --This case should be impossible         doCons l (Right (Compose v)) = Compose $           unsafeMakeVar l <$> mk l <|> unsafeInjectFront <$> v++{--------------------------------------------------------------------+  Generic instance+--------------------------------------------------------------------}++-- The generic structure we want Vars to have is not the hidden internal one,+-- but rather one that appears as a Haskell sum type.  Thus, we can't derive+-- Generic automatically.+--+-- The following Generic instance creates a representation of a Var that is+-- very similar to a native Haskell sum type except that the tree of possibilities (':+:')+-- that it produces will be extremely unbalanced.  I don't think this is a problem.+-- Furthermore, because we don't want Vars to always have a trailing void option on+-- the end, we must have a special case for singleton Vars.  This means that+-- we can't use metamorph and that we must use an overlappable instance for+-- larger variants.++instance GenericVar r => G.Generic (Var r) where+  type Rep (Var r) =+    G.D1 ('G.MetaData "Var" "Data.Row.Variants" "row-types" 'False) (RepVar r)+  from = G.M1 . fromVar+  to = toVar . G.unM1++type family RepVar (r :: Row *) :: * -> * where+  RepVar (R '[])                 = G.V1+  RepVar (R (name :-> t ': '[])) = G.C1+    ('G.MetaCons name 'G.PrefixI 'False)+    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)+          (G.Rec0 t))+  RepVar (R (name :-> t ': r))   = (G.C1+    ('G.MetaCons name 'G.PrefixI 'False)+    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)+          (G.Rec0 t)))  G.:+: RepVar (R r)++class GenericVar r where+  fromVar :: Var r -> RepVar r x+  toVar   :: RepVar r x -> Var r++instance GenericVar Empty where+  fromVar = impossible+  toVar = \case++instance KnownSymbol name => GenericVar (R '[name :-> t]) where+  fromVar (unSingleton -> (_, a)) = G.M1 (G.M1 (G.K1 a))+  toVar (G.M1 (G.M1 (G.K1 a))) = IsJust (Label @name) a++instance {-# OVERLAPPABLE #-}+    ( GenericVar (R r)+    , KnownSymbol name+    , r ~ (name' :-> t' ': r') -- r is not Empty+    , AllUniqueLabels (R (name :-> t ': r))+    ) => GenericVar (R (name :-> t ': r)) where+  fromVar v = case trial @name v Label of+    Left a   -> G.L1 (G.M1 (G.M1 (G.K1 a)))+    Right v' -> G.R1 (fromVar v')+  toVar (G.L1 (G.M1 (G.M1 (G.K1 a)))) = IsJust (Label @name) a+  toVar (G.R1 g) = unsafeInjectFront $ toVar g++{--------------------------------------------------------------------+  Native data type compatibility+--------------------------------------------------------------------}++-- $native+-- The 'toNative' and 'fromNative' functions allow one to convert between+-- 'Var's and regular Haskell data types ("native" types) that have the same+-- number of constructors such that each constructor has one field and the same+-- name as one of the options of the 'Var', which has the same type as that field.+-- That said, they do not compose to form the identity because 'fromNative' allows+-- constructors to be added: a variant with excess options can still be transformed+-- to a native type, but when the native type is converted to a variant, the+-- options are exactly transformed.  The only requirement is that+-- the native Haskell data type be an instance of 'Generic'.+--+-- For example, consider the following simple data type:+--+-- >>> data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)+--+-- Then, we have the following:+--+-- >>> toNative $ IsJust (Label @"Dog") 3 :: Pet+-- Dog {age = 3}+-- >>> V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int)+-- {Dog=3}+--+-- The 'fromNativeExact' function is a more restricted version of 'fromNative' that+-- does not allow options to be added; in other words, the options in the variant+-- must exactly match the constructors in the data type.  Because of this,+-- 'fromNativeExact' and 'toNative' compose to form the identity function.+++-- | Conversion helper to bring a variant back into a Haskell type. Note that the+-- native Haskell type must be an instance of 'Generic'.+class ToNative a ρ where+  toNative' :: Var ρ -> a x++instance ToNative cs ρ => ToNative (G.D1 m cs) ρ where+  toNative' = G.M1 . toNative'++instance ToNative G.V1 Empty where+  toNative' = impossible++instance (KnownSymbol name, ρ ≈ name .== t)+    => ToNative (G.C1 ('G.MetaCons name fixity sels)+                (G.S1 m (G.Rec0 t))) ρ where+  toNative' = G.M1 . G.M1 . G.K1 . snd . unSingleton++instance ( ToNative l ρ₁, ToNative r ρ₂, ρ₂ ≈ ρ .\\ ρ₁, ρ ≈ ρ₁ .+ ρ₂+         , AllUniqueLabels ρ₁, Forall ρ₂ Unconstrained1)+    => ToNative (l G.:+: r) ρ where+  toNative' v = case multiTrial @ρ₁ @ρ v of+    Left  v' -> G.L1 $ toNative' @_ @ρ₁ v'+    Right v' -> G.R1 $ toNative' @_ @ρ₂ v'++-- | Convert a variant to a native Haskell type.+toNative :: forall t ρ. (G.Generic t, ToNative (G.Rep t) ρ) => Var ρ -> t+toNative = G.to . toNative'++-- | Conversion helper to turn a Haskell variant into a row-types extensible+-- variant. Note that the native Haskell type must be an instance of 'Generic'.+class FromNative a ρ where+  fromNative' :: a x -> Var ρ++instance FromNative cs ρ => FromNative (G.D1 m cs) ρ where+  fromNative' (G.M1 v) = fromNative' v++instance FromNative G.V1 ρ where+  fromNative' = \ case++instance (KnownSymbol name, ρ .! name ≈ t, AllUniqueLabels ρ)+    => FromNative (G.C1 ('G.MetaCons name fixity sels)+                  (G.S1 m (G.Rec0 t))) ρ where+  fromNative' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x++instance (FromNative l ρ, FromNative r ρ)+    => FromNative (l G.:+: r) ρ where+  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it+  -- makes the constraints really hairy.+  fromNative' (G.L1 x) = unsafeCoerce $ fromNative' @l @ρ x+  fromNative' (G.R1 y) = unsafeCoerce $ fromNative' @r @ρ y++-- | Convert a Haskell record to a row-types Var.+fromNative :: forall t ρ. (G.Generic t, FromNative (G.Rep t) ρ) => t -> Var ρ+fromNative = fromNative' . G.from++-- | Conversion helper to turn a Haskell variant into a row-types extensible+-- variant. Note that the native Haskell type must be an instance of 'Generic'.+class FromNativeExact a ρ where+  fromNativeExact' :: a x -> Var ρ++instance FromNativeExact cs ρ => FromNativeExact (G.D1 m cs) ρ where+  fromNativeExact' (G.M1 v) = fromNativeExact' v++instance FromNativeExact G.V1 Empty where+  fromNativeExact' = \ case++instance (KnownSymbol name, ρ ≈ name .== t)+    => FromNativeExact (G.C1 ('G.MetaCons name fixity sels)+                       (G.S1 m (G.Rec0 t))) ρ where+  fromNativeExact' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x++instance (FromNativeExact l ρ₁, FromNativeExact r ρ₂, ρ ≈ ρ₁ .+ ρ₂)+    => FromNativeExact (l G.:+: r) ρ where+  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it+  -- makes the constraints really hairy.+  fromNativeExact' (G.L1 x) = unsafeCoerce $ fromNativeExact' @l @ρ₁ x+  fromNativeExact' (G.R1 y) = unsafeCoerce $ fromNativeExact' @r @ρ₂ y++-- | Convert a Haskell record to a row-types Var.+fromNativeExact :: forall t ρ. (G.Generic t, FromNativeExact (G.Rep t) ρ) => t -> Var ρ+fromNativeExact = fromNativeExact' . G.from+++{--------------------------------------------------------------------+  Generic-lens compatibility+--------------------------------------------------------------------}++-- | Every possibility of a row-types based variant has an 'AsConstructor' instance.+instance {-# OVERLAPPING #-}+  ( AllUniqueLabels r+  , AllUniqueLabels r'+  , KnownSymbol name+  , r  .! name ≈ a+  , r' .! name ≈ b+  , r' ≈ (r .- name) .\/ (name .== b))+  => AsConstructor name (Var r) (Var r') a b where+  _Ctor = focus (Label @name)+  {-# INLINE _Ctor #-}++instance {-# OVERLAPPING #-}+  ( AllUniqueLabels r+  , KnownSymbol name+  , r  .! name ≈ a+  , r ≈ (r .- name) .\/ (name .== a))+  => AsConstructor' name (Var r) a where+  _Ctor' = focus (Label @name)+  {-# INLINE _Ctor' #-}

@@ -1,10 +1,16 @@ Row-Types ======= +[![Build Status](https://api.travis-ci.org/target/row-types.svg?branch=master)](https://travis-ci.org/target/row-types/branches)+[![Hackage](https://img.shields.io/hackage/v/row-types.svg)](https://hackage.haskell.org/package/row-types)+ Row-types is a library of open records and variants for Haskell using closed type families and type literals (among other things...). See [examples/Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/examples/Examples.lhs) for an overview of how this library can be used.++Available on [Hackage](https://hackage.haskell.org/package/row-types)+  This work is a branch from CTRex [1,2] with other inspiration from data-diverse [3]. My thanks to the authors and contributors of those libraries!

@@ -6,28 +6,90 @@  import Data.Row.Records -type FiveRecord a = "a" .== a .+ "b" .== a .+ "c" .== a .+ "d" .== a .+ "e" .== a+type FourRecord a =+     "i0" .== a   .+ "i1" .== a   .+ "i2" .== a   .+ "i3"   .== a +type ElevenRecord a =+     "i0"  .== a  .+ "i1"  .== a  .+ "i2"  .== a  .+ "i3"   .== a+  .+ "i10" .== a  .+ "i11" .== a  .+ "i12" .== a  .+ "i13"  .== a+  .+ "i20" .== a  .+ "i21" .== a  .+ "i22" .== a++type SixteenRecord a =+     "i0"  .== a  .+ "i1"  .== a  .+ "i2"  .== a  .+ "i3"   .== a+  .+ "i10" .== a  .+ "i11" .== a  .+ "i12" .== a  .+ "i13"  .== a+  .+ "i20" .== a  .+ "i21" .== a  .+ "i22" .== a  .+ "i23"  .== a+  .+ "i30" .== a  .+ "i31" .== a  .+ "i32" .== a  .+ "i33"  .== a++type SixtyFourRecord a =+     "i0"   .== a .+ "i1"   .== a .+ "i2"   .== a .+ "i3"   .== a+  .+ "i10"  .== a .+ "i11"  .== a .+ "i12"  .== a .+ "i13"  .== a+  .+ "i20"  .== a .+ "i21"  .== a .+ "i22"  .== a .+ "i23"  .== a+  .+ "i30"  .== a .+ "i31"  .== a .+ "i32"  .== a .+ "i33"  .== a+  .+ "i100" .== a .+ "i101" .== a .+ "i102" .== a .+ "i103" .== a+  .+ "i110" .== a .+ "i111" .== a .+ "i112" .== a .+ "i113" .== a+  .+ "i120" .== a .+ "i121" .== a .+ "i122" .== a .+ "i123" .== a+  .+ "i130" .== a .+ "i131" .== a .+ "i132" .== a .+ "i133" .== a+  .+ "i200" .== a .+ "i201" .== a .+ "i202" .== a .+ "i203" .== a+  .+ "i210" .== a .+ "i211" .== a .+ "i212" .== a .+ "i213" .== a+  .+ "i220" .== a .+ "i221" .== a .+ "i222" .== a .+ "i223" .== a+  .+ "i230" .== a .+ "i231" .== a .+ "i232" .== a .+ "i233" .== a+  .+ "i300" .== a .+ "i301" .== a .+ "i302" .== a .+ "i303" .== a+  .+ "i310" .== a .+ "i311" .== a .+ "i312" .== a .+ "i313" .== a+  .+ "i320" .== a .+ "i321" .== a .+ "i322" .== a .+ "i323" .== a+  .+ "i330" .== a .+ "i331" .== a .+ "i332" .== a .+ "i333" .== a++my64Record :: Rec (SixtyFourRecord Double)+my64Record =+     #i0   .== 0 .+ #i1   .== 0 .+ #i2   .== 0 .+ #i3   .== 0+  .+ #i10  .== 0 .+ #i11  .== 0 .+ #i12  .== 0 .+ #i13  .== 0+  .+ #i20  .== 0 .+ #i21  .== 0 .+ #i22  .== 0 .+ #i23  .== 0+  .+ #i30  .== 0 .+ #i31  .== 0 .+ #i32  .== 0 .+ #i33  .== 0+  .+ #i100 .== 0 .+ #i101 .== 0 .+ #i102 .== 0 .+ #i103 .== 0+  .+ #i110 .== 0 .+ #i111 .== 0 .+ #i112 .== 0 .+ #i113 .== 0+  .+ #i120 .== 0 .+ #i121 .== 0 .+ #i122 .== 0 .+ #i123 .== 0+  .+ #i130 .== 0 .+ #i131 .== 0 .+ #i132 .== 0 .+ #i133 .== 0+  .+ #i200 .== 0 .+ #i201 .== 0 .+ #i202 .== 0 .+ #i203 .== 0+  .+ #i210 .== 0 .+ #i211 .== 0 .+ #i212 .== 0 .+ #i213 .== 0+  .+ #i220 .== 0 .+ #i221 .== 0 .+ #i222 .== 0 .+ #i223 .== 0+  .+ #i230 .== 0 .+ #i231 .== 0 .+ #i232 .== 0 .+ #i233 .== 0+  .+ #i300 .== 0 .+ #i301 .== 0 .+ #i302 .== 0 .+ #i303 .== 0+  .+ #i310 .== 0 .+ #i311 .== 0 .+ #i312 .== 0 .+ #i313 .== 0+  .+ #i320 .== 0 .+ #i321 .== 0 .+ #i322 .== 0 .+ #i323 .== 0+  .+ #i330 .== 0 .+ #i331 .== 0 .+ #i332 .== 0 .+ #i333 .== 0+ main :: IO () main =   defaultMain     [ bgroup "Record Construction"         [ bench "simple 1"  $ nf (#a .==) ()-        , bench "simple 5"  $ nf id $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== ()-        , bench "simple 10" $ nf id $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== ()-                                   .+ #f .== () .+ #g .== () .+ #h .== () .+ #i .== () .+ #j .== ()-        , bench "reverse 5" $ nf id $ #e .== () .+ #d .== () .+ #c .== () .+ #b .== () .+ #a .== ()-        , bench "append 3 3" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== (),   #d .== () .+ #e .== () .+ #f .== ())+        , bench "simple 4"  $ nf id $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()+        , bench "reverse 4" $ nf id $ #d .== () .+ #c .== () .+ #b .== () .+ #a .== ()+        , bench "default 4" $ nf id $ default' @Num @(FourRecord Double) 0+        , bench "recordFromLabels 4" $ nf id $ fromLabels @IsString @(FourRecord String) (fromString . show)+        , bench "default 11" $ nf id $ default' @Num @(ElevenRecord Double) 0+        , bench "recordFromLabels 11" $ nf id $ fromLabels @IsString @(ElevenRecord String) (fromString . show)+        , bench "default 16" $ nf id $ default' @Num @(SixteenRecord Double) 0+        , bench "recordFromLabels 16" $ nf id $ fromLabels @IsString @(SixteenRecord String) (fromString . show)+        , bench "simple 64" $ nf id $ my64Record+        , bench "default 64" $ nf id $ default' @Num @(SixtyFourRecord Double) 0+        , bench "recordFromLabels 64" $ nf id $ fromLabels @IsString @(SixtyFourRecord String) (fromString . show)+        ]+    , bgroup "Record Append"+        [ bench "append 3 3" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== (),   #d .== () .+ #e .== () .+ #f .== ())         , bench "append 5 1" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== (),   #f .== ())         , bench "append 1 5" $ nf (uncurry (.+)) (#a .== (),   #b .== () .+ #c .== () .+ #d .== () .+ #e .== () .+ #f .== ())-        , bench "default 5" $ nf id $ default' @Num @(FiveRecord Double) 0-        , bench "recordFromLabels 5" $ nf id $ fromLabels @IsString @(FiveRecord String) (fromString . show)         ]     , bgroup "Record Access"-        [ bench "get 1 of 5" $ nf (.! #a) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== ()-        , bench "get 5 of 5" $ nf (.! #e) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== ()+        [ bench "get 2 of 4" $ nf (.! #i1)     $ default' @Num @(FourRecord Double) 0+        [ bench "get 7 of 11" $ nf (.! #i1)    $ default' @Num @(ElevenRecord Double) 0+        , bench "get 4 of 16" $ nf (.! #i10)   $ default' @Num @(SixteenRecord Double) 0+        , bench "get 16 of 16" $ nf (.! #i33)  $ default' @Num @(SixteenRecord Double) 0+        , bench "get 4 of 64" $ nf (.! #i10)   $ default' @Num @(SixtyFourRecord Double) 1+        , bench "get 45 of 64" $ nf (.! #i230) $ default' @Num @(SixtyFourRecord Double) 2+        , bench "get 63 of 64" $ nf (.! #i332) $ default' @Num @(SixtyFourRecord Double) 3         ]     , bgroup "Record Metamorphosis"-        [ bench "erase" $ nf (erase @Show show) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== ()+        [ bench "erase 4"  $ nf (erase @Show show) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()+        , bench "erase 64" $ nf (erase @Show show) $ my64Record         ]     ]

@@ -1,4 +1,6 @@ > {-# LANGUAGE OverloadedLabels #-}+> {-# LANGUAGE DeriveGeneric #-}+> {-# LANGUAGE PartialTypeSignatures #-} > module Examples where > > import Data.Row@@ -33,9 +35,9 @@ --------------------------------------------------------------------------------  Records and variants play nicely with the lens library if we additionally import-Data.Row.Lens from the row-types-lens "orphan instance" library.  Each overloaded-label is also a Lens for a record and a Traversal for variants.  Thus, .! can be-replaced with ^. and trial can be made infix with ^?.  Additionally, update+Data.Generics.Labels from the generic-lens library.  Each overloaded+label is also a Lens for a record and a prism for variants.  Thus, .! can be+replaced with ^. and trial' can be made infix with ^?.  Additionally, update can be made infix:  update #x v r === r & #x .~ v@@ -43,11 +45,20 @@ And because of the power of lens, it's easy to make modifications rather than just update: -update #x (f $ r .! #x) r === r & #x %~ f+update #x (f (r .! #x)) r === r & #x %~ f  Lens is not included with row-types by default, but using it can make row-types-much friendlier.+much friendlier.  For this example module, we'll include a couple of handy lens+operations: +> import Data.Generics.Labels ()+> import Data.Generics.Internal.VL.Lens+>+> infixl 6 &+> (&) :: a -> (a -> b) -> b+> (&) = flip ($)+> (%~) = over+ --------------------------------------------------------------------------------   RECORDS --------------------------------------------------------------------------------@@ -145,7 +156,7 @@ Note that if we were using row-types-lens and the lens library, we could write move as: -move p dx dy = p & #x +~ dx & #y +~ dy+> moveLensy p dx dy = p & #x %~ (+ dx) & #y %~ (+ dy)  So far, we created an origin point in 2d and then one in 3d, but what if we are adventurous mathematicians who want to have points in a space with some arbitrary@@ -178,10 +189,9 @@ >       -> Rec r > get2D r = Rec.restrict r -GHC is a little finicky about the type operators and constraints -- indeed, this-type signature will fail to type check if the parentheses around-  "x" .== Double .+ "y" .== Double-in the argument are missing.  Of course, a type signature is not necessary when+GHC is a little finicky about the type operators and constraints -- indeed, some+slight modifications to the signature can easily cause type checking to fail.+However, a type signature is not necessary when using type applications, and the function can instead be written as:  > get2D' r = Rec.restrict @("x" .== Double .+ "y" .== Double) r@@ -243,8 +253,23 @@ λ> v == v3 True -Doing the above equality test does raise the question of how equality works on-variants.  For instance, v2 and v3 both look the same when you show them, and they+The diversify function makes use of the .\/ type class, pronounced min-join.+The min-join of two row-types is the minimum row-type that contains all the+bindings of the two constituent ones.  This allows use to write a function to+join two lists of variants:++> joinVarLists :: forall x y. (WellBehaved (x .\/ y), x .\/ y ≈ y .\/ x)+>              => [Var x] -> [Var y] -> [Var (x .\/ y)]+> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys++Unfortunately, GHC cannot deduce that the min-join of x and y is the same as the+min-join of y and x, so  we must add that to the constraints.  However, any concrete+types x and y that we construct will have this property, so it is easy to dispatch+when we go to use this function.++Taking a step back, it's worth looking closer at the equality tests we did earlier+on variants.  Indeed, one may ask how equality works on variants at all.+For instance, v2 and v3 both look the same when you show them, and they both have the same value inside, but can we test them for equality?  Indeed, we can't, precisely because their types are different: it is a type error to even try to check whether they're equal:@@ -291,17 +316,42 @@ If not, it provides a Right value of the variant with this label removed---since the trial failed, we now can be sure that the value is not from l. +--------------------------------------------------------------------------------+Note on lenses:+The generic-lens library distinguishes labels that are meant to be lens from labels+meant to be prisms by whether the front of the label is an underscore followed by+an uppercase letter.  This makes a lot of sense for data constructors, which is what+generic-lens's prisms were designed for, but it's a little restrictive for variants.+The result is that we can only use the lensy notation if the labels in our variants+are uppercase.  Consider the following:++> vUpper :: Var ("Y" .== String .+ "X" .== Integer)+> vUpper = IsJust (Label @"X") 1++λ> v ^? #_X+Left 1++The row-types library does not generally assert that variants need labels that+start with uppercase letters while records need labels that start with lowercase+letters---in fact, the `switch` function described below will only work if the+labels in a record and variant are exactly the same---but GHC is limited in that+the # syntax only works for lowercase labels.  Therefore, to make uppercase labels+like in the `vUpper` example above, one must use the syntax `Label @"X"` instead+of simply `#X`.  See the proposal in https://github.com/ghc-proposals/ghc-proposals/pull/170+for more information.+--------------------------------------------------------------------------------+ For ease of use in view patterns, Variants also exposes the view function. (If using lens, this can be replaced with preview.)  With it, we can write a function like this:  > myShow :: (r .! "y" ≈ String, Show (r .! "x")) => Var r -> String-> myShow (Var.view #x -> Just n) = "Int of "++show n+> myShow (Var.view #x -> Just n) = "Showable of "++show n > myShow (Var.view #y -> Just s) = "String of "++s > myShow _ = "Unknown"  λ> myShow v-"Int of 1"+"Showable of 1" λ> myShow v' "String of Foo" λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))@@ -310,22 +360,26 @@ This can also be achieved with the IsJust pattern synonym in much the same way:  > myShow' :: (WellBehaved r, r .! "y" ≈ String, Show (r .! "x")) => Var r -> String-> myShow' (IsJust (Label :: Label "x") n) = "Int of "++show n+> myShow' (IsJust (Label :: Label "x") n) = "Showable of "++show n > myShow' (IsJust (Label :: Label "y") s) = "String of "++s > myShow' _ = "Unknown"  In either case, the type signature is once again totally derivable. -There are two minor annoyances with this.  First, it's fairly common to want to define+There are three minor annoyances with this.  First, it's annoying to have to write+out the Label types in the pattern.  This is actually a requested issue on GHC+(see https://gitlab.haskell.org/ghc/ghc/issues/13116 and+https://github.com/ghc-proposals/ghc-proposals/pull/80 for more information).+Second, it's fairly common to want to define a function like myShow to be exhaustive in the variant's cases, but to do this, you must manually provide a type signature:  > myShowRestricted :: Var ("y" .== String .+ "x" .== Integer) -> String-> myShowRestricted (Var.view #x -> Just n) = "Int of "++show n+> myShowRestricted (Var.view #x -> Just n) = "Integer of "++show n > myShowRestricted (Var.view #y -> Just s) = "String of "++s > myShowRestricted _ = error "Unreachable" -The second blemish can be seen in this restricted version of myShow.  Even though+The final blemish can be seen in this restricted version of myShow.  Even though we know from the type that we've covered all the posibilities of the variant, GHC will generate a "non-exhaustive pattern match" warning without the final line. (This is true for the pattern synonym version too.)@@ -338,7 +392,7 @@  > --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String > myShowRestricted' v = switch v $->      #x .== (\n -> "Int of "++show n)+>      #x .== (\n -> "Integer of "++show n) >   .+ #y .== (\s -> "String of "++s)  This version of myShow needs neither a type signature (it is inferred exactly) nor@@ -346,7 +400,6 @@ standard pattern matching.  - A more powerful version of trial is multiTrial, which tests for multiple labels at once.  With this, you can wholesale change the type of the variant to any (valid) variant type you would like.  Of course, there needs to be a recourse if the variant@@ -371,11 +424,8 @@  Thus, multiTrial can be used not only to arbitrarily split apart a variant, but also to change unused label associations (in this case, we changed the variant-from one where "x" is an Integer to one where it's a Double).---Here are two functions you can define over variants.  The type constraints are a little-ugly (the type equalities are necessary but annoying).+from one where "x" is an Integer to one where it's a Double).  We can even use+it to combine dispatching of two different variants at once:  > also :: Disjoint xs ys >      => (Var xs -> a)@@ -385,6 +435,7 @@ >   Left  e' -> f1 e' >   Right e' -> f2 e' -> joinVarLists :: forall x y. (WellBehaved (x .\/ y), x .\/ y ≈ y .\/ x)->              => [Var x] -> [Var y] -> [Var (x .\/ y)]-> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys+The above also function takes two functions f1 and f2 that can each independently+be used on variants with rows xs and ys respectively.  Using multiTrial, we can+split the input variant (which is the join of xs and ys) and easily apply f1 or+f2 as appropriate.

@@ -1,5 +1,5 @@ Name:                row-types-Version:             0.2.3.0+Version:             0.3.0.0 License:             MIT License-file:        LICENSE Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck@@ -30,6 +30,8 @@                  deepseq >= 1.4,                  hashable >= 1.2,                  unordered-containers >= 0.2,+                 generic-lens >= 1.0.0.0,+                 profunctors >= 5.0,                  text   Exposed-modules: Data.Row                  , Data.Row.Internal@@ -40,12 +42,14 @@   Extensions: AllowAmbiguousTypes,               ConstraintKinds,               DataKinds,+              EmptyCase,               EmptyDataDecls,               FlexibleContexts,               FlexibleInstances,               GADTs,               InstanceSigs,               KindSignatures,+              LambdaCase,               MultiParamTypeClasses,               OverloadedLabels,               PatternGuards,@@ -86,6 +90,7 @@   ghc-options: -W   other-modules: Examples   build-depends: base >= 2 && < 6+               , generic-lens >= 1.1.0.0                , row-types   Extensions: AllowAmbiguousTypes,               DataKinds,