row-types 0.2.0.0 → 0.2.1.0

raw patch · 10 files changed

+491/−399 lines, 10 filesdep +constraintsdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: constraints

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• Data/Row.hs +0/−1
• Data/Row/Internal.hs +41/−1
• Data/Row/Records.hs +11/−2
• Data/Row/Variants.hs +11/−1
• Examples.lhs +0/−390
• README.md +1/−1
• examples/Examples.lhs +390/−0
• row-types.cabal +24/−3
• tests/Main.hs +6/−0

@@ -1,3 +1,10 @@ +## 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'.+- Added very simple test suite.+ ## 0.2.0.0 [2018-02-12] - Initial Release

@@ -34,7 +34,6 @@   , type (.==), (.==), pattern (:==), unSingleton   -- ** Restriction   , type (.-), (.-)-  , restrict   -- ** Query   , type (.!), (.!)   -- ** Disjoint union

@@ -30,9 +30,15 @@   , toKey   , type (≈)   , WellBehaved, AllUniqueLabels, Zip, Map, Subset, Disjoint++  , mapForall+  , uniqueMap+  , IsA(..)+  , As(..)   ) where +import Data.Constraint import Data.Functor.Const import Data.Proxy import Data.String (IsString (fromString))@@ -40,7 +46,8 @@ import qualified Data.Text as Text import Data.Type.Equality (type (==)) -import GHC.Exts -- needed for constraints kinds+import qualified Unsafe.Coerce as UNSAFE+ import GHC.OverloadedLabels import GHC.TypeLits import qualified GHC.TypeLits as TL@@ -193,6 +200,39 @@                -- ^ The fold             -> f r  -- ^ The input structure             -> g r++-- * Says that there exists a `t` such that `a ~ f t` and `c t`.+data As c f a where+  As :: forall c f a t. (a ~ f t, c t) => As c f a++class IsA c f a where+  as :: As c f a++instance c a => IsA c f (f a) where+  as = As++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 ..`.+mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f)+mapForall = Sub $ unMapForall $ metamorph @ρ @c @(Const ()) @(MapForall c f) @(Const ()) Proxy empty uncons cons $ Const ()+  where empty :: Const () Empty -> MapForall c f Empty+        empty _ = MapForall Dict++        uncons :: forall l t r. (KnownSymbol l, c t)+               => Label l -> Const () ('R (l :-> t ': r)) -> (Const () t, Const () ('R r))+        uncons _ _ = (Const (), Const ())++        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ)+             => 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++-- | Map preserves uniqueness of labels.+uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)+uniqueMap = Sub $ UNSAFE.unsafeCoerce @(Dict Unconstrained) Dict  instance Forall (R '[]) c where   {-# INLINE metamorph #-}

@@ -25,7 +25,7 @@   , empty   , type (.==), (.==), pattern (:==), unSingleton   , default', defaultA-  , fromLabels, fromLabelsA+  , fromLabels, fromLabelsA, fromLabelsMapA   -- ** Extension   , extend, Extend, Lacks, type (.\)   -- ** Restriction@@ -62,6 +62,7 @@  import Control.DeepSeq (NFData(..), deepseq) +import qualified Data.Constraint as Constraint import Data.Functor.Compose import Data.Functor.Const import Data.Functor.Identity@@ -145,7 +146,7 @@ extend (toKey -> l) a (OR m) = OR $ M.insert l (HideType a) m  -- | Update the value associated with the label.-update :: KnownSymbol l => Label l -> a -> Rec r -> Rec r+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Rec r -> Rec r 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.@@ -376,3 +377,11 @@                => Label ℓ -> Const () τ -> Compose f Rec ('R ρ) -> Compose f Rec ('R (ℓ :-> τ ': ρ))         doCons l _ (Compose r) = Compose $ unsafeInjectFront l <$> mk l <*> r +-- | Initialize a record that is produced by a `Map`.+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 @ρ+   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

@@ -22,6 +22,7 @@   , update, focus, Modify, rename, Rename   -- * Destruction   , impossible, trial, trial', multiTrial, view+  , restrict, split   -- ** Types for destruction   , type (.!), type (.-), type (.\\), type (.==)   -- * Row operations@@ -126,7 +127,7 @@  -- | If the variant exists at the given label, update it to the given value. -- Otherwise, do nothing.-update :: KnownSymbol l => Label l -> a -> Var r -> Var r+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Var r -> Var r update (toKey -> l') a (OneOf l x) = OneOf l $ if l == l' then HideType a else x  -- | If the variant exists at the given label, focus on the value associated with it.@@ -160,6 +161,15 @@ -- myShow (view y -> Just s) = "String of "++s @ view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l) view = flip trial'++-- | Split a variant into two sub-variants.+split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var s) (Var (r .\\ s))+split (OneOf l a) | l `elem` labels @s @Unconstrained1 = Left  $ OneOf l a+                  | otherwise                          = Right $ OneOf l a++-- | Arbitrary variant restriction.  Turn a variant into a subset of itself.+restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)+restrict = either Just (pure Nothing) . split   {--------------------------------------------------------------------

@@ -1,390 +0,0 @@-> {-# LANGUAGE OverloadedLabels #-}-> module Examples where->-> import Data.Row-> import qualified Data.Row.Records as Rec-> import qualified Data.Row.Variants as Var--In this example file, we will explore how to create and use records and variants.-----------------------------------------------------------------------------------  LABELS-----------------------------------------------------------------------------------To begin, we will briefly discuss creating labels -- their use will follow.--The most basic way to create a label is through construction with a type signature:-- x = Label :: Label "x"--With the above definition, x is a label for the field x.  Using type applications,-this can be shortened to:-- x = Label @"x"--And with OverloadedLabels, one can just write:-- #x--We will use the OverloadedLabels notation in these examples.-----------------------------------------------------------------------------------  LENS-----------------------------------------------------------------------------------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-can be made infix:--update #x v r === r & #x .~ v--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--Lens is not included with row-types by default, but using it can make row-types-much friendlier.-----------------------------------------------------------------------------------  RECORDS-----------------------------------------------------------------------------------With some labels defined, let's begin with records.  To start, let's create a-record representing the Cartesian coordinates of the origin.  To do this,-we use the .== operator to initialize values in a record, and we separate each-initialized value with the .+ operator.Notice that the value level code uses the-same operators as the type level code.--> origin :: Rec ("x" .== Double .+ "y" .== Double )-> origin = #x .== 0 .+ #y .== 0--Note that, although we wrote the type explicitly, GHC has no problem inferring-it exactly.--If we show this at the repl, we see:-λ> origin-{ x=0.0, y=0.0 }--Of course, as an extensible record, the order that we build it shouldn't matter,-and indeed, it doesn't.  Consider the following variation:--> origin' :: Rec ("y" .== Double .+ "x" .== Double)-> origin' = #y .== 0 .+ #x .== 0--If we show this at the repl, we see:--λ> origin2-{ x=0.0, y=0.0 }--Indeed, the two values are indistinguishable:--λ> origin == origin'-True--Now, let's expand upon our record.  Why stop at two dimensions when we can make-a record in three dimensions.--> origin3D = #z .== 0.0 .+ origin--Once again, the type is inferred for us, and the record is exactly as expected.--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 s r = #name .== s .+ r--Note that we require that the record we are naming must not have a "name" field-already.  Overlapping labels within a single record/variant is strictly forbidden.--Let's say we want to get the values out of the record.  Simple selection is achieved-with the .! operator, like so:--λ> origin .! #x-0.0--and we can use this to write whatever we want.  Here is a function for calculating-Euclidean distance from the origin to a point:--> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t-> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y--Once again, the type of distance is entirely inferrable, but we write it here for-convenience.  This works exactly as expected:--λ> distance origin-0.0-λ> distance origin3D-0.0-λ> distance (named "2D" origin)-0.0--Of course, that wasn't very interesting when our only points are at the origin-already.  We could make new records representing new points, but instead, let's-write a function to move the points we have:--> move :: (Num (r .! "x"), Num (r .! "y"))->      => Rec r -> r .! "x" -> r .! "y" -> Rec r-> move p dx dy = Rec.update #x (p .! #x + dx) $->                Rec.update #y (p .! #y + dy) p--Here, we're using the Rec.update operator to update the value at the label x by-adding dx to it, and then we do the same for y.-We can see it work in practice:--λ> move origin 3 4-{ x=3.0, y=4.0 }-λ> distance (move origin 3 4)-5.0-λ> distance (move (named "2D" origin3D) 5 12)-13.0--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--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-number of dimensions.  We could write out each of the 0s necessary, but there's-an easier way to initialize a record:--> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)-> origin4 = Rec.default' @Num 0--Finally, we have come to a case where GHC cannot infer the type signature, and how-could it!  The type is providing crucial information about the shape of the record.-Regardless, with the type provided, it works exactly as expected:--λ> origin4-{ w=0.0, x=0.0, y=0.0, z=0.0 }--While we have added names or further fields, we can also choose to forget-information in a record.  To remove a particular label, one can use the .--operator, like so:--> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")-> unName r = r .- #name--For larger changes, it is easier to use the restrict function.  The following-function will take a record that contains both an x and y coordinate and remove-the rest of the fields from it.--> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)->       => Rec (r .+ rest)->       -> Rec r-> get2D r = 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-using type applications, and the function can instead be written as:--> get2D' r = restrict @("x" .== Double .+ "y" .== Double) r--with no trouble.  Yet another altnerative is to match directly on the values desired-using the :== and :+ record patterns:--> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)->         => Rec (r .+ rest)->         -> Rec r-> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)->           = #x .== n1 .+ #y .== n2--(Note that overloaded labels cannot be used in the patterns, so the notation is-unfortunately bloated by types.  Also, the type operators are left associated,-so the "_" must go on the right, and the type signature is unforunately necessary.)--All three of the get2D functions behave the same.-----------------------------------------------------------------------------------  VARIANTS----------------------------------------------------------------------------------Let's move on from records to variants.  In many ways, variants are quite similar,-as might be expected given that variants are dual to records.  The types look-almost the same, and some of the operators are shared as well.  However,-construction and destruction are obviously different.--Creating a variant can be done with IsJust:--> v,v' :: Var ("y" .== String .+ "x" .== Integer)-> v  = IsJust #x 1-> v' = IsJust #y "Foo"--Here, the type is necessary to specify what concrete type the variant is (when-using AllowAmbiguousTypes, the type is not always needed, but it would be needed-to e.g. show the variant).  In the simple case of a variant of just one type,-the simpler singleton function can be used:--> v2 = Var.singleton #x 1--Now, the type can be easily derived by GHC.  We can show variants as easily as-records:--λ> v-{x=1}-λ> v'-{y="Foo"}-λ> v2-{x=1}--Once created, a variant can be expanded by using type applications and the-diversify function.--> v3 = diversify @("y" .== String) v2-> v4 = diversify @("y" .== String .+ "z" .== Double) v2--λ> :t v4-v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])-λ> 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-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:--λ> v2 == v3-error:-    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’-      Expected type: Var ('R '["x" ':-> Integer])-        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))-    • In the second argument of ‘(==)’, namely ‘v3’-      In the expression: v2 == v3-      In an equation for ‘it’: it = v2 == v3--This may look a little scary, but it's actually a pretty useful message.  Essentially,-it's expecting a variant that can only be an Integer at label "x", but it found one-that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,-but since v3 now has the same labels as v1, that comparison is fine:--λ> v == v3-True-λ> v == IsJust #x 3-False-λ> v == v'-False-λ> v == IsJust #y "fail"-False--(Also note here that using IsJust without a type signature is fine because the correct-type can be easily inferred due to v's type.)--What can you do with a variant?  The only way to really use one is to get the value-out, and to do that, you must trial it:--λ> trial v #x-Left 1-λ> trial v #y-Right {x=1}-λ> trial v' #x-Right {y="Foo"}-λ> trial v' #y-Left "Foo"--If trialing at a label l succeeds, then it provides a Left value of the value at l.-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.--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 #y -> Just s) = "String of "++s-> myShow _ = "Unknown"--λ> myShow v-"Int of 1"-λ> myShow v'-"String of Foo"-λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))-"Unknown"--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 "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-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 #y -> Just s) = "String of "++s-> myShowRestricted _ = error "Unreachable"--The second 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.)--One way to avoid this problem is to use switch.  The switch operator takes a variant-and a record such that for each label that the variant has, the record has a function-at that label that consumes the value the variant has and produces a value in a-common type.  Essentially, switch "applies" the variant to the record to produce-an output value.--> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String-> myShowRestricted' v = switch v $->      #x .== (\n -> "Int of "++show n)->   .+ #y .== (\s -> "String of "++s)--This version of myShow needs neither a type signature (it is inferred exactly) nor-a default "unreachable" case.  However, we no longer have the benefit of Haskell's-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-you provide is not expressible in the type you want, so multiTrial returns an Either-of the type you want or a Variant of the leftovers.  Consider the examples:--λ> :t multiTrial @("x" .== Double .+ "y" .== String) v-multiTrial @("x" .== Double .+ "y" .== String) v-  :: Either-       (Var ('R '["x" ':-> Double, "y" ':-> String]))-       (Var ('R '["x" ':-> Integer]))-λ> multiTrial @("x" .== Double .+ "y" .== String) v-Right {x=1}--λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'-multiTrial @("x" .== Double .+ "y" .== String) v'-  :: Either-       (Var ('R '["x" ':-> Double, "y" ':-> String]))-       (Var ('R '["x" ':-> Integer]))-λ> multiTrial @("x" .== Double .+ "y" .== String) v'-Left {y="Foo"}--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).--> also :: Disjoint xs ys->      => (Var xs -> a)->      -> (Var ys -> a)->      -> Var (xs .+ ys) -> a-> also f1 f2 e = case multiTrial e of->   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

@@ -3,7 +3,7 @@  Row-types is a library of open records and variants for Haskell using closed type families and type literals (among other things...).-See [Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/Examples.lhs)+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.  This work is a branch from CTRex [1,2] with other inspiration from data-diverse [3].

@@ -0,0 +1,390 @@+> {-# LANGUAGE OverloadedLabels #-}+> module Examples where+>+> import Data.Row+> import qualified Data.Row.Records as Rec+> import qualified Data.Row.Variants as Var++In this example file, we will explore how to create and use records and variants.++--------------------------------------------------------------------------------+  LABELS+--------------------------------------------------------------------------------++To begin, we will briefly discuss creating labels -- their use will follow.++The most basic way to create a label is through construction with a type signature:++ x = Label :: Label "x"++With the above definition, x is a label for the field x.  Using type applications,+this can be shortened to:++ x = Label @"x"++And with OverloadedLabels, one can just write:++ #x++We will use the OverloadedLabels notation in these examples.++--------------------------------------------------------------------------------+  LENS+--------------------------------------------------------------------------------++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+can be made infix:++update #x v r === r & #x .~ v++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++Lens is not included with row-types by default, but using it can make row-types+much friendlier.++--------------------------------------------------------------------------------+  RECORDS+--------------------------------------------------------------------------------++With some labels defined, let's begin with records.  To start, let's create a+record representing the Cartesian coordinates of the origin.  To do this,+we use the .== operator to initialize values in a record, and we separate each+initialized value with the .+ operator.Notice that the value level code uses the+same operators as the type level code.++> origin :: Rec ("x" .== Double .+ "y" .== Double )+> origin = #x .== 0 .+ #y .== 0++Note that, although we wrote the type explicitly, GHC has no problem inferring+it exactly.++If we show this at the repl, we see:+λ> origin+{ x=0.0, y=0.0 }++Of course, as an extensible record, the order that we build it shouldn't matter,+and indeed, it doesn't.  Consider the following variation:++> origin' :: Rec ("y" .== Double .+ "x" .== Double)+> origin' = #y .== 0 .+ #x .== 0++If we show this at the repl, we see:++λ> origin2+{ x=0.0, y=0.0 }++Indeed, the two values are indistinguishable:++λ> origin == origin'+True++Now, let's expand upon our record.  Why stop at two dimensions when we can make+a record in three dimensions.++> origin3D = #z .== 0.0 .+ origin++Once again, the type is inferred for us, and the record is exactly as expected.++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 s r = #name .== s .+ r++Note that we require that the record we are naming must not have a "name" field+already.  Overlapping labels within a single record/variant is strictly forbidden.++Let's say we want to get the values out of the record.  Simple selection is achieved+with the .! operator, like so:++λ> origin .! #x+0.0++and we can use this to write whatever we want.  Here is a function for calculating+Euclidean distance from the origin to a point:++> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t+> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y++Once again, the type of distance is entirely inferrable, but we write it here for+convenience.  This works exactly as expected:++λ> distance origin+0.0+λ> distance origin3D+0.0+λ> distance (named "2D" origin)+0.0++Of course, that wasn't very interesting when our only points are at the origin+already.  We could make new records representing new points, but instead, let's+write a function to move the points we have:++> move :: (Num (r .! "x"), Num (r .! "y"))+>      => Rec r -> r .! "x" -> r .! "y" -> Rec r+> move p dx dy = Rec.update #x (p .! #x + dx) $+>                Rec.update #y (p .! #y + dy) p++Here, we're using the Rec.update operator to update the value at the label x by+adding dx to it, and then we do the same for y.+We can see it work in practice:++λ> move origin 3 4+{ x=3.0, y=4.0 }+λ> distance (move origin 3 4)+5.0+λ> distance (move (named "2D" origin3D) 5 12)+13.0++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++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+number of dimensions.  We could write out each of the 0s necessary, but there's+an easier way to initialize a record:++> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)+> origin4 = Rec.default' @Num 0++Finally, we have come to a case where GHC cannot infer the type signature, and how+could it!  The type is providing crucial information about the shape of the record.+Regardless, with the type provided, it works exactly as expected:++λ> origin4+{ w=0.0, x=0.0, y=0.0, z=0.0 }++While we have added names or further fields, we can also choose to forget+information in a record.  To remove a particular label, one can use the .-+operator, like so:++> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")+> unName r = r .- #name++For larger changes, it is easier to use the restrict function.  The following+function will take a record that contains both an x and y coordinate and remove+the rest of the fields from it.++> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)+>       => Rec (r .+ rest)+>       -> 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+using type applications, and the function can instead be written as:++> get2D' r = Rec.restrict @("x" .== Double .+ "y" .== Double) r++with no trouble.  Yet another altnerative is to match directly on the values desired+using the :== and :+ record patterns:++> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)+>         => Rec (r .+ rest)+>         -> Rec r+> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)+>           = #x .== n1 .+ #y .== n2++(Note that overloaded labels cannot be used in the patterns, so the notation is+unfortunately bloated by types.  Also, the type operators are left associated,+so the "_" must go on the right, and the type signature is unforunately necessary.)++All three of the get2D functions behave the same.++--------------------------------------------------------------------------------+  VARIANTS+--------------------------------------------------------------------------------+Let's move on from records to variants.  In many ways, variants are quite similar,+as might be expected given that variants are dual to records.  The types look+almost the same, and some of the operators are shared as well.  However,+construction and destruction are obviously different.++Creating a variant can be done with IsJust:++> v,v' :: Var ("y" .== String .+ "x" .== Integer)+> v  = IsJust #x 1+> v' = IsJust #y "Foo"++Here, the type is necessary to specify what concrete type the variant is (when+using AllowAmbiguousTypes, the type is not always needed, but it would be needed+to e.g. show the variant).  In the simple case of a variant of just one type,+the simpler singleton function can be used:++> v2 = Var.singleton #x 1++Now, the type can be easily derived by GHC.  We can show variants as easily as+records:++λ> v+{x=1}+λ> v'+{y="Foo"}+λ> v2+{x=1}++Once created, a variant can be expanded by using type applications and the+diversify function.++> v3 = diversify @("y" .== String) v2+> v4 = diversify @("y" .== String .+ "z" .== Double) v2++λ> :t v4+v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])+λ> 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+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:++λ> v2 == v3+error:+    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’+      Expected type: Var ('R '["x" ':-> Integer])+        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))+    • In the second argument of ‘(==)’, namely ‘v3’+      In the expression: v2 == v3+      In an equation for ‘it’: it = v2 == v3++This may look a little scary, but it's actually a pretty useful message.  Essentially,+it's expecting a variant that can only be an Integer at label "x", but it found one+that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,+but since v3 now has the same labels as v1, that comparison is fine:++λ> v == v3+True+λ> v == IsJust #x 3+False+λ> v == v'+False+λ> v == IsJust #y "fail"+False++(Also note here that using IsJust without a type signature is fine because the correct+type can be easily inferred due to v's type.)++What can you do with a variant?  The only way to really use one is to get the value+out, and to do that, you must trial it:++λ> trial v #x+Left 1+λ> trial v #y+Right {x=1}+λ> trial v' #x+Right {y="Foo"}+λ> trial v' #y+Left "Foo"++If trialing at a label l succeeds, then it provides a Left value of the value at l.+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.++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 #y -> Just s) = "String of "++s+> myShow _ = "Unknown"++λ> myShow v+"Int of 1"+λ> myShow v'+"String of Foo"+λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))+"Unknown"++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 "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+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 #y -> Just s) = "String of "++s+> myShowRestricted _ = error "Unreachable"++The second 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.)++One way to avoid this problem is to use switch.  The switch operator takes a variant+and a record such that for each label that the variant has, the record has a function+at that label that consumes the value the variant has and produces a value in a+common type.  Essentially, switch "applies" the variant to the record to produce+an output value.++> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String+> myShowRestricted' v = switch v $+>      #x .== (\n -> "Int of "++show n)+>   .+ #y .== (\s -> "String of "++s)++This version of myShow needs neither a type signature (it is inferred exactly) nor+a default "unreachable" case.  However, we no longer have the benefit of Haskell's+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+you provide is not expressible in the type you want, so multiTrial returns an Either+of the type you want or a Variant of the leftovers.  Consider the examples:++λ> :t multiTrial @("x" .== Double .+ "y" .== String) v+multiTrial @("x" .== Double .+ "y" .== String) v+  :: Either+       (Var ('R '["x" ':-> Double, "y" ':-> String]))+       (Var ('R '["x" ':-> Integer]))+λ> multiTrial @("x" .== Double .+ "y" .== String) v+Right {x=1}++λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'+multiTrial @("x" .== Double .+ "y" .== String) v'+  :: Either+       (Var ('R '["x" ':-> Double, "y" ':-> String]))+       (Var ('R '["x" ':-> Integer]))+λ> multiTrial @("x" .== Double .+ "y" .== String) v'+Left {y="Foo"}++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).++> also :: Disjoint xs ys+>      => (Var xs -> a)+>      -> (Var ys -> a)+>      -> Var (xs .+ ys) -> a+> also f1 f2 e = case multiTrial e of+>   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

@@ -1,5 +1,5 @@ Name:                row-types-Version:             0.2.0.0+Version:             0.2.1.0 License:             MIT License-file:        LICENSE Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck@@ -18,7 +18,7 @@   label.  extra-source-files:-  Examples.lhs+  examples/Examples.lhs   README.md   CHANGELOG.md   LICENSE@@ -26,6 +26,7 @@  Library   Build-Depends: base >= 2 && < 5,+                 constraints,                  deepseq >= 1.4,                  hashable >= 1.2,                  unordered-containers >= 0.2,@@ -36,7 +37,6 @@                  , Data.Row.Variants                  , Data.Row.Switch   ghc-options: -W-  other-modules:   Extensions: AllowAmbiguousTypes,               ConstraintKinds,               DataKinds,@@ -78,6 +78,27 @@               TypeApplications,               TypeFamilies,               TypeOperators++test-suite test+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: tests, examples+  ghc-options: -W+  other-modules: Examples+  build-depends: base >= 2 && < 6+               , row-types+  Extensions: AllowAmbiguousTypes,+              DataKinds,+              FlexibleContexts,+              OverloadedLabels,+              PatternSynonyms,+              RankNTypes,+              ScopedTypeVariables,+              TypeApplications,+              TypeFamilies,+              TypeOperators,+              ViewPatterns+  source-repository head     type:     git

@@ -0,0 +1,6 @@++module Main where++import Examples ()++main = putStrLn "Test passes if Examples.lhs type-checks."