content: > {-# LANGUAGE AllowAmbiguousTypes #-}
  > {-# LANGUAGE DataKinds #-}
  > {-# LANGUAGE DeriveGeneric #-}
  > {-# LANGUAGE FlexibleContexts #-}
  > {-# LANGUAGE OverloadedLabels #-}
  > {-# LANGUAGE PartialTypeSignatures #-}
  > {-# LANGUAGE ScopedTypeVariables #-}
  > {-# LANGUAGE TypeOperators #-}
  > {-# LANGUAGE ViewPatterns #-}
  > 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.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
  
  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.  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
  --------------------------------------------------------------------------------
  
  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:
  
  λ> origin'
   #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 :: 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
  
  Or, with lenses, we could write move as:
  
  > 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
  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, 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
  
  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
  
  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:
  
  λ> 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
  Right 1
  λ> trial v #y
  Left {x=1}
  λ> trial v' #x
  Left {y="Foo"}
  λ> trial v' #y
  Right "Foo"
  
  If trialing at a label l succeeds, then it provides a Right value of the value at l.
  If not, it provides a Left 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) = "Showable of "++show n
  > myShow (Var.view #y -> Just s) = "String of "++s
  > myShow _ = "Unknown"
  
  λ> myShow v
  "Showable 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) = "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 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) = "Integer of "++show n
  > myShowRestricted (Var.view #y -> Just s) = "String of "++s
  > myShowRestricted _ = error "Unreachable"
  
  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.)
  
  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 -> "Integer 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" ':-> Integer]))
         (Var ('R '["x" ':-> Double, "y" ':-> String]))
  λ> multiTrial @("x" .== Double .+ "y" .== String) v
  Left {x=1}
  
  λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'
  multiTrial @("x" .== Double .+ "y" .== String) v'
    :: Either
         (Var ('R '["x" ':-> Integer]))
         (Var ('R '["x" ':-> Double, "y" ':-> String]))
  λ> multiTrial @("x" .== Double .+ "y" .== String) v'
  Right {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).  We can even use
  it to combine dispatching of two different variants at once:
  
  > 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'
  
  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.
  