row-types 0.2.1.0 → 0.2.2.0

raw patch · 6 files changed

+86/−35 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Row.hs +1/−1
• Data/Row/Internal.hs +41/−9
• Data/Row/Records.hs +38/−19
• Data/Row/Variants.hs +2/−2
• examples/Examples.lhs +3/−3
• row-types.cabal +1/−1

@@ -41,7 +41,7 @@   -- * Variant construction   , pattern IsJust   -- ** Restriction-  , diversify+  , diversify, type (.\/)   -- ** Destruction   , impossible, trial, trial', multiTrial   , type (.\\)

@@ -20,9 +20,10 @@   -- * Row Operations   , Extend, Modify, Rename   , type (.\), type (.!), type (.-), type (.+), type (.\\), type (.==)+  , type (.\/)   , Lacks, HasType   -- * Row Classes-  , Labels, labels+  , Labels, labels, labels'   , Forall(..), Forall2(..)   , Unconstrained1   -- * Helper functions@@ -32,9 +33,12 @@   , WellBehaved, AllUniqueLabels, Zip, Map, Subset, Disjoint    , mapForall+  , freeForall   , uniqueMap   , IsA(..)   , As(..)++  , FoldStep   ) where @@ -142,6 +146,11 @@ type family (l :: Row *) .\\ (r :: Row *) :: Row * where   R l .\\ R r = R (Diff l r) +-- | The minimum join of the two rows.+type family (l :: Row *) .\/ (r :: Row *) where+  R l .\/ R r = R (MinJoinR l r)++ {--------------------------------------------------------------------   Syntactic sugar for record operations --------------------------------------------------------------------}@@ -168,9 +177,7 @@ -- | 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 (ℓ :-> τ) ρ ≈ ℓ :-> τ ': ρ-                      , R ρ .\ ℓ-                      )+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.@@ -201,16 +208,21 @@             -> f r  -- ^ The input structure             -> g r --- * Says that there exists a `t` such that `a ~ f t` and `c t`.+-- | This data type is used to for its ability to existentially bind a type+-- variable.  Particularly, it says that for the type 'a', there exists a 't'+-- such that 'a ~ f t' and 'c t' holds. data As c f a where   As :: forall c f a t. (a ~ f t, c t) => As c f a +-- | A class to capture the idea of 'As' so that it can be partially applied in+-- a context. class IsA c f a where   as :: As c f a  instance c a => IsA c f (f a) where   as = As +-- | An internal type used by the 'metamorph' in 'mapForall'. newtype MapForall c f (r :: Row *) = MapForall { unMapForall :: Dict (Forall (Map f r) (IsA c f)) }  -- | This allows us to derive a `Forall (Map f r) ..` from a `Forall r ..`.@@ -234,6 +246,10 @@ uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ) uniqueMap = Sub $ UNSAFE.unsafeCoerce @(Dict Unconstrained) Dict +-- | Allow any 'Forall` over a row-type, be usable for 'Unconstrained1'.+freeForall :: forall r c. Forall r c :- Forall r Unconstrained1+freeForall = Sub $ UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict+ instance Forall (R '[]) c where   {-# INLINE metamorph #-}   metamorph _ empty _ _ = empty@@ -316,7 +332,11 @@   where doUncons _ _ = (Const (), Const ())         doCons l _ (Const c) = Const $ show' l : c +-- | Return a list of the labels in a row type and is specialized to the 'Unconstrained1' constraint.+labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]+labels' = labels @ρ @Unconstrained1 + {--------------------------------------------------------------------   Convenient type families and classes --------------------------------------------------------------------}@@ -425,16 +445,14 @@                           :<>: ShowType r)  type family LacksR (l :: Symbol) (r :: [LT *]) (r_orig :: [LT *]) :: Constraint where-  LacksR l '[] r = Unconstrained+  LacksR l '[] _ = Unconstrained   LacksR l (l :-> t ': x) r = TypeError (TL.Text "The label " :<>: ShowType l                                     :<>: TL.Text " already exists in " :<>: ShowType r)-  LacksR l (p ': x) r = LacksR l x r+  LacksR l (l' :-> _ ': x) r = Ifte (l <=.? l') Unconstrained (LacksR l x r)  type family Merge (l :: [LT *]) (r :: [LT *]) where   Merge '[] r = r   Merge l '[] = l-  Merge (h :-> a ': tl)   (h :-> a ': tr) =-      (h :-> a ': Merge tl tr)   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 ".")@@ -442,6 +460,20 @@       Ifte (hl <=.? hr)       (hl :-> al ': Merge tl (hr :-> ar ': tr))       (hr :-> ar ': Merge (hl :-> al ': tl) tr)++type family MinJoinR (l :: [LT *]) (r :: [LT *]) where+  MinJoinR '[] r = r+  MinJoinR l '[] = l+  MinJoinR (h :-> a ': tl)   (h :-> a ': tr) =+      (h :-> a ': MinJoinR tl tr)+  MinJoinR (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 ".")+  MinJoinR (hl :-> al ': tl) (hr :-> ar ': tr) =+      Ifte (CmpSymbol hl hr == 'LT)+      (hl :-> al ': MinJoinR tl (hr :-> ar ': tr))+      (hr :-> ar ': MinJoinR (hl :-> al ': tl) tr)+  -- | Returns the left list with all of the elements from the right list removed. type family Diff (l :: [LT *]) (r :: [LT *]) where

@@ -47,12 +47,13 @@   -- ** Zip   , Zip, zip   -- ** Sequence-  , sequence+  , sequence, sequence'   -- ** Compose   -- $compose   , compose, uncompose+  , compose', uncompose'   -- ** Labels-  , labels+  , labels, labels'   -- ** UNSAFE operations   , unsafeRemove, unsafeInjectFront   )@@ -62,7 +63,7 @@  import Control.DeepSeq (NFData(..), deepseq) -import qualified Data.Constraint as Constraint+import Data.Constraint ((\\)) import Data.Functor.Compose import Data.Functor.Const import Data.Functor.Identity@@ -70,7 +71,6 @@ import Data.Hashable import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as M-import Data.List hiding (map, zip) import qualified Data.List as L import Data.Proxy import Data.String (IsString)@@ -91,7 +91,7 @@   OR :: HashMap Text HideType -> Rec r  instance Forall r Show => Show (Rec r) where-  show r = "{ " ++ intercalate ", " binds ++ " }"+  show r = "{ " ++ L.intercalate ", " binds ++ " }"     where binds = (\ (x, y) -> x ++ "=" ++ y) <$> eraseWithLabels @Show show r  instance Forall r Eq => Eq (Rec r) where@@ -292,14 +292,20 @@ transform' :: forall r f g. Forall r Unconstrained1 => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r) transform' = transform @Unconstrained1 @r --- | Applicative sequencing over a record-sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Rec (Map f r) -> f (Rec r)-sequence = getCompose . metamorph @r @Unconstrained1 @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap+-- | A version of 'sequence' in which the constraint for 'Forall' can be chosen.+sequence' :: forall f r c. (Forall r c, Applicative f)+          => Rec (Map f r) -> f (Rec r)+sequence' = getCompose . metamorph @r @c @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap   where     doNil _ = Compose (pure empty)     doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)     doCons l fv (Compose fr) = Compose $ unsafeInjectFront l <$> fv <*> fr +-- | Applicative sequencing over a record.+sequence :: forall f r. (Forall r Unconstrained1, Applicative f)+         => Rec (Map f r) -> f (Rec r)+sequence = sequence' @_ @_ @Unconstrained1+ -- $compose -- We can easily convert between mapping two functors over the types of a row -- and mapping the composition of the two functors.  The following two functions@@ -309,25 +315,38 @@ -- -- >>> uncompose . compose = id --- | Convert from a record where two functors have been mapped over the types to--- one where the composition of the two functors is mapped over the types.-compose :: forall (f :: * -> *) g r . Forall r Unconstrained1 => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)-compose = unRMap . metamorph @r @Unconstrained1 @(RMap2 f g) @(RMap (Compose f g)) Proxy doNil doUncons doCons . RMap2+-- | A version of 'compose' in which the constraint for 'Forall' can be chosen.+compose' :: forall c (f :: * -> *) g r . Forall r c+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)+compose' = unRMap . metamorph @r @c @(RMap2 f g) @(RMap (Compose f g)) @(Compose f g) Proxy doNil doUncons doCons . RMap2   where     doNil _ = RMap empty     doUncons l (RMap2 r) = (Compose $ r .! l, RMap2 $ unsafeRemove l r)     doCons l v (RMap r) = RMap $ unsafeInjectFront l v r --- | Convert from a record where the composition of two functors have been mapped--- over the types to one where the two functors are mapped individually one at a--- time over the types.-uncompose :: forall (f :: * -> *) g r . Forall r Unconstrained1 => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))-uncompose = unRMap2 . metamorph @r @Unconstrained1 @(RMap (Compose f g)) @(RMap2 f g) Proxy doNil doUncons doCons . RMap+-- | Convert from a record where two functors have been mapped over the types to+-- one where the composition of the two functors is mapped over the types.+compose :: forall (f :: * -> *) g r . Forall r Unconstrained1+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)+compose = compose' @Unconstrained1 @f @g @r++-- | A version of 'uncompose' in which the constraint for 'Forall' can be chosen.+uncompose' :: forall c (f :: * -> *) g r . Forall r c+           => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))+uncompose' = unRMap2 . metamorph @r @c @(RMap (Compose f g)) @(RMap2 f g) @(Compose f g) Proxy doNil doUncons doCons . RMap   where     doNil _ = RMap2 empty     doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)     doCons l (Compose v) (RMap2 r) = RMap2 $ unsafeInjectFront l v r +-- | Convert from a record where the composition of two functors have been mapped+-- over the types to one where the two functors are mapped individually one at a+-- time over the types.+uncompose :: forall (f :: * -> *) g r . Forall r Unconstrained1+          => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))+uncompose = uncompose' @Unconstrained1 @f @g @r++ -- | RZipPair is used internally as a type level lambda for zipping records. newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { unRZipPair :: Rec (Zip ρ1 ρ2) } @@ -381,7 +400,7 @@ fromLabelsMapA :: forall c f g ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)                => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Rec (Map g ρ)) fromLabelsMapA f = fromLabelsA @(IsA c g) @f @(Map g ρ) inner-                Constraint.\\ mapForall @g @c @ρ-                Constraint.\\ uniqueMap @g @ρ+                \\ mapForall @g @c @ρ+                \\ uniqueMap @g @ρ    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

@@ -17,7 +17,7 @@   , HasType, pattern IsJust, singleton   , fromLabels   -- ** Extension-  , type (.\), Lacks, diversify, type (.+)+  , type (.\), Lacks, type (.\/), diversify, type (.+)   -- ** Modification   , update, focus, Modify, rename, Rename   -- * Destruction@@ -122,7 +122,7 @@ unSingleton v = (l, view l v) where l = Label @l  -- | Make the variant arbitrarily more diverse.-diversify :: forall r' r. AllUniqueLabels (r .+ r') => Var r -> Var (r .+ r')+diversify :: forall r' r. Var r -> Var (r .\/ r') diversify = unsafeCoerce -- (OneOf l x) = OneOf l x  -- | If the variant exists at the given label, update it to the given value.

@@ -94,7 +94,7 @@ In fact, we can do this generally.  The following function takes a name and a record and adds the "name" field to that record with the given name. -> named :: r .\ "name" => a -> Rec r -> Rec ("name" .== a .+ r)+> named :: a -> Rec r -> Rec ("name" .== a .+ r) > named s r = #name .== s .+ r  Note that we require that the record we are naming must not have a "name" field@@ -385,6 +385,6 @@ >   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 :: 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

@@ -1,5 +1,5 @@ Name:                row-types-Version:             0.2.1.0+Version:             0.2.2.0 License:             MIT License-file:        LICENSE Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck