packages feed

vinyl 0.4.3 → 0.5

raw patch · 21 files changed

+533/−720 lines, 21 filesdep −template-haskelldep ~basedep ~vinyl

Dependencies removed: template-haskell

Dependency ranges changed: base, vinyl

Files

Data/Vinyl.hs view
@@ -1,16 +1,10 @@ module Data.Vinyl   ( module Data.Vinyl.Core   , module Data.Vinyl.Derived-  , module Data.Vinyl.Operators   , module Data.Vinyl.Lens-  , module Data.Vinyl.Witnesses-  , module Data.Vinyl.Constraint   ) where  import Data.Vinyl.Core import Data.Vinyl.Derived-import Data.Vinyl.Operators import Data.Vinyl.Lens-import Data.Vinyl.Constraint-import Data.Vinyl.Witnesses
− Data/Vinyl/Constraint.hs 
@@ -1,50 +0,0 @@-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}--module Data.Vinyl.Constraint-  ( (<:)(..)-  , (:~:)-  , (~=)-  , RecAll-  ) where--import Data.Vinyl.Core-import Data.Vinyl.Witnesses-import Data.Vinyl.TyFun-import GHC.Prim (Constraint)---- | One record is a subtype of another if the fields of the latter are a--- subset of the fields of the former.-class (xs :: [k]) <: (ys :: [k]) where-  cast :: Rec el f xs -> Rec el f ys--instance xs <: '[] where-  cast _ = RNil--instance (y ∈ xs, xs <: ys) => xs <: (y ': ys) where-  cast xs = ith (implicitly :: Elem y xs) xs :& cast xs-    where-      ith :: Elem r rs -> Rec el f rs -> f (el $ r)-      ith Here (a :& _) = a-      ith (There p) (_ :& as) = ith p as---- | If two records types are subtypes of each other, that means that they--- differ only in order of fields.-type r1 :~: r2 = (r1 <: r2, r2 <: r1)---- | Term-level record congruence.-(~=) :: (Eq (Rec el f xs), xs :~: ys) => Rec el f xs -> Rec el f ys -> Bool-x ~= y = x == (cast y)--type family RecAll (el :: TyFun k l -> *) (f :: * -> *) (rs :: [k]) (c :: * -> Constraint) :: Constraint-type instance RecAll el f '[] c = ()-type instance RecAll el f (r ': rs) c = (c (f (el $ r)), RecAll el f rs c)-
Data/Vinyl/Core.hs view
@@ -1,80 +1,191 @@-{-# LANGUAGE BangPatterns        #-}-{-# LANGUAGE DataKinds           #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE FlexibleInstances   #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE PolyKinds           #-}-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeFamilies        #-}-{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE BangPatterns          #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}  module Data.Vinyl.Core where -import Data.Vinyl.TyFun-import Control.Applicative import Data.Monoid-import Data.Vinyl.Idiom.Identity import Foreign.Ptr (castPtr, plusPtr) import Foreign.Storable (Storable(..))+import Data.Vinyl.Functor+import Control.Applicative hiding (Const(..))+import Data.Typeable (Proxy(..))+import Data.List (intercalate)+import Data.Vinyl.TypeLevel --- | A record is parameterized by a universe @u@, list of rows @rs@, a large--- elimination @el@, and a type constructor @f@ to be applied to the--- interpretation @el r@ of each of those @r@.-data Rec (el :: TyFun u * -> *) (f :: * -> *) (rrs :: [u]) where-  RNil :: Rec el f '[]-  (:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r ': rs)+-- | A record is parameterized by a universe @u@, an interpretation @f@ and a+-- list of rows @rs@.  The labels or indices of the record are given by+-- inhabitants of the kind @u@; the type of values at any label @r :: u@ is+-- given by its interpretation @f r :: *@.+data Rec :: (u -> *) -> [u] -> * where+  RNil :: Rec f '[]+  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)+ infixr :&+infixr 5  <+>+infixl 8 <<$>>+infixl 8 <<*>> --- | Shorthand for a record with a single field. Lifts the field's--- value into the chosen functor automatically.-(=:) :: Applicative f => sing k -> el $ k -> Rec el f '[ k ]-_ =: x = pure x :& RNil+-- | Two records may be pasted together.+rappend+  :: Rec f as+  -> Rec f bs+  -> Rec f (as ++ bs)+rappend RNil ys = ys+rappend (x :& xs) ys = x :& (xs `rappend` ys) --- | Shorthand for a record with a single field. This is useful for--- @Applicative@ or @Monad@ic intialization of records as in the idiom:------ > dist $ myField <-: someIO <+> yourField <-: otherIO-(<-:) :: sing r -> f (el $ r) -> Rec el f '[r]-_ <-: x = x :& RNil-infixr 6 <-:+-- | A shorthand for 'rappend'.+(<+>)+  :: Rec f as+  -> Rec f bs+  -> Rec f (as ++ bs)+(<+>) = rappend --- | Records constructed using the above combinators will often be polymorphic--- in their interpreter @el@. To avoid providing a type annotation, one can--- provide their interpreters with a singleton tag and pass that in.-withUniverse :: (forall x. el x) -> Rec el f rs -> Rec el f rs-withUniverse _ x = x-{-# INLINE withUniverse #-}+-- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u ->+-- Hask@; that is, a natural transformation between two interpretation functors+-- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@.+rmap+  :: (forall x. f x -> g x)+  -> Rec f rs+  -> Rec g rs+rmap _ RNil = RNil+rmap η (x :& xs) = η x :& (η `rmap` xs)+{-# INLINE rmap #-} -instance Monoid (Rec el f '[]) where+-- | A shorthand for 'rmap'.+(<<$>>)+  :: (forall x. f x -> g x)+  -> Rec f rs+  -> Rec g rs+(<<$>>) = rmap+{-# INLINE (<<$>>) #-}++-- | An inverted shorthand for 'rmap'.+(<<&>>)+  :: Rec f rs+  -> (forall x. f x -> g x)+  -> Rec g rs+xs <<&>> f = rmap f xs+{-# INLINE (<<&>>) #-}++-- | A record of components @f r -> g r@ may be applied to a record of @f@ to+-- get a record of @g@.+rapply+  :: Rec (Lift (->) f g) rs+  -> Rec f rs+  -> Rec g rs+rapply RNil RNil = RNil+rapply (f :& fs) (x :& xs) = getLift f x :& (fs `rapply` xs)+{-# INLINE rapply #-}++-- | A shorthand for 'rapply'.+(<<*>>)+  :: Rec (Lift (->) f g) rs+  -> Rec f rs+  -> Rec g rs+(<<*>>) = rapply+{-# INLINE (<<*>>) #-}++-- | Given a section of some functor, records in that functor of any size are+-- inhabited.+class RecApplicative rs where+  rpure+    :: (forall x. f x)+    -> Rec f rs+instance RecApplicative '[] where+  rpure _ = RNil+  {-# INLINE rpure #-}+instance RecApplicative rs => RecApplicative (r ': rs) where+  rpure s = s :& rpure s+  {-# INLINE rpure #-}++-- | 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)+rtraverse _ RNil      = pure RNil+rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs++-- | A record with uniform fields may be turned into a list.+recordToList+  :: Rec (Const a) rs+  -> [a]+recordToList RNil = []+recordToList (x :& xs) = getConst x : recordToList xs++-- | Wrap up a value with a capability given by its type+data Dict c a where+  Dict+    :: c a+    => a+    -> Dict c a++-- | Sometimes we may know something for /all/ fields of a record, but when+-- you expect to be able to /each/ of the fields, you are then out of luck.+-- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! 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+reifyConstraint prx rec =+  case rec of+    RNil -> RNil+    (x :& xs) -> Compose (Dict x) :& reifyConstraint prx xs++-- | Records may be shown insofar as their points may be shown.+-- 'reifyConstraint' is used to great effect here.+instance RecAll f rs Show => Show (Rec f rs) where+  show xs =+    (\str -> "{" <> str <> "}")+      . intercalate "; "+      . recordToList+      . rmap (\(Compose (Dict x)) -> Const $ show x)+      $ reifyConstraint (Proxy :: Proxy Show) xs++instance Monoid (Rec f '[]) where   mempty = RNil   RNil `mappend` RNil = RNil -instance (Monoid (el $ r), Monoid (Rec el f rs), Applicative f) => Monoid (Rec el f (r ': rs)) where-  mempty = pure mempty :& mempty-  (x :& xs) `mappend` (y :& ys) = liftA2 mappend x y :& (xs `mappend` ys)+instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where+  mempty = mempty :& mempty+  (x :& xs) `mappend` (y :& ys) = (x <> y) :& (xs <> ys) -instance Eq (Rec el f '[]) where+instance Eq (Rec f '[]) where   _ == _ = True-instance (Eq (f (el $ r)), Eq (Rec el f rs)) => Eq (Rec el f (r ': rs)) where+instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where   (x :& xs) == (y :& ys) = (x == y) && (xs == ys) -instance Storable (Rec el Identity '[]) where+instance Storable (Rec f '[]) where   sizeOf _    = 0   alignment _ = 0   peek _      = return RNil   poke _ RNil = return () -instance (Storable (el $ r), Storable (Rec el Identity rs)) => Storable (Rec el Identity (r ': rs)) where-  sizeOf _ = sizeOf (undefined :: el $ r) + sizeOf (undefined :: Rec el Identity rs)+instance (Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) where+  sizeOf _ = sizeOf (undefined :: f r) + sizeOf (undefined :: Rec f rs)   {-# INLINABLE sizeOf #-}-  alignment _ =  alignment (undefined :: el $ r)+  alignment _ =  alignment (undefined :: f r)   {-# INLINABLE alignment #-}   peek ptr = do !x <- peek (castPtr ptr)-                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: el $ r))-                return $ Identity x :& xs+                !xs <- peek (ptr `plusPtr` sizeOf (undefined :: f r))+                return $ x :& xs   {-# INLINABLE peek #-}-  poke ptr (Identity !x :& xs) = poke (castPtr ptr) x >>-                                 poke (ptr `plusPtr` sizeOf (undefined :: el $ r)) xs+  poke ptr (!x :& xs) = poke (castPtr ptr) x >> poke (ptr `plusPtr` sizeOf (undefined :: f r)) xs   {-# INLINEABLE poke #-}-
Data/Vinyl/Derived.hs view
@@ -1,26 +1,18 @@+{-# LANGUAGE DataKinds  #-}+{-# LANGUAGE GADTs      #-} {-# LANGUAGE PolyKinds  #-} {-# LANGUAGE RankNTypes #-}  module Data.Vinyl.Derived where  import Data.Vinyl.Core-import qualified Data.Vinyl.Idiom.Identity as I-import qualified Data.Vinyl.Idiom.Thunk as I-import qualified Data.Vinyl.Universe as U--import Control.Applicative--type PlainRec el = Rec el I.Identity-type LazyPlainRec el = Rec el I.Thunk-type FieldRec = Rec U.ElField-type PlainFieldRec = Rec U.ElField I.Identity-type HList = Rec U.Id I.Identity-type LazyHList = Rec U.Id I.Thunk+import Data.Vinyl.Functor --- | Fixes a polymorphic record into the 'Identity' functor.-toPlainRec :: (forall f. Applicative f => Rec el f rs) -> PlainRec el rs-toPlainRec xs = xs+import GHC.TypeLits -toLazyPlainRec :: (forall f. Applicative f => Rec el f rs) -> LazyPlainRec el rs-toLazyPlainRec xs = xs+data ElField (field :: (Symbol, *)) where+  Field :: KnownSymbol s => t -> ElField '(s,t) +type FieldRec = Rec ElField+type HList = Rec Identity+type LazyHList = Rec Thunk
Data/Vinyl/Functor.hs view
@@ -1,14 +1,85 @@-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveFoldable             #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE TypeOperators              #-}  module Data.Vinyl.Functor where  import Control.Applicative+import Data.Foldable+import Data.Traversable+import Foreign.Storable -class Presheaf f where-  contramap :: (a -> b) -> (f b -> f a)+newtype Identity a+  = Identity { getIdentity :: a }+    deriving ( Functor+             , Foldable+             , Traversable+             , Storable+             ) -newtype Lift op f g x = Lift { runLift :: op (f x) (g x) }+data Thunk a+  = Thunk { getThunk :: a }+    deriving ( Functor+             , Foldable+             , Traversable+             ) +newtype Lift (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l') (x :: k)+  = Lift { getLift :: op (f x) (g x) }++newtype Compose (f :: l -> *) (g :: k -> l) (x :: k)+  = Compose { getCompose :: f (g x) }+    deriving (Storable)++type f :. g = Compose f g++newtype Const (a :: *) (b :: k)+  = Const { getConst :: a }+    deriving ( Functor+             , Foldable+             , Traversable+             , Storable+             )++instance (Functor f, Functor g) => Functor (Compose f g) where+  fmap f (Compose x) = Compose (fmap (fmap f) x)++instance (Foldable f, Foldable g) => Foldable (Compose f g) where+  foldMap f (Compose t) = foldMap (foldMap f) t++instance (Traversable f, Traversable g) => Traversable (Compose f g) where+  traverse f (Compose t) = Compose <$> traverse (traverse f) t++instance (Applicative f, Applicative g) => Applicative (Compose f g) where+  pure x = Compose (pure (pure x))+  Compose f <*> Compose x = Compose ((<*>) <$> f <*> x)++instance Applicative Identity where+  pure = Identity+  Identity f <*> Identity x = Identity (f x)++instance Monad Identity where+  return = Identity+  Identity x >>= f = f x++instance Show a => Show (Identity a) where+  show (Identity x) = show x++instance Applicative Thunk where+  pure = Thunk+  (Thunk f) <*> (Thunk x) = Thunk (f x)++instance Monad Thunk where+  return = Thunk+  (Thunk x) >>= f = f x++instance Show a => Show (Thunk a) where+  show (Thunk x) = show x+ instance (Functor f, Functor g) => Functor (Lift (,) f g) where   fmap f (Lift (x, y)) = Lift (fmap f x, fmap f y) @@ -16,20 +87,7 @@   fmap f (Lift (Left x)) = Lift . Left . fmap f $ x   fmap f (Lift (Right x)) = Lift . Right . fmap f $ x -instance (Presheaf f, Presheaf g) => Presheaf (Lift (,) f g) where-  contramap f (Lift (x, y)) = Lift (contramap f x, contramap f y)--instance (Presheaf f, Presheaf g) => Presheaf (Lift Either f g) where-  contramap f (Lift (Left x)) = Lift . Left . contramap f $ x-  contramap f (Lift (Right x)) = Lift . Right . contramap f $ x- instance (Applicative f, Applicative g) => Applicative (Lift (,) f g) where   pure x = Lift (pure x, pure x)   Lift (f, g) <*> Lift (x, y) = Lift (f <*> x, g <*> y)--instance (Presheaf f, Functor g) => Functor (Lift (->) f g) where-  fmap f (Lift ηx) = Lift $ fmap f . ηx . contramap f--instance (Functor f, Presheaf g) => Presheaf (Lift (->) f g) where-  contramap f (Lift ηx) = Lift $ contramap f . ηx . fmap f
− Data/Vinyl/Idiom/Identity.hs 
@@ -1,25 +0,0 @@-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveTraversable #-}--module Data.Vinyl.Idiom.Identity where--import Control.Applicative-import Data.Foldable-import Data.Traversable--newtype Identity a-  = Identity-  { runIdentity :: a-  } deriving (Functor, Foldable, Traversable)--instance Applicative Identity where-  pure = Identity-  (Identity f) <*> (Identity x) = Identity (f x)--instance Monad Identity where-  return = Identity-  (Identity x) >>= f = f x--instance Show a => Show (Identity a) where-  show (Identity x) = show x
− Data/Vinyl/Idiom/Thunk.hs 
@@ -1,25 +0,0 @@-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveTraversable #-}--module Data.Vinyl.Idiom.Thunk where--import Control.Applicative-import Data.Foldable-import Data.Traversable--data Thunk a-  = Thunk-  { runThunk :: a-  } deriving (Functor, Foldable, Traversable)--instance Applicative Thunk where-  pure = Thunk-  (Thunk f) <*> (Thunk x) = Thunk (f x)--instance Monad Thunk where-  return = Thunk-  (Thunk x) >>= f = f x--instance Show a => Show (Thunk a) where-  show (Thunk x) = show x
− Data/Vinyl/Idiom/Validation.hs 
@@ -1,32 +0,0 @@-{-# LANGUAGE TypeOperators #-}--module Data.Vinyl.Idiom.Validation where--import Data.Vinyl.Idiom.Identity-import Data.Vinyl.Functor--import Control.Applicative-import Data.Monoid---- | A type which is similar to 'Either', except that it has a--- slightly different Applicative instance.-data Result e a-  = Failure e-  | Success a-  deriving (Show, Eq)---- | Validators transform identities into results.-type Validator e = Lift (->) Identity (Result e)--instance Functor (Result e) where-  fmap f (Success x) = Success $ f x-  fmap _ (Failure e) = Failure e---- | The 'Applicative' instance to 'Result' relies on its error type--- being a 'Monoid'. That way, it can accumulate errors.-instance Monoid e => Applicative (Result e) where-  pure = Success-  (Success f) <*> (Success x)  = Success $ f x-  (Failure e) <*> (Success _)  = Failure e-  (Success _) <*> (Failure e)  = Failure e-  (Failure e) <*> (Failure e') = Failure $ e <> e'
Data/Vinyl/Lens.hs view
@@ -1,82 +1,138 @@+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-} {-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds             #-} {-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE TypeOperators         #-} --- | A small, /en passant/ lens implementation to provide accessors--- for record fields. Lenses produced with 'rLens' are fully--- compatible with the @lens@ package.-module Data.Vinyl.Lens where+module Data.Vinyl.Lens+  ( RElem(..)+  , RSubset(..)+  , REquivalent+  , type (∈)+  , type (⊆)+  , type (≅)+  , type (<:)+  , type (:~:)+  ) where  import Data.Vinyl.Core-import Data.Vinyl.Derived-import Data.Vinyl.TyFun-import Data.Vinyl.Witnesses-import Data.Vinyl.Idiom.Identity+import Data.Vinyl.Functor+import Data.Vinyl.TypeLevel+import Data.Typeable (Proxy(..)) -import Control.Applicative+-- | The presence of a field in a record is witnessed by a lens into its value.+-- The third parameter to 'RElem', @i@, is there to help the constraint solver+-- realize that this is a decidable predicate with respect to the judgemental+-- equality in @k@.+class i ~ RIndex r rs => RElem (r :: k) (rs :: [k]) (i :: Nat) where --- | Project a field from a 'Rec'.-rGet' :: (r ∈ rs) => sing r -> Rec el f rs -> f (el $ r)-rGet' r = getConst . rLens' r Const-{-# INLINE rGet' #-}+  -- | 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 @lens@+  -- library. Morally:+  --+  -- > rlens :: sing r => Lens' (Rec f rs) (f r)+  rlens+    :: Functor g+    => sing r+    -> (f r -> g (f r))+    -> Rec f rs+    -> g (Rec f rs) --- | Project a field from a 'PlainRec'.-rGet :: (r ∈ rs) => sing r -> PlainRec el rs -> el $ r-rGet = (runIdentity .) . rGet'-{-# INLINE rGet #-}+  -- | For Vinyl users who are not using the @lens@ package, we provide a getter.+  rget+    :: sing r+    -> Rec f rs+    -> f r+  rget k = getConst . rlens k Const --- | Set a field in a 'Rec' over an arbitrary functor.-rPut' :: (r ∈ rs) => sing r -> f (el $ r) -> Rec el f rs -> Rec el f rs-rPut' r x = runIdentity . rLens' r (Identity . const x)-{-# INLINE rPut' #-}+  -- | For Vinyl users who are not using the @lens@ 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+    :: f r+    -> Rec f rs+    -> Rec f rs+  rput y = getIdentity . rlens Proxy (\_ -> Identity y) --- | Set a field in a 'PlainRec'.-rPut :: (r ∈ rs) => sing r -> el $ r -> PlainRec el rs -> PlainRec el rs-rPut r x = rPut' r (Identity x)-{-# INLINE rPut #-}+-- This is an internal convenience stolen from the @lens@ library.+lens+  :: Functor f+  => (t -> s)+  -> (t -> a -> b)+  -> (s -> f a)+  -> t+  -> f b+lens sa sbt afb s = fmap (sbt s) $ afb (sa s)+{-# INLINE lens #-} --- | Modify a field.-rMod :: (r ∈ rs , Functor f) => sing r -> (el $ r -> el $ r) -> Rec el f rs -> Rec el f rs-rMod r f = runIdentity . rLens' r (Identity . fmap f)-{-# INLINE rMod #-}+instance RElem r (r ': rs) Z where+  rlens _ f (x :& xs) = fmap (:& xs) (f x)+  {-# INLINE rlens #-} --- We manually unroll several levels of 'Elem' value traversal to help--- GHC statically index into small records.+instance (RIndex r (s ': rs) ~ S i, RElem r rs i) => RElem r (s ': rs) (S i) where+  rlens p f (x :& xs) = fmap (x :&) (rlens p f xs)+  {-# INLINE rlens #-} --- | Provide a lens to a record field. Note that this implementation--- does not support polymorphic update. In the parlance of the @lens@--- package,------ > rLens' :: (r ∈ rs) => Sing r -> Lens' (Rec el f rs) (f (el $ r))-rLens' :: forall r rs f g el sing. (r ∈ rs , Functor g) => sing r -> (f (el $ r) -> g (f (el $ r))) -> Rec el f rs -> g (Rec el f rs)-rLens' _ f = go implicitly-  where go :: Elem r rr -> Rec el f rr -> g (Rec el f rr)-        go Here (x :& xs) = fmap (:& xs) (f x)-        go (There Here) (a :& x :& xs) = fmap ((a :&) . (:& xs)) (f x)-        go (There (There Here)) (a :& b :& x :& xs) =-          fmap (\x' -> a :& b :& x' :& xs) (f x)-        go (There (There (There Here))) (a :& b :& c :& x :& xs) =-          fmap (\x' -> a :& b :& c :& x' :& xs) (f x)-        go (There (There (There (There Here)))) (a :& b :& c :& d :& x :& xs) =-          fmap (\x' -> a :& b :& c :& d :& x' :& xs) (f x)-        go (There (There (There (There p)))) (a :& b :& c :& d :& xs) =-          fmap (\xs' -> a :& b :& c :& d :& xs') (go' p xs)-        {-# INLINE go #-}+-- | 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 => RSubset (rs :: [k]) (ss :: [k]) is where -        go' :: Elem r rr -> Rec el f rr -> g (Rec el f rr)-        go' Here (x :& xs) = fmap (:& xs) (f x)-        go' (There p) (x :& xs) = fmap (x :&) (go p xs)-        {-# INLINABLE go' #-}-{-# INLINE rLens' #-}+  -- | This is a lens into a slice of the larger record. Morally, we have:+  --+  -- > rsubset :: Lens' (Rec f ss) (Rec f rs)+  rsubset+    :: Functor g+    => (Rec f rs -> g (Rec f rs))+    -> Rec f ss+    -> g (Rec f ss) --- | A lens into a 'PlainRec' that smoothly interoperates with lenses--- from the @lens@ package. Note that polymorphic update is not--- supported. In the parlance of the @lens@ package,------ > rLens :: (r ∈ rs) => sing r -> Lens' (PlainRec el rs) (el $ r)-rLens :: forall r rs g el sing. (r ∈ rs , Functor g) => sing r -> (el $ r -> g (el $ r)) -> PlainRec el rs -> g (PlainRec el rs)-rLens r = rLens' r . lenser runIdentity (const Identity)-  where lenser sa sbt afb s = sbt s <$> afb (sa s)-{-# INLINE rLens #-}+  -- | The getter of the 'rsubset' lens is 'rcast', which takes a larger record+  -- to a smaller one by forgetting fields.+  rcast+    :: Rec f ss+    -> Rec f rs+  rcast = getConst . rsubset Const+  {-# INLINE rcast #-}++  -- | The setter of the 'rsubset' lens is 'rreplace', which allows a slice of+  -- a record to be replaced with different values.+  rreplace+    :: Rec f rs+    -> Rec f ss+    -> Rec f ss+  rreplace rs = getIdentity . rsubset (\_ -> Identity rs)+  {-# INLINE rreplace #-}++instance RSubset '[] ss '[] where+  rsubset = lens (const RNil) const++instance (RElem r ss i , RSubset rs ss is) => RSubset (r ': rs) ss (i ': is) where+  rsubset = lens (\ss -> rget Proxy ss :& rcast ss) set+    where+      set :: Rec f ss -> Rec f (r ': rs) -> Rec f ss+      set ss (r :& rs) = rput r $ rreplace rs ss++-- | 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 'RElem' which supplies its index.+type r ∈ rs = RElem r rs (RIndex r rs)++-- | A shorthand for 'RSubset' which supplies its image.+type rs ⊆ ss = RSubset rs ss (RImage rs ss)++-- | A shorthand for 'REquivalent' which supplies its images.+type rs ≅ ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)++-- | A non-unicode equivalent of @(⊆)@.+type rs <: ss = rs ⊆ ss++-- | A non-unicode equivalent of @(≅)@.+type rs :~: ss = rs ≅ ss
Data/Vinyl/Notation.hs view
@@ -1,17 +1,17 @@+{-# LANGUAGE ExplicitNamespaces #-}+ module Data.Vinyl.Notation-  ( (:~:)-  , (<-:)-  , (<:)()-  , (<+>)+  ( (<+>)   , (<<*>>)   , (<<$>>)-  , (=:)-  , (~=)+  , (<<&>>)   , Rec((:&))-  , Semantics((:~>))+  , type (∈)+  , type (⊆)+  , type (≅)+  , type (<:)+  , type (:~:)   ) where -import Data.Vinyl.Constraint import Data.Vinyl.Core-import Data.Vinyl.Operators-import Data.Vinyl.TH+import Data.Vinyl.Lens
− Data/Vinyl/Operators.hs 
@@ -1,100 +0,0 @@-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE TypeFamilies          #-}-{-# LANGUAGE TypeOperators         #-}--module Data.Vinyl.Operators-  ( (<<$>>)-  , (<<*>>)-  , (<+>)-  , type (++)-  , RecApplicative(rpure)-  , rtraverse-  , rdist-  , rdistLazy-  , FoldRec(foldRec)-  , recToList-  , showWithNames-  , rshow-  ) where--import Data.Vinyl.Core-import Data.Vinyl.Functor-import Data.Vinyl.TyFun-import Data.Vinyl.Witnesses-import Data.Vinyl.Constraint-import Data.Vinyl.Derived-import qualified Data.Vinyl.Idiom.Identity as I-import qualified Data.Vinyl.Idiom.Thunk as I-import qualified Data.Vinyl.Universe.Const as U--import Control.Applicative-import qualified Data.List as L (intercalate)---- | Append for records.-(<+>) :: Rec el f as -> Rec el f bs -> Rec el f (as ++ bs)-RNil      <+> xs = xs-(x :& xs) <+> ys =  x :& (xs <+> ys)-infixr 5  <+>---- | Append for type-level lists.-type family (as :: [k]) ++ (bs :: [k]) :: [k]-type instance '[] ++ bs = bs-type instance (a ': as) ++ bs  = a ': (as ++ bs)--(<<$>>) :: (forall x. f x -> g x) -> Rec el f rs -> Rec el g rs-_   <<$>> RNil    = RNil-eta <<$>> x :& xs = eta x :& (eta <<$>> xs)-infixl 8 <<$>>-{-# INLINE (<<$>>) #-}--(<<*>>) :: Rec el (Lift (->) f g) rs -> Rec el f rs -> Rec el g rs-RNil    <<*>> RNil    = RNil-f :& fs <<*>> x :& xs = runLift f x :& (fs <<*>> xs)-infixl 8 <<*>>-{-# INLINE (<<*>>) #-}--class RecApplicative rs where-  rpure :: (forall x. f x) -> Rec el f rs-instance RecApplicative '[] where-  rpure _ = RNil-instance RecApplicative rs => RecApplicative (f ': rs) where-  rpure s = s :& rpure s--class FoldRec r a where-  foldRec :: (a -> b -> b) -> b -> r -> b-instance FoldRec (Rec el f '[]) a where-  foldRec _ z RNil = z-instance (t ~ (el $ r), FoldRec (Rec el f rs) (f t)) => FoldRec (Rec el f (r ': rs)) (f t) where-  foldRec f z (x :& xs) = f x (foldRec f z xs)---- | Accumulates a homogenous record into a list-recToList :: FoldRec (Rec el f rs) (f t) => Rec el f rs -> [f t]-recToList = foldRec (\e a -> [e] ++ a) []--rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec el f rs -> h (Rec el g rs)-rtraverse _ RNil      = pure RNil-rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs--rdist :: Applicative f => Rec el f rs -> f (PlainRec el rs)-rdist = rtraverse $ fmap I.Identity--rdistLazy :: Applicative f => Rec el f rs -> f (LazyPlainRec el rs)-rdistLazy = rtraverse $ fmap I.Thunk--showWithNames :: RecAll el f rs Show => PlainRec (U.Const String) rs -> Rec el f rs -> String-showWithNames names rec = "{ " ++ L.intercalate ", " (go names rec []) ++ " }"-  where-    go :: RecAll el f rs Show => PlainRec (U.Const String) rs -> Rec el f rs -> [String] -> [String]-    go RNil RNil ss = ss-    go (I.Identity n :& ns) (x :& xs) ss = (n ++ " =: " ++ show x) : go ns xs ss--rshow :: (Implicit (PlainRec (U.Const String) rs), RecAll el f rs Show) => Rec el f rs -> String-rshow = showWithNames implicitly-
− Data/Vinyl/TH.hs 
@@ -1,59 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE QuasiQuotes #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleInstances #-}--module Data.Vinyl.TH-  ( makeUniverse-  , makeUniverse'-  , Semantics(..)-  , semantics-  ) where--import Language.Haskell.TH-import Data.Vinyl.TyFun--makeUniverse :: Name -> Q [Dec]-makeUniverse u = makeUniverse' u ("El" ++ nameBase u)--makeUniverse' :: Name -> String -> Q [Dec]-makeUniverse' u elName = do-  let elu = mkName elName-  u' <- conT u--  tvs <- do-    el <- newName "el"-    tyfun <- conT ''TyFun-    return [KindedTV el (AppT (AppT tyfun u') StarT)]--  let cons = [NormalC elu []]-  return [DataD [] elu tvs cons []]--class TyRep r where-  asType :: r -> TypeQ-instance TyRep Name where-  asType = conT-instance TyRep (Q Type) where-  asType = id--data Semantics = forall s t. (TyRep t, TyRep s) => t :~> s--semantics :: Name -> [Semantics] -> Q [Dec]-semantics elu sems = sequence (map inst sems)-  where-    inst :: Semantics -> Q Dec-    inst (u :~> t) = do-      elu' <- conT elu-      u' <- asType u-      t' <- asType t-      return $ TySynInstD ''App-#if __GLASGOW_HASKELL__ > 707-          (TySynEqn [elu',u'] t')-#else-                    [elu',u'] t'-#endif
− Data/Vinyl/TyFun.hs 
@@ -1,14 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}--module Data.Vinyl.TyFun where--data TyFun :: * -> * -> *-type family App (f :: TyFun k l -> *) (a :: k) :: l--data TC :: (k -> *) -> TyFun k * -> *-type instance App (TC t) x = t x-type f $ x = App f x-
+ Data/Vinyl/TypeLevel.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}++module Data.Vinyl.TypeLevel where++import GHC.Exts++-- | A mere approximation of the natural numbers. And their image as lifted by+-- @-XDataKinds@ corresponds to the actual natural numbers.+data Nat = Z | S !Nat++-- | A partial relation that gives the index of a value in a list.+type family RIndex (r :: k) (rs :: [k]) :: Nat where+  RIndex r (r ': rs) = Z+  RIndex r (s ': rs) = S (RIndex r rs)++-- | A partial relation that gives the indices of a sublist in a larger list.+type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where+  RImage '[] ss = '[]+  RImage (r ': rs) ss = RIndex r ss ': RImage rs ss++-- | A constraint-former which applies to every field in a record.+type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where+  RecAll f '[] c = ()+  RecAll f (r ': rs) c = (c (f r), RecAll f rs c)++-- | Append for type-level lists.+type family (as :: [k]) ++ (bs :: [k]) :: [k] where+  '[] ++ bs = bs+  (a ': as) ++ bs = a ': (as ++ bs)+
− Data/Vinyl/Universe.hs 
@@ -1,7 +0,0 @@-module Data.Vinyl.Universe-  ( module Data.Vinyl.Universe.Id-  , module Data.Vinyl.Universe.Field-  ) where--import Data.Vinyl.Universe.Id-import Data.Vinyl.Universe.Field
− Data/Vinyl/Universe/Const.hs 
@@ -1,13 +0,0 @@-{-# LANGUAGE DataKinds    #-}-{-# LANGUAGE GADTs        #-}-{-# LANGUAGE PolyKinds    #-}-{-# LANGUAGE TypeFamilies #-}--module Data.Vinyl.Universe.Const (Const(..)) where--import Data.Vinyl.TyFun--data Const :: * -> (TyFun k *) -> * where-  Const :: Const t el--type instance App (Const t) x = t
− Data/Vinyl/Universe/Field.hs 
@@ -1,26 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds     #-}-{-# LANGUAGE GADTs         #-}-{-# LANGUAGE PolyKinds     #-}-{-# LANGUAGE TypeFamilies  #-}-{-# LANGUAGE TypeOperators #-}--module Data.Vinyl.Universe.Field where--import Data.Vinyl.TyFun-import GHC.TypeLits--data (sy :: k) ::: (t :: *)--#if __GLASGOW_HASKELL__ > 707-data SField :: * -> * where-  SField :: KnownSymbol sy => SField (sy ::: t)-#else-data SField :: * -> * where-  SField :: SingE (Kind :: Symbol) str => SField (sy ::: t)-#endif--data ElField :: (TyFun * *) -> * where-  ElField :: ElField el-type instance App ElField (sy ::: t) = t
− Data/Vinyl/Universe/Id.hs 
@@ -1,13 +0,0 @@-{-# LANGUAGE DataKinds    #-}-{-# LANGUAGE GADTs        #-}-{-# LANGUAGE PolyKinds    #-}-{-# LANGUAGE TypeFamilies #-}--module Data.Vinyl.Universe.Id (Id(..)) where--import Data.Vinyl.TyFun--data Id :: (TyFun k k) -> * where-  Id :: Id el-type instance App Id x = x-
− Data/Vinyl/Witnesses.hs 
@@ -1,29 +0,0 @@-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE GADTs                 #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE OverlappingInstances  #-}-{-# LANGUAGE PolyKinds             #-}-{-# LANGUAGE TypeOperators         #-}--module Data.Vinyl.Witnesses where--class Implicit p where-  implicitly :: p---- | An inductive list membership proposition.-data Elem :: k -> [k] -> * where-  Here  :: Elem x (x ': xs)-  There :: Elem x xs -> Elem x (y ': xs)---- | A constraint for implicit resolution of list membership proofs.-type IElem x xs = Implicit (Elem x xs)-type x ∈ xs = IElem x xs--instance Implicit (Elem x (x ': xs)) where-  implicitly = Here-instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where-  implicitly = There implicitly-
tests/Intro.lhs view
@@ -19,17 +19,12 @@  > {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-} > {-# LANGUAGE FlexibleContexts, FlexibleInstances, NoMonomorphismRestriction #-}-> {-# LANGUAGE GADTs, TemplateHaskell, TypeSynonymInstances #-}+> {-# LANGUAGE GADTs, TypeSynonymInstances, TemplateHaskell, StandaloneDeriving #-} > import Data.Vinyl-> import Data.Vinyl.TyFun-> import Data.Vinyl.TH > import Data.Vinyl.Functor-> import Data.Vinyl.Idiom.Identity-> import Data.Vinyl.Idiom.Validation-> import Data.Vinyl.Witnesses-> import qualified Data.Vinyl.Universe.Const as U > import Control.Applicative > import Control.Lens hiding (Identity)+> import Control.Lens.TH > import Data.Char > import Test.DocTest > import Data.Singletons.TH@@ -37,51 +32,47 @@ Let’s define a universe of fields which we want to use:  > data Fields = Name | Age | Sleeping | Master deriving Show-> genSingletons [ ''Fields ]-> makeUniverse' ''Fields "ElF"-> semantics ''ElF [ 'Name     :~> ''String->                 , 'Age      :~> ''Int->                 , 'Sleeping :~> ''Bool->                 ]--Now, let’s try to make an entity that represents a man:--> jon = SName =: "jon"->    <+> SAge =: 20->    <+> SSleeping =: False+> type LifeForm = [Name, Age, Sleeping] +> type family ElF (f :: Fields) :: * where+>   ElF Name = String+>   ElF Age = Int+>   ElF Sleeping = Bool+>   ElF Master = Rec Attr LifeForm -We could make an alias for the sort of entity that jon is:+> newtype Attr f = Attr { _unAttr :: ElF f }+> makeLenses ''Attr+> 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 -> type LifeForm = [Name, Age, Sleeping]-> jon :: PlainRec ElF LifeForm+> (=:) :: sing f -> ElF f -> Attr f+> _ =: x = Attr x -We can print out the record by assigning names to each field:+> genSingletons [ ''Fields ] -> instance Implicit (PlainRec (U.Const String) [ Name, Age, Sleeping ]) where->   implicitly = SName     =: "name"->            <+> SAge      =: "age"->            <+> SSleeping =: "sleeping"+Now, let’s try to make an entity that represents a man: -> -- | >>> rshow jon-> -- "{ name =: \"jon\", age =: 20, sleeping =: False }"+> jon = (SName =: "jon")+>    :& (SAge =: 23)+>    :& (SSleeping =: False)+>    :& RNil -The types are inferred, though, so this is unnecessary unless you’d-like to reuse the type later. Now, make a dog! Dogs are life-forms,-but unlike men, they have masters. So, let’s build my dog:+Automatically, we can show the record: -> semantics ''ElF [ 'Master :~> [t| PlainRec ElF LifeForm |] ]+> -- |+> -- >>> show jon+> -- "{name: \"jon\"; age: 23; sleeping: False}" -> tucker = withUniverse ElF $->   SName =: "tucker"->   <+> SAge =: 7->   <+> SSleeping =: True->   <+> SMaster =: jon+And its types are all inferred with no problem. Now, make a dog! Dogs are+life-forms, but unlike men, they have masters. So, let’s build my dog: -It was necessary to specify the interpreter for the universe in which `tucker`-lives, since (lacking a type annotation), records constructed using `(<+>)` and-`(=:)` are polymorphic with respect to `el`. We can help along the type-inference by giving it explicitly using `withUniverse`.+> tucker = (SName =: "tucker")+>       :& (SAge =: 9)+>       :& (SSleeping =: True)+>       :& (SMaster =: jon)+>       :& RNil  Using Lenses ------------@@ -92,9 +83,10 @@ on a particular field in the record for access and update, without losing additional information: -> wakeUp :: (Sleeping ∈ fields) => PlainRec ElF fields -> PlainRec ElF fields-> wakeUp = SSleeping `rPut` False +> wakeUp :: (Sleeping ∈ fields) => Rec Attr fields -> Rec Attr fields+> wakeUp = rput $ SSleeping =: False+ Now, the type annotation on wakeUp was not necessary; I just wanted to show how intuitive the type is. Basically, it takes as an input any record that has a `Bool` field labelled `sleeping`, and modifies that@@ -104,34 +96,29 @@ > jon' = wakeUp jon  > -- |-> -- >>> tucker' ^. rLens SSleeping-> -- False+> -- >>> tucker' ^. rlens SSleeping+> -- sleeping: False > ---> -- >>> tucker ^. rLens SSleeping-> -- True+> -- >>> tucker ^. rlens SSleeping+> -- sleeping: True > ---> -- >>> jon' ^. rLens SSleeping-> -- False+> -- >>> jon' ^. rlens SSleeping+> -- sleeping: False  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: -> masterSleeping :: (Master ∈ fields) => Lens' (PlainRec ElF fields) Bool-> masterSleeping = rLens SMaster . rLens SSleeping-> tucker'' = masterSleeping .~ True $ tucker'-+> masterSleeping = rlens SMaster . unAttr . rlens SSleeping+> tucker'' = masterSleeping .~ (SSleeping =: True) $ tucker'  > -- | >>> tucker'' ^. masterSleeping-> -- True--Again, the type annotation is unnecessary.-+> -- sleeping: True  Subtyping Relation and Coercion ------------------------------- -A record `PlainRec xs` is a subtype of a record `PlainRec ys` if `ys ⊆ xs`;+A record `Rec f xs` is a subtype of a record `Rec f ys` if `ys ⊆ xs`; 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@@ -140,73 +127,80 @@  Therefore, the following works: -> upcastedTucker :: PlainRec ElF LifeForm-> upcastedTucker = cast (toPlainRec tucker)--The reason for using `toPlainRec` will become clear a bit later.+> upcastedTucker :: Rec Attr LifeForm+> upcastedTucker = rcast tucker  The subtyping relationship between record types is expressed with the `(<:)` constraint; so, cast is of the following type: -< cast :: r1 <: r2 => Rec r1 f -> Rec r2 f+< rcast :: r1 <: r2 => Rec f r1 -> Rec f r2  Also provided is a `(≅)` constraint which indicates record congruence (that is, two record types differ only in the order of their fields). +In fact, `rcast` is actually given as a special case of the lens `rsubset`,+which lets you modify entire (possibly non-contiguous) slices of a record!+ Records are polymorphic over functors ------------------------------------- -So far, we’ve been working with the `PlainRec` type; but below that,-there is something a bit more advanced called `Rec`, which looks like-this:+Consider the following declaration: -< data Rec :: (TyFun u * -> *) -> (* -> *) -> [u] -> * where-<   RNil :: Rec el f '[]-<   (:&) :: f (el $ r) -> Rec el f rs -> Rec el f (r ': rs)+< data Rec :: (u -> *) -> [u] -> * where+<   RNil :: Rec f '[]+<   (:&) :: f r -> Rec f rs -> Rec f (r ': rs) -The second parameter is a functor, in which every element of the-record will be placed. In `PlainRec`, the functor is just set to-`Identity`. Let’s try and motivate this stuff with an example.+Records are implicitly parameterized over a kind `u`, which stands for the+"universe" or key space. Keys (inhabitants of `u`) are then interpreted into+the types of their values by the first parameter to `Rec`, `f`. An extremely+powerful aspect of Vinyl records is that you can construct natural+transformations between different interpretation functors `f,g`, 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:  > type Person = [Name, Age] -We’ve decided that names must be alphabetic, and ages must be-positive. For validation, we’ll use a type that’s included here called-`Result e a`, which is similar to `Either`, except that its-`Applicative` instance accumulates monoidal errors on the left.+We’ve decided that names must be alphabetic, and ages must be positive. For+validation, we’ll use `Maybe` for now, though you should use a+left-accumulating `Validation` type. -> goodPerson :: PlainRec ElF Person-> goodPerson = SName =: "Jon"->          <+> SAge  =: 20-> badPerson = SName =: "J#@#$on"->         <+> SAge  =: 20+> goodPerson :: Rec Attr Person+> goodPerson = (SName =: "Jon")+>           :& (SAge =: 20)+>           :& RNil -> validatePerson :: PlainRec ElF Person -> Result [String] (PlainRec ElF Person)-> validatePerson p = (\n a -> SName =: n <+> SAge =: a) <$> vName <*> vAge where->   vName = validateName (rGet SName p)->   vAge  = validateAge  (rGet SAge p)+> badPerson = (SName =: "J#@#$on")+>           :& (SAge =: 20)+>           :& RNil++We'll give validation a (rather poor) shot.++> validatePerson :: Rec Attr Person -> Maybe (Rec Attr Person)+> validatePerson p = (\n a -> (SName =: n) :& (SAge =: a) :& RNil) <$> vName <*> vAge where+>   vName = validateName $ p ^. rlens SName . unAttr+>   vAge  = validateAge $ p ^. rlens SAge . unAttr >->   validateName str | all isAlpha str = Success str->   validateName _ = Failure [ "name must be alphabetic" ]->   validateAge i | i >= 0 = Success i->   validateAge _ = Failure [ "age must be positive" ]+>   validateName str | all isAlpha str = Just str+>   validateName _ = Nothing+>   validateAge i | i >= 0 = Just i+>   validateAge _ = Nothing  > -- $setup-> -- >>> let isSuccess (Success _) = True; isSuccess _ = False+> -- >>> let isJust (Just _) = True; isJust _ = False  > -- |-> -- >>> isSuccess $ validatePerson goodPerson+> -- >>> isJust $ validatePerson goodPerson > -- True > ---> -- >>> isSuccess $ validatePerson badPerson+> -- >>> isJust $ validatePerson badPerson > -- False -The results are as expected (`Success` for `goodPerson`, and a-`Failure` with one error for `badPerson`); but this was not very fun-to build.+The results are as expected (`Just` for `goodPerson`, and a `Nothing` for+`badPerson`); 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@@ -215,21 +209,19 @@ 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. -Vinyl provides a type of validators, which is the class of functions from the-`Identity` functor to the `Result` functor at some type.--< type Validator e = Lift (->) Identity ~> Result e+> type Validator f = Lift (->) f (Maybe :. f)  Let’s parameterize a record by it: when we do, then an element of type `a` should be a function `Identity a -> Result e a`: -> vperson :: Rec ElF (Validator [String]) Person-> vperson = Lift validateName :& Lift validateAge :& RNil where->    validateName (Identity str) | all isAlpha str = Success str->    validateName _ = Failure [ "name must be alphabetic" ]->    validateAge (Identity i) | i >= 0 = Success i->    validateAge _ = Failure [ "age must be positive" ]-+> vperson :: Rec (Validator Attr) Person+> vperson = lift validateName :& lift validateAge :& RNil+>   where+>     lift f = Lift $ Compose . f+>     validateName (Attr str) | all isAlpha str = Just (Attr str)+>     validateName _ = Nothing+>     validateAge (Attr i) | i >= 0 = Just (Attr i)+>     validateAge _ = Nothing  And we can use the special application operator `<<*>>` (which is analogous to `<*>`, but generalized a bit) to use this to validate a@@ -238,56 +230,31 @@ > goodPersonResult = vperson <<*>> goodPerson > badPersonResult  = vperson <<*>> badPerson -< goodPersonResult === SName :=: Success "Jon", SAge :=: Success 20, {}-< badPersonResult  === SName :=: Failure ["name must be alphabetic"], SAge :=: Success 20, {}- > -- |-> -- >>> isSuccess $ goodPersonResult ^. rLens' SName+> -- >>> isJust . getCompose $ goodPersonResult ^. rlens SName > -- True-> -- >>> isSuccess $ goodPersonResult ^. rLens' SAge+> -- >>> isJust . getCompose $ goodPersonResult ^. rlens SAge > -- True-> -- >>> isSuccess $ badPersonResult ^. rLens' SName+> -- >>> isJust . getCompose $ badPersonResult ^. rlens SName > -- False-> -- >>> isSuccess $ badPersonResult ^. rLens' SAge+> -- >>> isJust . getCompose $ badPersonResult ^. rlens SAge > -- True -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 `Result [String]-(PlainRec Person)`) using `rdist`: -> distGoodPerson = rdist goodPersonResult-> distBadPerson  = rdist badPersonResult+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 `Maybe (Rec Attr Person)`) using `rtraverse`: -< distGoodPerson === Success name :=: "Jon", age :=: 20, {}-< distBadPerson  === Failure ["name must be alphabetic"]+> mgoodPerson :: Maybe (Rec Attr Person)+> mgoodPerson = rtraverse getCompose goodPersonResult +> mbadPerson  = rtraverse getCompose badPersonResult+ > -- |-> -- >>> isSuccess distGoodPerson+> -- >>> isJust mgoodPerson > -- True-> -- >>> isSuccess distBadPerson+> -- >>> isJust mbadPerson > -- False -Fixing a polymorphic record into the Identity Functor--------------------------------------------------------If you produced a record using `(=:)` and `(<+>)` without providing a-type annotation, then its type is something like this:--< record :: Applicative f => Rec el f [ <bunch of stuff> ]--The problem is then we can’t do anything with the record that requires-us to know what its functor is. For instance, `cast` will fail. So, we-might try to provide a type annotation, but that can be a bit brittle-and frustrating to have to do. To alleviate this problem, `toPlainRec` is-provided:--< toPlainRec :: (forall f. Applicative f => Rec el f rs) -> PlainRec el rs-------(We must define a main value for doctest to run.)- > main :: IO () > main = doctest ["tests/Intro.lhs"]-
vinyl.cabal view
@@ -1,5 +1,5 @@ name:                vinyl-version:             0.4.3+version:             0.5 synopsis:            Extensible Records -- description: license:             MIT@@ -21,23 +21,12 @@ library   exposed-modules:     Data.Vinyl                      , Data.Vinyl.Core-                     , Data.Vinyl.Operators                      , Data.Vinyl.Lens                      , Data.Vinyl.Derived-                     , Data.Vinyl.Witnesses-                     , Data.Vinyl.Constraint-                     , Data.Vinyl.Idiom.Validation-                     , Data.Vinyl.Idiom.Identity-                     , Data.Vinyl.Idiom.Thunk-                     , Data.Vinyl.TyFun+                     , Data.Vinyl.TypeLevel                      , Data.Vinyl.Functor                      , Data.Vinyl.Notation-                     , Data.Vinyl.Universe-                     , Data.Vinyl.Universe.Id-                     , Data.Vinyl.Universe.Const-                     , Data.Vinyl.Universe.Field-                     , Data.Vinyl.TH-  build-depends:       base >=4.6 && <= 5, ghc-prim, template-haskell >= 2.7.0.0+  build-depends:       base >=4.7 && <= 5, ghc-prim   default-language:    Haskell2010   ghc-options: -fwarn-dodgy-exports -fwarn-dodgy-imports -fwarn-unused-matches -fwarn-unused-imports -fwarn-unused-binds -fwarn-incomplete-record-updates -fwarn-missing-signatures -fwarn-name-shadowing -fwarn-orphans -fwarn-overlapping-patterns -fwarn-tabs -fwarn-type-defaults @@ -45,7 +34,7 @@   type:             exitcode-stdio-1.0   hs-source-dirs:   benchmarks   main-is:          StorableBench.hs-  build-depends:    base >= 4.6 && <= 5, vector, criterion, vinyl == 0.4.3, mwc-random, lens, linear+  build-depends:    base >= 4.7 && <= 5, vector, criterion, vinyl == 0.5, mwc-random, lens, linear   ghc-options:      -O2 -fllvm   default-language: Haskell2010 @@ -53,5 +42,5 @@   type:             exitcode-stdio-1.0   hs-source-dirs:   tests   main-is:          Intro.lhs-  build-depends:    base >= 4.6 && <= 5, lens, vinyl == 0.4.3, doctest >= 0.8, singletons >= 0.10+  build-depends:    base >= 4.7 && <= 5, lens, vinyl == 0.5, doctest >= 0.8, singletons >= 0.10   default-language: Haskell2010