{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Core vinyl definitions. The 'Rec' data type is defined here, but -- also of interest are definitions commonly used functions like -- 'rmap', 'rapply', and 'rtraverse'. -- -- The definitions in this module are written in terms of type classes -- so that the definitions may be specialized to each record type at -- which they are used. This usually helps with runtime performance, -- but can slow down compilation time. If you are experiencing poor -- compile times, you may wish to try the semantically equivalent -- definitions in the "Data.Vinyl.Recursive" module: they should -- produce the same results given the same inputs as functions defined -- in this module, but they will not be specialized to your record -- type. Instead, they treat the record as a list of fields, so will -- have performance linear in the size of the record. module Data.Vinyl.Core where import Data.Monoid (Monoid) import Data.Semigroup import Foreign.Ptr (castPtr, plusPtr) import Foreign.Storable (Storable(..)) import Data.Vinyl.Functor import Data.List (intercalate) import Data.Vinyl.TypeLevel import Data.Type.Equality (TestEquality (..), (:~:) (..)) import Data.Type.Coercion (TestCoercion (..), Coercion (..)) -- | 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 7 :& infixr 5 <+> infixl 8 <<$>> infixl 8 <<*>> instance TestEquality f => TestEquality (Rec f) where testEquality RNil RNil = Just Refl testEquality (x :& xs) (y :& ys) = do Refl <- testEquality x y Refl <- testEquality xs ys Just Refl testEquality _ _ = Nothing instance TestCoercion f => TestCoercion (Rec f) where testCoercion RNil RNil = Just Coercion testCoercion (x :& xs) (y :& ys) = do Coercion <- testCoercion x y Coercion <- testCoercion xs ys Just Coercion testCoercion _ _ = Nothing -- | 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) -- | A shorthand for 'rappend'. (<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs) (<+>) = rappend -- | '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@. class RMap rs where rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs instance RMap '[] where rmap _ RNil = RNil {-# INLINE rmap #-} instance RMap xs => RMap (x ': xs) where rmap f (x :& xs) = f x :& rmap f xs {-# INLINE rmap #-} -- | A shorthand for 'rmap'. (<<$>>) :: RMap rs => (forall x. f x -> g x) -> Rec f rs -> Rec g rs (<<$>>) = rmap {-# INLINE (<<$>>) #-} -- | An inverted shorthand for 'rmap'. (<<&>>) :: RMap rs => 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@. class RApply rs where rapply :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs instance RApply '[] where rapply _ RNil = RNil {-# INLINE rapply #-} instance RApply xs => RApply (x ': xs) where rapply (f :& fs) (x :& xs) = getLift f x :& (fs `rapply` xs) {-# INLINE rapply #-} -- | A shorthand for 'rapply'. (<<*>>) :: RApply rs => 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 {-# INLINABLE rtraverse #-} -- | Given a natural transformation from the product of @f@ and @g@ to @h@, we -- have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to -- @'Rec' h@. You can also think about this operation as zipping two records -- with the same element types but different interpretations. class RZipWith xs where rzipWith :: (forall x . f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs instance RZipWith '[] where rzipWith _ RNil RNil = RNil {-# INLINE rzipWith #-} instance RZipWith xs => RZipWith (x ': xs) where rzipWith m (fa :& fas) (ga :& gas) = m fa ga :& rzipWith m fas gas {-# INLINE rzipWith #-} -- | Map each element of a record to a monoid and combine the results. class RFoldMap rs where rfoldMapAux :: Monoid m => (forall x. f x -> m) -> m -> Rec f rs -> m instance RFoldMap '[] where rfoldMapAux _ m RNil = m {-# INLINE rfoldMapAux #-} instance RFoldMap xs => RFoldMap (x ': xs) where rfoldMapAux f m (r :& rs) = rfoldMapAux f (mappend m (f r)) rs {-# INLINE rfoldMapAux #-} rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs) => (forall x. f x -> m) -> Rec f rs -> m rfoldMap f = rfoldMapAux f mempty {-# INLINE rfoldMap #-} -- | A record with uniform fields may be turned into a list. class RecordToList rs where recordToList :: Rec (Const a) rs -> [a] instance RecordToList '[] where recordToList RNil = [] {-# INLINE recordToList #-} instance RecordToList xs => RecordToList (x ': xs) where recordToList (x :& xs) = getConst x : recordToList xs {-# INLINE recordToList #-} -- | 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. class ReifyConstraint c f rs where reifyConstraint :: Rec f rs -> Rec (Dict c :. f) rs instance ReifyConstraint c f '[] where reifyConstraint RNil = RNil {-# INLINE reifyConstraint #-} instance (c (f x), ReifyConstraint c f xs) => ReifyConstraint c f (x ': xs) where reifyConstraint (x :& xs) = Compose (Dict x) :& reifyConstraint xs {-# INLINE reifyConstraint #-} -- | Build a record whose elements are derived solely from a -- constraint satisfied by each. class RPureConstrained c ts where rpureConstrained :: (forall a. c a => f a) -> Rec f ts instance RPureConstrained c '[] where rpureConstrained _ = RNil {-# INLINE rpureConstrained #-} instance (c x, RPureConstrained c xs) => RPureConstrained c (x ': xs) where rpureConstrained f = f :& rpureConstrained @c @xs f {-# INLINE rpureConstrained #-} -- | Build a record whose elements are derived solely from a -- list of constraint constructors satisfied by each. class RPureConstraints cs ts where rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts instance RPureConstraints cs '[] where rpureConstraints _ = RNil {-# INLINE rpureConstraints #-} instance (AllSatisfied cs t, RPureConstraints cs ts) => RPureConstraints cs (t ': ts) where rpureConstraints f = f :& rpureConstraints @cs @ts f {-# INLINE rpureConstraints #-} -- | Records may be shown insofar as their points may be shown. -- 'reifyConstraint' is used to great effect here. instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs) where show xs = (\str -> "{" <> str <> "}") . intercalate ", " . recordToList . rmap (\(Compose (Dict x)) -> Const $ show x) $ reifyConstraint @Show xs instance Semigroup (Rec f '[]) where RNil <> RNil = RNil instance (Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs)) where (x :& xs) <> (y :& ys) = (x <> y) :& (xs <> ys) instance Monoid (Rec f '[]) where mempty = RNil RNil `mappend` RNil = RNil instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where mempty = mempty :& mempty (x :& xs) `mappend` (y :& ys) = (mappend x y) :& (mappend xs ys) instance Eq (Rec f '[]) where _ == _ = True instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where (x :& xs) == (y :& ys) = (x == y) && (xs == ys) instance Ord (Rec f '[]) where compare _ _ = EQ instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where compare (x :& xs) (y :& ys) = mappend (compare x y) (compare xs ys) instance Storable (Rec f '[]) where sizeOf _ = 0 alignment _ = 0 peek _ = return RNil poke _ RNil = return () instance (Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) where sizeOf _ = sizeOf (undefined :: f r) + sizeOf (undefined :: Rec f rs) {-# INLINE sizeOf #-} alignment _ = alignment (undefined :: f r) {-# INLINE alignment #-} peek ptr = do !x <- peek (castPtr ptr) !xs <- peek (ptr `plusPtr` sizeOf (undefined :: f r)) return $ x :& xs {-# INLINE peek #-} poke ptr (!x :& xs) = poke (castPtr ptr) x >> poke (ptr `plusPtr` sizeOf (undefined :: f r)) xs {-# INLINE poke #-}