packages feed

vinyl 0.1.1.0 → 0.1.1.1

raw patch · 7 files changed

+54/−53 lines, 7 files

Files

Data/Vinyl/Classes.hs view
@@ -8,11 +8,15 @@ import           Control.Applicative import           Control.Monad.Identity +-- | This class is a generalized, but non-pointed version of 'Applicative'. This+-- is useful for types which range over functors rather than sets. class Apply (arr :: k -> k -> k) (f :: k -> *) where   (<<*>>) :: f (arr a b) -> f a -> f b +-- | To accumulate effects distributed over a data type, you 'run' it. class Run t where   run :: Applicative f => t f -> f (t Identity) +-- | '(~>)' is a morphism between functors. newtype (f ~> g) x = NT { runNT :: f x -> g x }
Data/Vinyl/Field.hs view
@@ -9,8 +9,10 @@  import           GHC.TypeLits --- A field is a symbol key and a type for its value.+-- | A field contains a key and a type. data (:::) :: Symbol -> * -> * where+  -- | A constructor is given to facilitate introducing fields from terms without+  -- type annotations.   Field :: sy ::: t  instance SingI sy => Show (sy ::: t) where
Data/Vinyl/Rec.hs view
@@ -28,76 +28,61 @@ import           Data.Vinyl.Field import           GHC.TypeLits --- A record is parameterized by a list of fields and a functor+-- | A record is parameterized by a list of fields and a functor -- to be applied to each of those fields. data Rec :: [*] -> (* -> *) -> * where+  -- | The empty record.   RNil :: Rec '[] f-  (:&) :: (r ~ (sy ::: t)) => f t -> Rec rs f -> Rec (r ': rs) f++  -- | Cons for records.+  (:&) :: f t -> Rec rs f -> Rec ((sy ::: t) ': rs) f infixr :& --- Fixes a polymorphic record into the identity functor.+-- | Fixes a polymorphic record into the 'Identity' functor. fixRecord :: (forall f. Applicative f => Rec rs f) -> PlainRec rs fixRecord xs = xs --- Fields of plain records are in the Identity functor.+-- | Fields of plain records are in the 'Identity' functor. type PlainRec rs = Rec rs Identity --- Appends records+-- | Append for records. (<+>) :: Rec as f -> Rec bs f -> Rec (as ++ bs) f RNil      <+> xs = xs (x :& xs) <+> ys =  x :& (xs <+> ys)-infixl 8 <+>+infixl 8  <+> --- Shorthand for a record with a single field+-- | Shorthand for a record with a single field. Lifts the field's+-- value into the chosen functor automatically. (=:) :: Applicative f => sy ::: t -> t -> Rec '[sy ::: t] f a =: b = pure b :& RNil --- Type level list append+-- | Append for type-level lists. type family (as :: [*]) ++ (bs :: [*]) :: [*] type instance '[] ++ bs = bs type instance (a ': as) ++ bs  = a ': (as ++ bs) --- Type Class Instances+ instance Show (Rec '[] f) where   show RNil = "{}"- instance (SingI sy, Show (g t), Show (Rec fs g)) => Show (Rec ((sy ::: t) ': fs) g) where-  show (x :& xs) = show (Field :: sy ::: t) ++ " :=: " ++ show x ++ ", " ++ show xs where+  show (x :& xs) = show (Field :: sy ::: t) ++ " :=: " ++ show x ++ ", " ++ show xs + instance Eq (Rec '[] f) where   _ == _ = True instance (Eq (g t), Eq (Rec fs g)) => Eq (Rec ((s ::: t) ': fs) g) where   (x :& xs) == (y :& ys) = (x == y) && (xs == ys) +-- | Records can be applied to each other. instance Apply (~>) (Rec rs) where   RNil <<*>> RNil = RNil   (f :& fs) <<*>> (x :& xs) = runNT f x :& (fs <<*>> xs) +-- | Records may be 'run' to accumulate the effects of their fields. instance Run (Rec rs) where   run RNil      = pure RNil   run (x :& xs) = (:&) <$> (pure <$> x) <*> run xs +-- | We provide a 'Show' instance for 'Identity'. instance Show a => Show (Identity a) where   show (Identity x) = show x---{--ex :: Rec Name Identity-ex = Identity "jon"-  :& Identity "sterling"-  :& Identity 20-  :& RNil--verifyFirst = NT $ \str -> Failure ["asdfadS"]-verifyLast = NT $ \str -> Failure ["uhoh"]-verifyAge = NT $ \_ -> Failure ["uhoh"]--ex2 :: Rec Name (Identity ~> Result [String])-ex2 = verifyFirst-    :& verifyLast-    :& verifyAge-    :& RNil--ex3 = ex2 <<*>> ex-ex4 = run ex3--}
Data/Vinyl/Relation.hs view
@@ -25,20 +25,20 @@  import           GHC.Prim             (Constraint) --- A subtyping relation+-- | A subtyping relation. class (IsSubtype r1 r2) => r1 <: r2 where   cast :: r1 -> r2 --- On record is a subtype of another if the fields of the latter are a+-- | One record is a subtype of another if the fields of the latter are a -- subset of the fields of the former. type family IsSubtype r1 r2 :: Constraint type instance IsSubtype (Rec ss f) (Rec ts f) = ISubset ts ss --- If two records types are subtypes of each other, that means that they+-- | 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+-- | Term-level record congruence. (~=) :: (Eq a, a :~: b) => a -> b -> Bool x ~= y = x == (cast y) @@ -50,7 +50,7 @@     where field = lookupField (implicitly :: Elem y xs) r  lookupField :: Elem x xs -> Rec xs f -> x-lookupField Here (_ :& _)       = Field+lookupField Here      (_ :& _)  = Field lookupField (There p) (_ :& xs) = lookupField p xs  rIso :: (r1 :~: r2) => SimpleIso r1 r2
Data/Vinyl/Validation.hs view
@@ -2,25 +2,30 @@  module Data.Vinyl.Validation where -import Data.Vinyl.Classes-import Control.Applicative-import Control.Monad.Identity-import Data.Monoid+import           Control.Applicative+import           Control.Monad.Identity+import           Data.Monoid+import           Data.Vinyl.Classes +-- | 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 = Identity ~> Result e  instance Functor (Result e) where-  fmap f (Success x) = Success (f x)+  fmap f (Success x) = Success $ f x   fmap f (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)+  (Success f) <*> (Success x)  = Success $ f x   (Failure e) <*> (Success x)  = Failure e   (Success f) <*> (Failure e)  = Failure e-  (Failure e) <*> (Failure e') = Failure (e <> e')+  (Failure e) <*> (Failure e') = Failure $ e <> e'
Data/Vinyl/Witnesses.hs view
@@ -13,18 +13,23 @@ class Implicit p where   implicitly :: p -type IElem x xs = Implicit (Elem x xs)+-- | An inductive list membership proposition. data Elem :: k -> [k] -> * where   Here  :: Elem x (x ': xs)   There :: Elem x xs -> Elem x (y ': xs) -type ISubset xs ys = Implicit (Subset xs ys)+-- | A constraint for implicit resolution of list membership proofs.+type IElem x xs = Implicit (Elem x xs)++-- | An inductive list subset relation. data Subset :: [k] -> [k] -> * where   SubsetNil  :: Subset '[] xs-  SubsetCons ::-    Elem x ys ->-    Subset xs ys ->-    Subset (x ': xs) ys+  SubsetCons :: Elem x ys+             -> Subset xs ys+             -> Subset (x ': xs) ys++-- | A constraint for implicit resolution of list subset proofs.+type ISubset xs ys = Implicit (Subset xs ys)  instance Implicit (Elem x (x ': xs)) where   implicitly = Here
vinyl.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                vinyl-version:             0.1.1.0+version:             0.1.1.1 synopsis:            Extensible Records -- description: license:             MIT