-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Extensible Records
--   
--   Extensible records for Haskell with lenses.
@package vinyl
@version 0.8.1.1

module Data.Vinyl.Functor

-- | This is identical to the <a>Identity</a> from
--   <a>Data.Functor.Identity</a> in "base" except for its <a>Show</a>
--   instance.
newtype Identity a
Identity :: a -> Identity a
[getIdentity] :: Identity a -> a

-- | Used this instead of <a>Identity</a> to make a record lazy in its
--   fields.
data Thunk a
Thunk :: a -> Thunk a
[getThunk] :: Thunk a -> a
newtype Lift (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l') (x :: k)
Lift :: op (f x) (g x) -> Lift
[getLift] :: Lift -> op (f x) (g x)
newtype Compose (f :: l -> *) (g :: k -> l) (x :: k)
Compose :: f (g x) -> Compose
[getCompose] :: Compose -> f (g x)
type f :. g = Compose f g
newtype Const (a :: *) (b :: k)
Const :: a -> Const
[getConst] :: Const -> a
instance forall a k (b :: k). Foreign.Storable.Storable a => Foreign.Storable.Storable (Data.Vinyl.Functor.Const a b)
instance Data.Traversable.Traversable (Data.Vinyl.Functor.Const a)
instance Data.Foldable.Foldable (Data.Vinyl.Functor.Const a)
instance GHC.Base.Functor (Data.Vinyl.Functor.Const a)
instance forall l (f :: l -> *) k (g :: k -> l) (x :: k). Foreign.Storable.Storable (f (g x)) => Foreign.Storable.Storable (Data.Vinyl.Functor.Compose f g x)
instance Data.Traversable.Traversable Data.Vinyl.Functor.Thunk
instance Data.Foldable.Foldable Data.Vinyl.Functor.Thunk
instance GHC.Base.Functor Data.Vinyl.Functor.Thunk
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Vinyl.Functor.Identity a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Vinyl.Functor.Identity a)
instance Foreign.Storable.Storable a => Foreign.Storable.Storable (Data.Vinyl.Functor.Identity a)
instance Data.Traversable.Traversable Data.Vinyl.Functor.Identity
instance Data.Foldable.Foldable Data.Vinyl.Functor.Identity
instance GHC.Base.Functor Data.Vinyl.Functor.Identity
instance forall k a (b :: k). GHC.Show.Show a => GHC.Show.Show (Data.Vinyl.Functor.Const a b)
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (Data.Vinyl.Functor.Compose f g)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable g) => Data.Foldable.Foldable (Data.Vinyl.Functor.Compose f g)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable g) => Data.Traversable.Traversable (Data.Vinyl.Functor.Compose f g)
instance (GHC.Base.Applicative f, GHC.Base.Applicative g) => GHC.Base.Applicative (Data.Vinyl.Functor.Compose f g)
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (Data.Vinyl.Functor.Lift (,) f g)
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (Data.Vinyl.Functor.Lift Data.Either.Either f g)
instance (GHC.Base.Applicative f, GHC.Base.Applicative g) => GHC.Base.Applicative (Data.Vinyl.Functor.Lift (,) f g)
instance GHC.Base.Applicative Data.Vinyl.Functor.Thunk
instance GHC.Base.Monad Data.Vinyl.Functor.Thunk
instance GHC.Show.Show a => GHC.Show.Show (Data.Vinyl.Functor.Thunk a)
instance GHC.Base.Applicative Data.Vinyl.Functor.Identity
instance GHC.Base.Monad Data.Vinyl.Functor.Identity
instance GHC.Show.Show a => GHC.Show.Show (Data.Vinyl.Functor.Identity a)

module Data.Vinyl.TypeLevel

-- | A mere approximation of the natural numbers. And their image as lifted
--   by <tt>-XDataKinds</tt> corresponds to the actual natural numbers.
data Nat
Z :: Nat
S :: !Nat -> Nat

-- | Produce a runtime <a>Int</a> value corresponding to a <a>Nat</a> type.
class NatToInt (n :: Nat)
natToInt :: NatToInt n => Int

-- | Reify a list of type-level natural number indices as runtime
--   <a>Int</a>s relying on instances of <a>NatToInt</a>.
class IndexWitnesses (is :: [Nat])
indexWitnesses :: IndexWitnesses is => [Int]

-- | Project the first component of a type-level tuple.

-- | Project the second component of a type-level tuple.

-- | A partial relation that gives the index of a value in a list.

-- | A partial relation that gives the indices of a sublist in a larger
--   list.

-- | Remove the first occurence of a type from a type-level list.

-- | A constraint-former which applies to every field in a record.

-- | Append for type-level lists.

-- | Constraint that all types in a type-level list satisfy a constraint.

-- | Constraint that each Constraint in a type-level list is satisfied by a
--   particular type.

-- | Constraint that all types in a type-level list satisfy each constraint
--   from a list of constraints.
--   
--   <tt>AllAllSat cs ts</tt> should be equivalent to <tt>AllConstrained
--   (AllSatisfied cs) ts</tt> if partial application of type families were
--   legal.
instance Data.Vinyl.TypeLevel.IndexWitnesses '[]
instance (Data.Vinyl.TypeLevel.IndexWitnesses is, Data.Vinyl.TypeLevel.NatToInt i) => Data.Vinyl.TypeLevel.IndexWitnesses (i : is)
instance Data.Vinyl.TypeLevel.NatToInt 'Data.Vinyl.TypeLevel.Z
instance Data.Vinyl.TypeLevel.NatToInt n => Data.Vinyl.TypeLevel.NatToInt ('Data.Vinyl.TypeLevel.S n)

module Data.Vinyl.Core

-- | A record is parameterized by a universe <tt>u</tt>, an interpretation
--   <tt>f</tt> and a list of rows <tt>rs</tt>. The labels or indices of
--   the record are given by inhabitants of the kind <tt>u</tt>; the type
--   of values at any label <tt>r :: u</tt> is given by its interpretation
--   <tt>f r :: *</tt>.
data Rec :: (u -> *) -> [u] -> *
[RNil] :: Rec f '[]
[:&] :: !(f r) -> !(Rec f rs) -> Rec f (r : rs)

-- | Two records may be pasted together.
rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs)

-- | A shorthand for <a>rappend</a>.
(<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
infixr 5 <+>

-- | <a>Rec</a> <tt>_ rs</tt> with labels in kind <tt>u</tt> gives rise to
--   a functor <tt>Hask^u -&gt; Hask</tt>; that is, a natural
--   transformation between two interpretation functors <tt>f,g</tt> may be
--   used to transport a value from <a>Rec</a> <tt>f rs</tt> to <a>Rec</a>
--   <tt>g rs</tt>.
rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs

-- | A shorthand for <a>rmap</a>.
(<<$>>) :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs
infixl 8 <<$>>

-- | An inverted shorthand for <a>rmap</a>.
(<<&>>) :: Rec f rs -> (forall x. f x -> g x) -> Rec g rs

-- | A record of components <tt>f r -&gt; g r</tt> may be applied to a
--   record of <tt>f</tt> to get a record of <tt>g</tt>.
rapply :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs

-- | A shorthand for <a>rapply</a>.
(<<*>>) :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
infixl 8 <<*>>

-- | Given a section of some functor, records in that functor of any size
--   are inhabited.
class RecApplicative rs
rpure :: RecApplicative rs => (forall x. f x) -> Rec f rs

-- | A record may be traversed with respect to its interpretation functor.
--   This can be used to yank (some or all) effects from the fields of the
--   record to the outside of the record.
rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec f rs -> h (Rec g rs)

-- | Given a natural transformation from the product of <tt>f</tt> and
--   <tt>g</tt> to <tt>h</tt>, we have a natural transformation from the
--   product of <tt><a>Rec</a> f</tt> and <tt><a>Rec</a> g</tt> to
--   <tt><a>Rec</a> h</tt>. You can also think about this operation as
--   zipping two records with the same element types but different
--   interpretations.
rzipWith :: (forall x. f x -> g x -> h x) -> (forall xs. Rec f xs -> Rec g xs -> Rec h xs)

-- | Map each element of a record to a monoid and combine the results.
rfoldMap :: forall f m rs. Monoid m => (forall x. f x -> m) -> Rec f rs -> m

-- | A record with uniform fields may be turned into a list.
recordToList :: Rec (Const a) rs -> [a]

-- | Wrap up a value with a capability given by its type
data Dict c a
[Dict] :: c a => a -> Dict c a

-- | Sometimes we may know something for <i>all</i> fields of a record, but
--   when you expect to be able to <i>each</i> of the fields, you are then
--   out of luck. Surely given <tt>∀x:u.φ(x)</tt> we should be able to
--   recover <tt>x:u ⊢ φ(x)</tt>! Sadly, the constraint solver is not quite
--   smart enough to realize this and we must make it patently obvious by
--   reifying the constraint pointwise with proof.
reifyConstraint :: RecAll f rs c => proxy c -> Rec f rs -> Rec (Dict c :. f) rs

-- | Build a record whose elements are derived solely from a constraint
--   satisfied by each.
rpureConstrained :: forall c (f :: u -> *) proxy ts. (AllConstrained c ts, RecApplicative ts) => proxy c -> (forall a. c a => f a) -> Rec f ts

-- | Build a record whose elements are derived solely from a list of
--   constraint constructors satisfied by each.
rpureConstraints :: forall cs (f :: * -> *) proxy ts. (AllAllSat cs ts, RecApplicative ts) => proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts
instance forall u (f :: u -> *) (rs :: [u]). Data.Vinyl.TypeLevel.RecAll f rs GHC.Show.Show => GHC.Show.Show (Data.Vinyl.Core.Rec f rs)
instance Data.Vinyl.Core.RecApplicative '[]
instance forall u (rs :: [u]) (r :: u). Data.Vinyl.Core.RecApplicative rs => Data.Vinyl.Core.RecApplicative (r : rs)
instance forall u (f :: u -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Vinyl.Core.Rec f)
instance forall u (f :: u -> *). Data.Type.Coercion.TestCoercion f => Data.Type.Coercion.TestCoercion (Data.Vinyl.Core.Rec f)
instance forall u (f :: u -> *). GHC.Base.Semigroup (Data.Vinyl.Core.Rec f '[])
instance forall a (f :: a -> *) (r :: a) (rs :: [a]). (GHC.Base.Monoid (f r), GHC.Base.Monoid (Data.Vinyl.Core.Rec f rs)) => GHC.Base.Semigroup (Data.Vinyl.Core.Rec f (r : rs))
instance forall u (f :: u -> *). GHC.Base.Monoid (Data.Vinyl.Core.Rec f '[])
instance forall a (f :: a -> *) (r :: a) (rs :: [a]). (GHC.Base.Monoid (f r), GHC.Base.Monoid (Data.Vinyl.Core.Rec f rs)) => GHC.Base.Monoid (Data.Vinyl.Core.Rec f (r : rs))
instance forall u (f :: u -> *). GHC.Classes.Eq (Data.Vinyl.Core.Rec f '[])
instance forall a (f :: a -> *) (r :: a) (rs :: [a]). (GHC.Classes.Eq (f r), GHC.Classes.Eq (Data.Vinyl.Core.Rec f rs)) => GHC.Classes.Eq (Data.Vinyl.Core.Rec f (r : rs))
instance forall u (f :: u -> *). GHC.Classes.Ord (Data.Vinyl.Core.Rec f '[])
instance forall a (f :: a -> *) (r :: a) (rs :: [a]). (GHC.Classes.Ord (f r), GHC.Classes.Ord (Data.Vinyl.Core.Rec f rs)) => GHC.Classes.Ord (Data.Vinyl.Core.Rec f (r : rs))
instance forall u (f :: u -> *). Foreign.Storable.Storable (Data.Vinyl.Core.Rec f '[])
instance forall a (f :: a -> *) (r :: a) (rs :: [a]). (Foreign.Storable.Storable (f r), Foreign.Storable.Storable (Data.Vinyl.Core.Rec f rs)) => Foreign.Storable.Storable (Data.Vinyl.Core.Rec f (r : rs))


-- | Lenses into record fields.
module Data.Vinyl.Lens

-- | The presence of a field in a record is witnessed by a lens into its
--   value. The third parameter to <a>RElem</a>, <tt>i</tt>, is there to
--   help the constraint solver realize that this is a decidable predicate
--   with respect to the judgemental equality in <tt>k</tt>.
class i ~ RIndex r rs => RecElem record (r :: k) (rs :: [k]) (i :: Nat)

-- | We can get a lens for getting and setting the value of a field which
--   is in a record. As a convenience, we take a proxy argument to fix the
--   particular field being viewed. These lenses are compatible with the
--   <tt>lens</tt> library. Morally:
--   
--   <pre>
--   rlens :: sing r =&gt; Lens' (Rec f rs) (f r)
--   </pre>
rlens :: (RecElem record r rs i, Functor g) => sing r -> (f r -> g (f r)) -> record f rs -> g (record f rs)

-- | For Vinyl users who are not using the <tt>lens</tt> package, we
--   provide a getter.
rget :: RecElem record r rs i => sing r -> record f rs -> f r

-- | For Vinyl users who are not using the <tt>lens</tt> package, we also
--   provide a setter. In general, it will be unambiguous what field is
--   being written to, and so we do not take a proxy argument here.
rput :: RecElem record r rs i => f r -> record f rs -> record f rs

-- | <a>RecElem</a> for classic vinyl <a>Rec</a> types.
type RElem = RecElem Rec

-- | If one field set is a subset another, then a lens of from the latter's
--   record to the former's is evident. That is, we can either cast a
--   larger record to a smaller one, or we may replace the values in a
--   slice of a record.
class is ~ RImage rs ss => RecSubset record (rs :: [k]) (ss :: [k]) is

-- | This is a lens into a slice of the larger record. Morally, we have:
--   
--   <pre>
--   rsubset :: Lens' (Rec f ss) (Rec f rs)
--   </pre>
rsubset :: (RecSubset record rs ss is, Functor g) => (record f rs -> g (record f rs)) -> record f ss -> g (record f ss)

-- | The getter of the <a>rsubset</a> lens is <a>rcast</a>, which takes a
--   larger record to a smaller one by forgetting fields.
rcast :: RecSubset record rs ss is => record f ss -> record f rs

-- | The setter of the <a>rsubset</a> lens is <a>rreplace</a>, which allows
--   a slice of a record to be replaced with different values.
rreplace :: RecSubset record rs ss is => record f rs -> record f ss -> record f ss
type RSubset = RecSubset Rec

-- | Two record types are equivalent when they are subtypes of each other.
type REquivalent rs ss is js = (RSubset rs ss is, RSubset ss rs js)

-- | A shorthand for <a>RElem</a> which supplies its index.
type r ∈ rs = RElem r rs (RIndex r rs)

-- | A shorthand for <a>RSubset</a> which supplies its image.
type rs ⊆ ss = RSubset rs ss (RImage rs ss)

-- | A shorthand for <a>REquivalent</a> which supplies its images.
type rs ≅ ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)

-- | A non-unicode equivalent of <tt>(⊆)</tt>.
type rs <: ss = rs ⊆ ss

-- | A non-unicode equivalent of <tt>(≅)</tt>.
type rs :~: ss = rs ≅ ss
instance forall k (r :: k) (ss :: [k]) (i :: Data.Vinyl.TypeLevel.Nat) (rs :: [k]) (is :: [Data.Vinyl.TypeLevel.Nat]). (Data.Vinyl.Lens.RElem r ss i, Data.Vinyl.Lens.RSubset rs ss is) => Data.Vinyl.Lens.RecSubset Data.Vinyl.Core.Rec (r : rs) ss (i : is)
instance forall k (ss :: [k]). Data.Vinyl.Lens.RecSubset Data.Vinyl.Core.Rec '[] ss '[]
instance forall a (r :: a) (s :: a) (rs :: [a]) (i :: Data.Vinyl.TypeLevel.Nat). (Data.Vinyl.TypeLevel.RIndex r (s : rs) ~ 'Data.Vinyl.TypeLevel.S i, Data.Vinyl.Lens.RElem r rs i) => Data.Vinyl.Lens.RecElem Data.Vinyl.Core.Rec r (s : rs) ('Data.Vinyl.TypeLevel.S i)
instance forall a (r :: a) (rs :: [a]). Data.Vinyl.Lens.RecElem Data.Vinyl.Core.Rec r (r : rs) 'Data.Vinyl.TypeLevel.Z


-- | Vinyl is a general solution to the records problem in Haskell using
--   type level strings and other modern GHC features, featuring static
--   structural typing (with a subtyping relation), and automatic
--   row-polymorphic lenses. All this is possible without Template Haskell.
--   
--   Let's work through a quick example. We'll need to enable some language
--   extensions first:
--   
--   <pre>
--   &gt;&gt;&gt; :set -XDataKinds
--   
--   &gt;&gt;&gt; :set -XPolyKinds
--   
--   &gt;&gt;&gt; :set -XTypeOperators
--   
--   &gt;&gt;&gt; :set -XTypeFamilies
--   
--   &gt;&gt;&gt; :set -XFlexibleContexts
--   
--   &gt;&gt;&gt; :set -XFlexibleInstances
--   
--   &gt;&gt;&gt; :set -XNoMonomorphismRestriction
--   
--   &gt;&gt;&gt; :set -XGADTs
--   
--   &gt;&gt;&gt; :set -XTypeSynonymInstances
--   
--   &gt;&gt;&gt; :set -XTemplateHaskell
--   
--   &gt;&gt;&gt; :set -XStandaloneDeriving
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Vinyl
--   
--   &gt;&gt;&gt; import Data.Vinyl.Functor
--   
--   &gt;&gt;&gt; import Control.Applicative
--   
--   &gt;&gt;&gt; import Control.Lens hiding (Identity)
--   
--   &gt;&gt;&gt; import Control.Lens.TH
--   
--   &gt;&gt;&gt; import Data.Char
--   
--   &gt;&gt;&gt; import Test.DocTest
--   
--   &gt;&gt;&gt; import Data.Singletons.TH (genSingletons)
--   
--   &gt;&gt;&gt; import Data.Maybe
--   </pre>
--   
--   Let's define a universe of fields which we want to use.
--   
--   First of all, we need a data type defining the field labels:
--   
--   <pre>
--   &gt;&gt;&gt; data Fields = Name | Age | Sleeping | Master deriving Show
--   </pre>
--   
--   Any record can be now described by a type-level list of these labels.
--   The <tt>DataKinds</tt> extension must be enabled to autmatically turn
--   all the constructors of the <tt>Field</tt> type into types.
--   
--   <pre>
--   &gt;&gt;&gt; type LifeForm = [Name, Age, Sleeping]
--   </pre>
--   
--   Now, we need a way to map our labels to concrete types. We use a type
--   family for this purpose. Unfortunately, type families aren't first
--   class in Haskell. That's why we also need a data type, with which we
--   will parametrise <a>Rec</a>. We also generate the necessary singletons
--   for each field label using Template Haskell.
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   type family ElF (f :: Fields) :: * where
--     ElF Name = String
--     ElF Age = Int
--     ElF Sleeping = Bool
--     ElF Master = Rec Attr LifeForm
--   newtype Attr f = Attr { _unAttr :: ElF f }
--   makeLenses ''Attr
--   genSingletons [ ''Fields ]
--   instance Show (Attr Name) where show (Attr x) = "name: " ++ show x
--   instance Show (Attr Age) where show (Attr x) = "age: " ++ show x
--   instance Show (Attr Sleeping) where show (Attr x) = "sleeping: " ++ show x
--   instance Show (Attr Master) where show (Attr x) = "master: " ++ show x
--   :}
--   </pre>
--   
--   To make field construction easier, we define an operator. The first
--   argument of this operator is a singleton - a constructor bringing the
--   data-kinded field label type into the data level. It's needed because
--   there can be multiple labels with the same field type, so by just
--   supplying a value of type <tt>ElF f</tt> there would be no way to
--   deduce the correct "f".
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let (=::) :: sing f -&gt; ElF f -&gt; Attr f
--       _ =:: x = Attr x
--   :}
--   </pre>
--   
--   Now, let's try to make an entity that represents a human:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let jon = (SName =:: "jon")
--          :&amp; (SAge =:: 23)
--          :&amp; (SSleeping =:: False)
--          :&amp; RNil
--   :}
--   </pre>
--   
--   Automatically, we can show the record:
--   
--   <pre>
--   &gt;&gt;&gt; print jon
--   {name: "jon", age: 23, sleeping: False}
--   </pre>
--   
--   And its types are all inferred with no problem. Now, make a dog! Dogs
--   are life-forms, but unlike humans, they have masters. So, let’s build
--   my dog:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let tucker = (SName =:: "tucker")
--             :&amp; (SAge =:: 9)
--             :&amp; (SSleeping =:: True)
--             :&amp; (SMaster =:: jon)
--             :&amp; RNil
--   :}
--   </pre>
--   
--   Now, if we want to wake entities up, we don't want to have to write a
--   separate wake-up function for both dogs and humans (even though they
--   are of different type). Luckily, we can use the built-in lenses to
--   focus on a particular field in the record for access and update,
--   without losing additional information:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let wakeUp :: (Sleeping ∈ fields) =&gt; Rec Attr fields -&gt; Rec Attr fields
--       wakeUp = rput $ SSleeping =:: False
--   :}
--   </pre>
--   
--   Now, the type annotation on <tt>wakeUp</tt> was not necessary; I just
--   wanted to show how intuitive the type is. Basically, it takes as an
--   input any record that has a <a>Bool</a> field labelled
--   <tt>sleeping</tt>, and modifies that specific field in the record
--   accordingly.
--   
--   <pre>
--   &gt;&gt;&gt; let tucker' = wakeUp tucker
--   
--   &gt;&gt;&gt; let jon' = wakeUp jon
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tucker' ^. rlens SSleeping
--   sleeping: False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tucker ^. rlens SSleeping
--   sleeping: True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; jon' ^. rlens SSleeping
--   sleeping: False
--   </pre>
--   
--   We can also access the entire lens for a field using the rLens
--   function; since lenses are composable, it’s super easy to do deep
--   update on a record:
--   
--   <pre>
--   &gt;&gt;&gt; let masterSleeping = rlens SMaster . unAttr . rlens SSleeping
--   
--   &gt;&gt;&gt; let tucker'' = masterSleeping .~ (SSleeping =:: True) $ tucker'
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tucker'' ^. masterSleeping
--   sleeping: True
--   </pre>
--   
--   A record <tt>Rec f xs</tt> is a subtype of a record <tt>Rec f ys</tt>
--   if <tt>ys ⊆ xs</tt>; that is to say, if one record can do everything
--   that another record can, the former is a subtype of the latter. As
--   such, we should be able to provide an upcast operator which "forgets"
--   whatever makes one record different from another (whether it be extra
--   data, or different order).
--   
--   Therefore, the following works:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let upcastedTucker :: Rec Attr LifeForm
--       upcastedTucker = rcast tucker
--   :}
--   </pre>
--   
--   The subtyping relationship between record types is expressed with the
--   <a>&lt;:</a> constraint; so, <a>rcast</a> is of the following type:
--   
--   <pre>
--   rcast :: r1 &lt;: r2 =&gt; Rec f r1 -&gt; Rec f r2
--   </pre>
--   
--   Also provided is a "≅" constraint which indicates record congruence
--   (that is, two record types differ only in the order of their fields).
--   
--   In fact, <a>rcast</a> is actually given as a special case of the lens
--   <a>rsubset</a>, which lets you modify entire (possibly non-contiguous)
--   slices of a record!
--   
--   Consider the following declaration:
--   
--   <pre>
--   data Rec :: (u -&gt; *) -&gt; [u] -&gt; * where
--     RNil :: Rec f '[]
--     (:&amp;) :: f r -&gt; Rec f rs -&gt; Rec f (r ': rs)
--   </pre>
--   
--   Records are implicitly parameterized over a kind <tt>u</tt>, which
--   stands for the "universe" or key space. Keys (inhabitants of
--   <tt>u</tt>) are then interpreted into the types of their values by the
--   first parameter to <a>Rec</a>, <tt>f</tt>. An extremely powerful
--   aspect of Vinyl records is that you can construct natural
--   transformations between different interpretation functors
--   <tt>f,g</tt>, or postcompose some other functor onto the stack. This
--   can be used to immerse each field of a record in some particular
--   effect modality, and then the library functions can be used to
--   traverse and accumulate these effects.
--   
--   Let's imagine that we want to do validation on a record that
--   represents a name and an age:
--   
--   <pre>
--   &gt;&gt;&gt; type Person = [Name, Age]
--   </pre>
--   
--   We've decided that names must be alphabetic, and ages must be
--   positive. For validation, we'll use <a>Maybe</a> for now, though you
--   should use a left-accumulating <tt>Validation</tt> type (the module
--   <tt>Data.Either.Validation</tt> from the <tt>either</tt> package
--   provides such a type, though we do not cover it here).
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let goodPerson :: Rec Attr Person
--       goodPerson = (SName =:: "Jon")
--                 :&amp; (SAge =:: 20)
--                 :&amp; RNil
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let badPerson = (SName =:: "J#@#$on")
--                :&amp; (SAge =:: 20)
--                :&amp; RNil
--   :}
--   </pre>
--   
--   We'll give validation a (rather poor) shot.
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let
--       validatePerson :: Rec Attr Person -&gt; Maybe (Rec Attr Person)
--       validatePerson p = (\n a -&gt; (SName =:: n) :&amp; (SAge =:: a) :&amp; RNil) &lt;$&gt; vName &lt;*&gt; vAge
--         where
--         vName = validateName $ p ^. rlens SName . unAttr
--         vAge  = validateAge $ p ^. rlens SAge . unAttr
--         validateName str | all isAlpha str = Just str
--         validateName _ = Nothing
--         validateAge i | i &gt;= 0 = Just i
--         validateAge _ = Nothing
--   :}
--   </pre>
--   
--   Let's try it out:
--   
--   <pre>
--   &gt;&gt;&gt; isJust $ validatePerson goodPerson
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust $ validatePerson badPerson
--   False
--   </pre>
--   
--   The results are as expected (<tt>Just</tt> for <tt>goodPerson</tt>,
--   and a <tt>Nothing</tt> for <tt>badPerson</tt>); but this was not very
--   fun to build.
--   
--   Further, it would be nice to have some notion of a partial record;
--   that is, if part of it can't be validated, it would still be nice to
--   be able to access the rest. What if we could make a version of this
--   record where the elements themselves were validation functions, and
--   then that record could be applied to a plain one, to get a record of
--   validated fields? That's what we’re going to do.
--   
--   <pre>
--   &gt;&gt;&gt; type Validator f = Lift (-&gt;) f (Maybe :. f)
--   </pre>
--   
--   Let's parameterize a record by it: when we do, then an element of type
--   <tt>a</tt> should be a function <tt>Identity a -&gt; Result e a</tt>:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let lift f = Lift $ Compose . f
--       validateName (Attr str) | all isAlpha str = Just (Attr str)
--       validateName _ = Nothing
--       validateAge (Attr i) | i &gt;= 0 = Just (Attr i)
--       validateAge _ = Nothing
--       vperson :: Rec (Validator Attr) Person
--       vperson = lift validateName :&amp; lift validateAge :&amp; RNil
--   :}
--   </pre>
--   
--   And we can use the special application operator
--   <a>&lt;&lt;*&gt;&gt;</a> (which is analogous to <a>&lt;*&gt;</a>, but
--   generalized a bit) to use this to validate a record:
--   
--   <pre>
--   &gt;&gt;&gt; let goodPersonResult = vperson &lt;&lt;*&gt;&gt; goodPerson
--   
--   &gt;&gt;&gt; let badPersonResult  = vperson &lt;&lt;*&gt;&gt; badPerson
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust . getCompose $ goodPersonResult ^. rlens SName
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust . getCompose $ goodPersonResult ^. rlens SAge
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust . getCompose $ badPersonResult ^. rlens SName
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust . getCompose $ badPersonResult ^. rlens SAge
--   True
--   </pre>
--   
--   So now we have a partial record, and we can still do stuff with its
--   contents. Next, we can even recover the original behavior of the
--   validator (that is, to give us a value of type <tt>Maybe (Rec Attr
--   Person)</tt>) using <a>rtraverse</a>:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let mgoodPerson :: Maybe (Rec Attr Person)
--       mgoodPerson = rtraverse getCompose goodPersonResult
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; let mbadPerson  = rtraverse getCompose badPersonResult
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust mgoodPerson
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isJust mbadPerson
--   False
--   </pre>
module Data.Vinyl.Tutorial.Overview

module Data.Vinyl.Notation

-- | A shorthand for <a>rappend</a>.
(<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
infixr 5 <+>

-- | A shorthand for <a>rapply</a>.
(<<*>>) :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
infixl 8 <<*>>

-- | A shorthand for <a>rmap</a>.
(<<$>>) :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs
infixl 8 <<$>>

-- | An inverted shorthand for <a>rmap</a>.
(<<&>>) :: Rec f rs -> (forall x. f x -> g x) -> Rec g rs

-- | A record is parameterized by a universe <tt>u</tt>, an interpretation
--   <tt>f</tt> and a list of rows <tt>rs</tt>. The labels or indices of
--   the record are given by inhabitants of the kind <tt>u</tt>; the type
--   of values at any label <tt>r :: u</tt> is given by its interpretation
--   <tt>f r :: *</tt>.
data Rec :: (u -> *) -> [u] -> *
[:&] :: !(f r) -> !(Rec f rs) -> Rec f (r : rs)

-- | A shorthand for <a>RElem</a> which supplies its index.
type r ∈ rs = RElem r rs (RIndex r rs)

-- | A shorthand for <a>RSubset</a> which supplies its image.
type rs ⊆ ss = RSubset rs ss (RImage rs ss)

-- | A shorthand for <a>REquivalent</a> which supplies its images.
type rs ≅ ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)

-- | A non-unicode equivalent of <tt>(⊆)</tt>.
type rs <: ss = rs ⊆ ss

-- | A non-unicode equivalent of <tt>(≅)</tt>.
type rs :~: ss = rs ≅ ss


-- | This module uses <a>RecAll</a> to extend common typeclass methods to
--   records. Generally, it is preferable to use the original typeclass
--   methods to these variants. For example, in most places where
--   <a>recCompare</a> could be used, you could use <a>compare</a> instead.
--   They are useful in scenarios that involve working on unknown subsets
--   of a record's fields because <a>RecAll</a> constraints can easily be
--   weakened. An example of this is given at the bottom of this page.
module Data.Vinyl.Class.Method
recEq :: RecAll f rs Eq => Rec f rs -> Rec f rs -> Bool
recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering

-- | This function differs from the original <a>mempty</a> in that it takes
--   an argument. In some cases, you will already have a record of the type
--   you are interested in, and that can be passed an the argument. In
--   other situations where this is not the case, you may need the
--   interpretation function of the argument record to be <tt>Const ()</tt>
--   or <tt>Proxy</tt> so the you can generate the argument with
--   <a>rpure</a>.
recMempty :: RecAll f rs Monoid => Rec proxy rs -> Rec f rs
recMappend :: RecAll f rs Monoid => Rec f rs -> Rec f rs -> Rec f rs

-- | This function differs from the original <a>mconcat</a>. See
--   <a>recMempty</a>.
recMconcat :: RecAll f rs Monoid => Rec proxy rs -> [Rec f rs] -> Rec f rs
recAdd :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recSubtract :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recMultiply :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recAbs :: RecAll f rs Num => Rec f rs -> Rec f rs
recSignum :: RecAll f rs Num => Rec f rs -> Rec f rs
recNegate :: RecAll f rs Num => Rec f rs -> Rec f rs

-- | This function differs from the original <a>minBound</a>. See
--   <a>recMempty</a>.
recMinBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs

-- | This function differs from the original <a>maxBound</a>. See
--   <a>recMempty</a>.
recMaxBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs


-- | Constant-time field accessors for extensible records. The trade-off is
--   the usual lists vs arrays one: it is fast to add an element to the
--   head of a list, but element access is linear time; array access time
--   is uniform, but extending the array is more slower.
module Data.Vinyl.ARec

-- | An array-backed extensible record with constant-time field access.
newtype ARec (f :: k -> *) (ts :: [k])
ARec :: (Array Int Any) -> ARec

-- | Convert a <a>Rec</a> into an <a>ARec</a> for constant-time field
--   access.
toARec :: forall f ts. (NatToInt (RLength ts)) => Rec f ts -> ARec f ts

-- | Defines a constraint that lets us index into an <a>ARec</a> in order
--   to produce a <a>Rec</a> using <a>fromARec</a>.
class (NatToInt (RIndex t ts)) => IndexableField ts t

-- | Convert an <a>ARec</a> into a <a>Rec</a>.
fromARec :: forall f ts. (RecApplicative ts, AllConstrained (IndexableField ts) ts) => ARec f ts -> Rec f ts

-- | Get a field from an <a>ARec</a>.
aget :: forall t f ts. (NatToInt (RIndex t ts)) => ARec f ts -> f t

-- | Set a field in an <a>ARec</a>.
aput :: forall t f ts. (NatToInt (RIndex t ts)) => f t -> ARec f ts -> ARec f ts

-- | Define a lens for a field of an <a>ARec</a>.
alens :: (Functor g, NatToInt (RIndex t ts)) => (f t -> g (f t)) -> ARec f ts -> g (ARec f ts)

-- | Get a subset of a record's fields.
arecGetSubset :: forall rs ss f. (IndexWitnesses (RImage rs ss), NatToInt (RLength rs)) => ARec f ss -> ARec f rs

-- | Set a subset of a larger record's fields to all of the fields of a
--   smaller record.
arecSetSubset :: forall rs ss f. (IndexWitnesses (RImage rs ss)) => ARec f ss -> ARec f rs -> ARec f ss
instance forall k (t :: k) (ts :: [k]). Data.Vinyl.TypeLevel.NatToInt (Data.Vinyl.TypeLevel.RIndex t ts) => Data.Vinyl.ARec.IndexableField ts t
instance forall k (rs :: [k]) (f :: k -> *). (Data.Vinyl.TypeLevel.AllConstrained (Data.Vinyl.ARec.IndexableField rs) rs, Data.Vinyl.Core.RecApplicative rs, GHC.Show.Show (Data.Vinyl.Core.Rec f rs)) => GHC.Show.Show (Data.Vinyl.ARec.ARec f rs)
instance forall k (rs :: [k]) (f :: k -> *). (Data.Vinyl.TypeLevel.AllConstrained (Data.Vinyl.ARec.IndexableField rs) rs, Data.Vinyl.Core.RecApplicative rs, GHC.Classes.Eq (Data.Vinyl.Core.Rec f rs)) => GHC.Classes.Eq (Data.Vinyl.ARec.ARec f rs)
instance forall k (rs :: [k]) (f :: k -> *). (Data.Vinyl.TypeLevel.AllConstrained (Data.Vinyl.ARec.IndexableField rs) rs, Data.Vinyl.Core.RecApplicative rs, GHC.Classes.Ord (Data.Vinyl.Core.Rec f rs)) => GHC.Classes.Ord (Data.Vinyl.ARec.ARec f rs)
instance forall k (i :: Data.Vinyl.TypeLevel.Nat) (t :: k) (ts :: [k]). (i ~ Data.Vinyl.TypeLevel.RIndex t ts, Data.Vinyl.TypeLevel.NatToInt (Data.Vinyl.TypeLevel.RIndex t ts)) => Data.Vinyl.Lens.RecElem Data.Vinyl.ARec.ARec t ts i
instance forall k (is :: [Data.Vinyl.TypeLevel.Nat]) (rs :: [k]) (ss :: [k]). (is ~ Data.Vinyl.TypeLevel.RImage rs ss, Data.Vinyl.TypeLevel.IndexWitnesses is, Data.Vinyl.TypeLevel.NatToInt (Data.Vinyl.TypeLevel.RLength rs)) => Data.Vinyl.Lens.RecSubset Data.Vinyl.ARec.ARec rs ss is


-- | Commonly used <a>Rec</a> instantiations.
module Data.Vinyl.Derived

-- | Alias for Field spec
type a ::: b = '(a, b)
data ElField (field :: (Symbol, *))
[Field] :: KnownSymbol s => !t -> ElField '(s, t)

-- | A record of named fields.
type FieldRec = Rec ElField

-- | An <a>ARec</a> of named fields to provide constant-time field access.
type AFieldRec ts = ARec ElField ts

-- | Heterogeneous list whose elements are evaluated during list
--   construction.
type HList = Rec Identity

-- | Heterogeneous list whose elements are left as-is during list
--   construction (cf. <a>HList</a>).
type LazyHList = Rec Thunk

-- | Get the data payload of an <a>ElField</a>.
getField :: ElField '(s, t) -> t

-- | Get the label name of an <a>ElField</a>.
getLabel :: forall s t. ElField '(s, t) -> String

-- | <a>ElField</a> is isomorphic to a functor something like <tt>Compose
--   ElField ('(,) s)</tt>.
fieldMap :: (a -> b) -> ElField '(s, a) -> ElField '(s, b)

-- | Lens for an <tt>ElField'</tt>s data payload.
rfield :: Functor f => (a -> f b) -> ElField '(s, a) -> f (ElField '(s, b))

-- | Operator for creating an <a>ElField</a>. With the
--   <tt>-XOverloadedLabels</tt> extension, this permits usage such as,
--   <tt>#foo =: 23</tt> to produce a value of type <tt>ElField ("foo" :::
--   Int)</tt>.
(=:) :: KnownSymbol l => Label (l :: Symbol) -> (v :: *) -> ElField (l ::: v)
infix 8 =:

-- | Get a named field from a record.
rgetf :: forall l f v record us. HasField record l us v => Label l -> record f us -> f (l ::: v)

-- | Get the value associated with a named field from a record.
rvalf :: HasField record l us v => Label l -> record ElField us -> v

-- | Set a named field. <tt>rputf #foo 23</tt> sets the field named
--   <tt>#foo</tt> to <tt>23</tt>.
rputf :: forall l v record us. (HasField record l us v, KnownSymbol l) => Label l -> v -> record ElField us -> record ElField us

-- | A lens into a <a>Rec</a> identified by a <a>Label</a>.
rlensf' :: forall l v record g f us. (Functor g, HasField record l us v) => Label l -> (f (l ::: v) -> g (f (l ::: v))) -> record f us -> g (record f us)

-- | A lens into the payload value of a <a>Rec</a> field identified by a
--   <a>Label</a>.
rlensf :: forall l v record g f us. (Functor g, HasField record l us v) => Label l -> (v -> g v) -> record ElField us -> g (record ElField us)

-- | Shorthand for a <a>FieldRec</a> with a single field.
(=:=) :: KnownSymbol s => proxy '(s, a) -> a -> FieldRec '['(s, a)]

-- | A proxy for field types.
data SField (field :: k)
SField :: SField

-- | Constraint that a label is associated with a particular type in a
--   record.
type HasField record l fs v = (RecElem record (l ::: v) fs (RIndex (l ::: v) fs), FieldType l fs ~ v)

-- | Proxy for label type
data Label (a :: Symbol)
Label :: Label

-- | Defines a constraint that lets us extract the label from an
--   <a>ElField</a>. Used in <a>rmapf</a> and <a>rpuref</a>.
class (KnownSymbol (Fst a), a ~ '(Fst a, Snd a)) => KnownField a

-- | Shorthand for working with records of fields as in <a>rmapf</a> and
--   <a>rpuref</a>.
type AllFields fs = (AllConstrained KnownField fs, RecApplicative fs)

-- | Map a function between functors across a <a>Rec</a> taking advantage
--   of knowledge that each element is an <a>ElField</a>.
rmapf :: AllFields fs => (forall a. KnownField a => f a -> g a) -> Rec f fs -> Rec g fs

-- | Construct a <a>Rec</a> with <a>ElField</a> elements.
rpuref :: AllFields fs => (forall a. KnownField a => f a) -> Rec f fs

-- | Operator synonym for <a>rmapf</a>.
(<<$$>>) :: AllFields fs => (forall a. KnownField a => f a -> g a) -> Rec f fs -> Rec g fs

-- | Produce a <a>Rec</a> of the labels of a <a>Rec</a> of <a>ElField</a>s.
rlabels :: AllFields fs => Rec (Const String) fs
instance GHC.Show.Show (Data.Vinyl.Derived.Label a)
instance GHC.Classes.Eq (Data.Vinyl.Derived.Label a)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Data.Vinyl.Derived.ElField '(s, t))
instance GHC.Classes.Ord t => GHC.Classes.Ord (Data.Vinyl.Derived.ElField '(s, t))
instance forall k (l :: GHC.Types.Symbol) (v :: k). GHC.TypeLits.KnownSymbol l => Data.Vinyl.Derived.KnownField (l Data.Vinyl.Derived.::: v)
instance (s ~ s') => GHC.OverloadedLabels.IsLabel s (Data.Vinyl.Derived.Label s')
instance forall k (a :: k). GHC.Classes.Eq (Data.Vinyl.Derived.SField a)
instance forall k (a :: k). GHC.Classes.Ord (Data.Vinyl.Derived.SField a)
instance forall k (s :: GHC.Types.Symbol) (t :: k). GHC.TypeLits.KnownSymbol s => GHC.Show.Show (Data.Vinyl.Derived.SField '(s, t))
instance GHC.Show.Show t => GHC.Show.Show (Data.Vinyl.Derived.ElField '(s, t))
instance (GHC.TypeLits.KnownSymbol s, Foreign.Storable.Storable t) => Foreign.Storable.Storable (Data.Vinyl.Derived.ElField '(s, t))

module Data.Vinyl

-- | An array-backed extensible record with constant-time field access.
data ARec (f :: k -> *) (ts :: [k])

-- | Convert a <a>Rec</a> into an <a>ARec</a> for constant-time field
--   access.
toARec :: forall f ts. (NatToInt (RLength ts)) => Rec f ts -> ARec f ts

-- | Convert an <a>ARec</a> into a <a>Rec</a>.
fromARec :: forall f ts. (RecApplicative ts, AllConstrained (IndexableField ts) ts) => ARec f ts -> Rec f ts


-- | Provides combinators for currying and uncurrying functions over
--   arbitrary vinyl records.
module Data.Vinyl.Curry
class RecordCurry ts

-- | N-ary version of <a>curry</a> over functorial records.
--   
--   Example specialized signatures:
--   
--   <pre>
--   rcurry :: (Rec Maybe '[Int, Double] -&gt; Bool) -&gt; Maybe Int -&gt; Maybe Double -&gt; Bool
--   rcurry :: (Rec (Either Int) '[Double, String, ()] -&gt; Int) -&gt; Either Int Double -&gt; Either Int String -&gt; Either Int () -&gt; Int
--   rcurry :: (Rec f '[] -&gt; Bool) -&gt; Bool
--   
--   </pre>
rcurry :: RecordCurry ts => (Rec f ts -> a) -> CurriedF f ts a

-- | N-ary version of <a>curry</a> over pure records.
--   
--   Example specialized signatures:
--   
--   <pre>
--   rcurry' :: (Rec Identity '[Int, Double] -&gt; Bool) -&gt; Int -&gt; Double -&gt; Bool
--   rcurry' :: (Rec Identity '[Double, String, ()] -&gt; Int) -&gt; Double -&gt; String -&gt; () -&gt; Int
--   rcurry' :: (Rec Identity '[] -&gt; Bool) -&gt; Bool
--   
--   </pre>
rcurry' :: RecordCurry ts => (Rec Identity ts -> a) -> Curried ts a

-- | N-ary version of <a>uncurry</a> over functorial records.
--   
--   Example specialized signatures:
--   
--   <pre>
--   runcurry :: (Maybe Int -&gt; Maybe Double -&gt; String) -&gt; Rec Maybe '[Int, Double] -&gt; String
--   runcurry :: (IO FilePath -&gt; String) -&gt; Rec IO '[FilePath] -&gt; String
--   runcurry :: Int -&gt; Rec f '[] -&gt; Int
--   </pre>
runcurry :: CurriedF f ts a -> Rec f ts -> a

-- | N-ary version of <a>uncurry</a> over pure records.
--   
--   Example specialized signatures:
--   
--   <pre>
--   runcurry' :: (Int -&gt; Double -&gt; String) -&gt; Rec Identity '[Int, Double] -&gt; String
--   runcurry' :: Int -&gt; Rec Identity '[] -&gt; Int
--   </pre>
--   
--   Example usage:
--   
--   <pre>
--   f :: Rec Identity '[Bool, Int, Double] -&gt; Either Int Double
--   f = runcurry' $ b x y -&gt; if b then Left x else Right y
--   </pre>
runcurry' :: Curried ts a -> Rec Identity ts -> a

-- | Lift an N-ary function to work over a record of <a>Applicative</a>
--   computations.
--   
--   <pre>
--   &gt;&gt;&gt; runcurryA' (+) (Just 2 :&amp; Just 3 :&amp; RNil)
--   Just 5
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runcurryA' (+) (Nothing :&amp; Just 3 :&amp; RNil)
--   Nothing
--   </pre>
runcurryA' :: (Applicative f) => Curried ts a -> Rec f ts -> f a

-- | Lift an N-ary function over types in <tt>g</tt> to work over a record
--   of <a>Compose</a>d <a>Applicative</a> computations. A more general
--   version of <a>runcurryA'</a>.
--   
--   Example specialized signatures:
--   
--   <pre>
--   runcurryA :: (g x -&gt; g y -&gt; a) -&gt; Rec (Compose Maybe g) '[x, y] -&gt; Maybe a
--   </pre>
runcurryA :: (Applicative f) => CurriedF g ts a -> Rec (Compose f g) ts -> f a

-- | For the list of types <tt>ts</tt>, <tt><a>Curried</a> ts a</tt> is a
--   curried function type from arguments of types in <tt>ts</tt> to a
--   result of type <tt>a</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Curried '[Int, Bool, String] Int
--   Curried '[Int, Bool, String] Int :: *
--   = Int -&gt; Bool -&gt; [Char] -&gt; Int
--   </pre>

-- | For the type-level list <tt>ts</tt>, <tt><a>CurriedF</a> f ts a</tt>
--   is a curried function type from arguments of type <tt>f t</tt> for
--   <tt>t</tt> in <tt>ts</tt>, to a result of type <tt>a</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! CurriedF Maybe '[Int, Bool, String] Int
--   CurriedF Maybe '[Int, Bool, String] Int :: *
--   = Maybe Int -&gt; Maybe Bool -&gt; Maybe [Char] -&gt; Int
--   </pre>
instance Data.Vinyl.Curry.RecordCurry '[]
instance Data.Vinyl.Curry.RecordCurry ts => Data.Vinyl.Curry.RecordCurry (t : ts)


-- | Co-records: open sum types.
--   
--   Consider a record with three fields <tt>A</tt>, <tt>B</tt>, and
--   <tt>C</tt>. A record is a product of its fields; that is, it contains
--   all of them: <tt>A</tt>, <tt>B</tt>, <i>and</i> <tt>C</tt>. If we want
--   to talk about a value whose type is one of those three types, it is
--   <i>any one</i> of type <tt>A</tt>, <tt>B</tt>, <i>or</i> <tt>C</tt>.
--   The type <tt>CoRec '[A,B,C]</tt> corresponds to this sum type.
module Data.Vinyl.CoRec

-- | Generalize algebraic sum types.
data CoRec :: (k -> *) -> [k] -> *
[CoRec] :: RElem a ts (RIndex a ts) => !(f a) -> CoRec f ts

-- | Apply a function to a <a>CoRec</a> value. The function must accept
--   <i>any</i> variant.
foldCoRec :: (forall a. RElem a ts (RIndex a ts) => f a -> b) -> CoRec f ts -> b

-- | A Field of a <a>Rec</a> <a>Identity</a> is a <a>CoRec</a>
--   <a>Identity</a>.
type Field = CoRec Identity

-- | A function type constructor that takes its arguments in the reverse
--   order.
newtype Op b a
Op :: a -> b -> Op b a
[runOp] :: Op b a -> a -> b

-- | We can inject a a <a>CoRec</a> into a <a>Rec</a> where every field of
--   the <a>Rec</a> is <a>Nothing</a> except for the one whose type
--   corresponds to the type of the given <a>CoRec</a> variant.
coRecToRec :: RecApplicative ts => CoRec f ts -> Rec (Maybe :. f) ts

-- | Shorthand for applying <a>coRecToRec</a> with common functors.
coRecToRec' :: RecApplicative ts => CoRec Identity ts -> Rec Maybe ts

-- | Fold a field selection function over a <a>Rec</a>.
class FoldRec ss ts
foldRec :: FoldRec ss ts => (CoRec f ss -> CoRec f ss -> CoRec f ss) -> CoRec f ss -> Rec f ts -> CoRec f ss

-- | Apply a natural transformation to a variant.
coRecMap :: (forall x. f x -> g x) -> CoRec f ts -> CoRec g ts

-- | This can be used to pull effects out of a <a>CoRec</a>.
coRecTraverse :: Functor h => (forall x. f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)

-- | Fold a field selection function over a non-empty <a>Rec</a>.
foldRec1 :: FoldRec (t : ts) ts => (CoRec f (t : ts) -> CoRec f (t : ts) -> CoRec f (t : ts)) -> Rec f (t : ts) -> CoRec f (t : ts)

-- | Similar to <a>First</a>: find the first field that is not
--   <a>Nothing</a>.
firstField :: FoldRec ts ts => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)

-- | Similar to <a>Last</a>: find the last field that is not
--   <a>Nothing</a>.
lastField :: FoldRec ts ts => Rec (Maybe :. f) ts -> Maybe (CoRec f ts)

-- | Apply a type class method on a <a>CoRec</a>. The first argument is a
--   <a>Proxy</a> value for a <i>list</i> of <a>Constraint</a>
--   constructors. For example, <tt>onCoRec [pr|Num,Ord|] (&gt; 20) r</tt>.
--   If only one constraint is needed, use the <tt>pr1</tt> quasiquoter.
onCoRec :: forall (cs :: [* -> Constraint]) f ts b. (AllAllSat cs ts, Functor f, RecApplicative ts) => Proxy cs -> (forall a. AllSatisfied cs a => a -> b) -> CoRec f ts -> f b

-- | Apply a type class method on a <a>Field</a>. The first argument is a
--   <a>Proxy</a> value for a <i>list</i> of <a>Constraint</a>
--   constructors. For example, <tt>onCoRec [pr|Num,Ord|] (&gt; 20) r</tt>.
--   If only one constraint is needed, use the <tt>pr1</tt> quasiquoter.
onField :: forall cs ts b. (AllAllSat cs ts, RecApplicative ts) => Proxy cs -> (forall a. AllSatisfied cs a => a -> b) -> Field ts -> b

-- | Build a record whose elements are derived solely from a list of
--   constraint constructors satisfied by each.
reifyDicts :: forall cs f proxy (ts :: [*]). (AllAllSat cs ts, RecApplicative ts) => proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts

-- | Given a proxy of type t and a 'CoRec Identity' that might be a t, try
--   to convert the CoRec to a t.
asA :: (t ∈ ts, RecApplicative ts) => proxy t -> CoRec Identity ts -> Maybe t

-- | Pattern match on a CoRec by specifying handlers for each case. Note
--   that the order of the Handlers has to match the type level list
--   (t:ts).
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let testCoRec = Col (Identity False) :: CoRec Identity [Int, String, Bool] in
--   match testCoRec $
--         (H $ \i -&gt; "my Int is the successor of " ++ show (i - 1))
--      :&amp; (H $ \s -&gt; "my String is: " ++ s)
--      :&amp; (H $ \b -&gt; "my Bool is not: " ++ show (not b) ++ " thus it is " ++ show b)
--      :&amp; RNil
--   :}
--   "my Bool is not: True thus it is False"
--   </pre>
match :: CoRec Identity ts -> Handlers ts b -> b

-- | Helper for handling a variant of a <a>CoRec</a>: either the function
--   is applied to the variant or the type of the <a>CoRec</a> is refined
--   to reflect the fact that the variant is <i>not</i> compatible with the
--   type of the would-be handler.
class RIndex t ts ~ i => Match1 t ts i
match1' :: Match1 t ts i => Handler r t -> Rec Maybe ts -> Either r (Rec Maybe (RDelete t ts))

-- | Handle a single variant of a <a>CoRec</a>: either the function is
--   applied to the variant or the type of the <a>CoRec</a> is refined to
--   reflect the fact that the variant is <i>not</i> compatible with the
--   type of the would-be handler
match1 :: (Match1 t ts (RIndex t ts), RecApplicative ts, FoldRec (RDelete t ts) (RDelete t ts)) => Handler r t -> CoRec Identity ts -> Either r (CoRec Identity (RDelete t ts))
matchNil :: CoRec f '[] -> r

-- | Newtype around functions for a to b
newtype Handler b a
H :: (a -> b) -> Handler b a

-- | 'Handlers ts b', is essentially a list of functions, one for each type
--   in ts. All functions produce a value of type <tt>b</tt>. Hence,
--   'Handlers ts b' would represent something like the type-level list: [t
--   -&gt; b | t in ts ]
type Handlers ts b = Rec (Handler b) ts
instance Data.Vinyl.CoRec.Match1 t (t : ts) 'Data.Vinyl.TypeLevel.Z
instance (Data.Vinyl.CoRec.Match1 t ts i, Data.Vinyl.TypeLevel.RIndex t (s : ts) ~ 'Data.Vinyl.TypeLevel.S i, Data.Vinyl.TypeLevel.RDelete t (s : ts) ~ (s : Data.Vinyl.TypeLevel.RDelete t ts)) => Data.Vinyl.CoRec.Match1 t (s : ts) ('Data.Vinyl.TypeLevel.S i)
instance forall k (ss :: [k]). Data.Vinyl.CoRec.FoldRec ss '[]
instance forall a (t :: a) (ss :: [a]) (ts :: [a]). (t Data.Vinyl.Lens.∈ ss, Data.Vinyl.CoRec.FoldRec ss ts) => Data.Vinyl.CoRec.FoldRec ss (t : ts)
instance (Data.Vinyl.TypeLevel.AllConstrained GHC.Show.Show ts, Data.Vinyl.Core.RecApplicative ts) => GHC.Show.Show (Data.Vinyl.CoRec.CoRec Data.Vinyl.Functor.Identity ts)
instance (Data.Vinyl.TypeLevel.RecAll GHC.Base.Maybe ts GHC.Classes.Eq, Data.Vinyl.Core.RecApplicative ts) => GHC.Classes.Eq (Data.Vinyl.CoRec.CoRec Data.Vinyl.Functor.Identity ts)
