{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE CPP #-} #if __GLASGOW_HASKELL__ < 806 {-# LANGUAGE TypeInType #-} #endif -- | Recursive definitions of various core vinyl functions. These are -- simple definitions that put less strain on the compiler. They are -- expected to have slower run times, but faster compile times than -- the definitions in "Data.Vinyl.Core". module Data.Vinyl.Recursive where #if __GLASGOW_HASKELL__ < 806 import Data.Kind #endif import Data.Proxy (Proxy(..)) import Data.Vinyl.Core (rpure, RecApplicative, Rec(..), Dict(..)) import Data.Vinyl.Functor (Compose(..), (:.), Lift(..), Const(..)) import Data.Vinyl.TypeLevel -- | Two records may be pasted together. rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) rappend Rec f as RNil Rec f bs ys = Rec f bs Rec f (as ++ bs) ys rappend (f r x :& Rec f rs xs) Rec f bs ys = f r x f r -> Rec f (rs ++ bs) -> Rec f (r : (rs ++ bs)) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec f rs xs Rec f rs -> Rec f bs -> Rec f (rs ++ bs) forall k (f :: k -> *) (as :: [k]) (bs :: [k]). Rec f as -> Rec f bs -> Rec f (as ++ bs) `rappend` Rec f bs ys) -- | A shorthand for 'rappend'. (<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs) <+> :: Rec f as -> Rec f bs -> Rec f (as ++ bs) (<+>) = Rec f as -> Rec f bs -> Rec f (as ++ bs) forall k (f :: k -> *) (as :: [k]) (bs :: [k]). 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@. rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs rmap :: (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (x :: u). f x -> g x _ Rec f rs RNil = Rec g rs forall u (f :: u -> *). Rec f '[] RNil rmap forall (x :: u). f x -> g x η (f r x :& Rec f rs xs) = f r -> g r forall (x :: u). f x -> g x η f r x g r -> Rec g rs -> Rec g (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (x :: u). f x -> g x η (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (f :: u -> *) (g :: u -> *) (rs :: [u]). (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs `rmap` Rec f rs xs) {-# INLINE rmap #-} -- | A shorthand for 'rmap'. (<<$>>) :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs <<$>> :: (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs (<<$>>) = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (f :: u -> *) (g :: u -> *) (rs :: [u]). (forall (x :: u). 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 Rec f rs xs <<&>> :: Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs <<&>> forall (x :: u). f x -> g x f = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs forall u (f :: u -> *) (g :: u -> *) (rs :: [u]). (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs rmap forall (x :: u). f x -> g x f Rec f rs 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 :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs rapply Rec (Lift (->) f g) rs RNil Rec f rs RNil = Rec g rs forall u (f :: u -> *). Rec f '[] RNil rapply (Lift (->) f g r f :& Rec (Lift (->) f g) rs fs) (f r x :& Rec f rs xs) = Lift (->) f g r -> f r -> g r forall l l' (op :: l -> l' -> *) k (f :: k -> l) (g :: k -> l') (x :: k). Lift op f g x -> op (f x) (g x) getLift Lift (->) f g r f f r x g r -> Rec g rs -> Rec g (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (Rec (Lift (->) f g) rs fs Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs forall u (f :: u -> *) (g :: u -> *) (rs :: [u]). Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs `rapply` Rec f rs Rec f rs xs) {-# INLINE rapply #-} -- | A shorthand for 'rapply'. (<<*>>) :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs <<*>> :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs (<<*>>) = Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs forall u (f :: u -> *) (g :: u -> *) (rs :: [u]). Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs rapply {-# INLINE (<<*>>) #-} -- | 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 :: (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) rtraverse forall (x :: u). f x -> h (g x) _ Rec f rs RNil = Rec g '[] -> h (Rec g '[]) forall (f :: * -> *) a. Applicative f => a -> f a pure Rec g '[] forall u (f :: u -> *). Rec f '[] RNil rtraverse forall (x :: u). f x -> h (g x) f (f r x :& Rec f rs xs) = g r -> Rec g rs -> Rec g (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) (:&) (g r -> Rec g rs -> Rec g (r : rs)) -> h (g r) -> h (Rec g rs -> Rec g (r : rs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f r -> h (g r) forall (x :: u). f x -> h (g x) f f r x h (Rec g rs -> Rec g (r : rs)) -> h (Rec g rs) -> h (Rec g (r : rs)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]). Applicative h => (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs) rtraverse forall (x :: u). f x -> h (g x) f Rec f rs 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. rzipWith :: (forall x . f x -> g x -> h x) -> (forall xs . Rec f xs -> Rec g xs -> Rec h xs) rzipWith :: (forall (x :: u). f x -> g x -> h x) -> forall (xs :: [u]). Rec f xs -> Rec g xs -> Rec h xs rzipWith forall (x :: u). f x -> g x -> h x m = \Rec f xs r -> case Rec f xs r of Rec f xs RNil -> \Rec g xs RNil -> Rec h xs forall u (f :: u -> *). Rec f '[] RNil (f r fa :& Rec f rs fas) -> \(g r ga :& Rec g rs gas) -> f r -> g r -> h r forall (x :: u). f x -> g x -> h x m f r fa g r g r ga h r -> Rec h rs -> Rec h (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& (forall (x :: u). f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs forall u (f :: u -> *) (g :: u -> *) (h :: u -> *). (forall (x :: u). f x -> g x -> h x) -> forall (xs :: [u]). Rec f xs -> Rec g xs -> Rec h xs rzipWith forall (x :: u). f x -> g x -> h x m Rec f rs fas Rec g rs Rec g rs gas -- | 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 rfoldMap :: (forall (x :: u). f x -> m) -> Rec f rs -> m rfoldMap forall (x :: u). f x -> m f = m -> Rec f rs -> m forall (ss :: [u]). m -> Rec f ss -> m go m forall a. Monoid a => a mempty where go :: forall ss. m -> Rec f ss -> m go :: m -> Rec f ss -> m go !m m Rec f ss record = case Rec f ss record of Rec f ss RNil -> m m f r r :& Rec f rs rs -> m -> Rec f rs -> m forall (ss :: [u]). m -> Rec f ss -> m go (m -> m -> m forall a. Monoid a => a -> a -> a mappend m m (f r -> m forall (x :: u). f x -> m f f r r)) Rec f rs rs {-# INLINABLE go #-} {-# INLINE rfoldMap #-} -- | A record with uniform fields may be turned into a list. recordToList :: Rec (Const a) rs -> [a] recordToList :: Rec (Const a) rs -> [a] recordToList Rec (Const a) rs RNil = [] recordToList (Const a r x :& Rec (Const a) rs xs) = Const a r -> a forall a k (b :: k). Const a b -> a getConst Const a r x a -> [a] -> [a] forall a. a -> [a] -> [a] : Rec (Const a) rs -> [a] forall u a (rs :: [u]). Rec (Const a) rs -> [a] recordToList Rec (Const a) rs xs -- | 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 :: proxy c -> Rec f rs -> Rec (Dict c :. f) rs reifyConstraint proxy c prx Rec f rs rec = case Rec f rs rec of Rec f rs RNil -> Rec (Dict c :. f) rs forall u (f :: u -> *). Rec f '[] RNil (f r x :& Rec f rs xs) -> Dict c (f r) -> Compose (Dict c) f r forall l k (f :: l -> *) (g :: k -> l) (x :: k). f (g x) -> Compose f g x Compose (f r -> Dict c (f r) forall (c :: * -> Constraint) a. c a => a -> Dict c a Dict f r x) Compose (Dict c) f r -> Rec (Dict c :. f) rs -> Rec (Dict c :. f) (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& proxy c -> Rec f rs -> Rec (Dict c :. f) rs forall u (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) (proxy :: (* -> Constraint) -> *). RecAll f rs c => proxy c -> Rec f rs -> Rec (Dict c :. f) rs reifyConstraint proxy c prx Rec f rs xs -- | Build a record whose elements are derived solely from a -- constraint satisfied by each. rpureConstrained :: forall u c (f :: u -> *) proxy ts. (AllConstrained c ts, RecApplicative ts) => proxy c -> (forall a. c a => f a) -> Rec f ts rpureConstrained :: proxy c -> (forall (a :: u). c a => f a) -> Rec f ts rpureConstrained proxy c _ forall (a :: u). c a => f a f = Rec Proxy ts -> Rec f ts forall (ts' :: [u]). AllConstrained c ts' => Rec Proxy ts' -> Rec f ts' go ((forall (x :: u). Proxy x) -> Rec Proxy ts forall u (rs :: [u]) (f :: u -> *). RecApplicative rs => (forall (x :: u). f x) -> Rec f rs rpure forall (x :: u). Proxy x forall k (t :: k). Proxy t Proxy) where go :: AllConstrained c ts' => Rec Proxy ts' -> Rec f ts' go :: Rec Proxy ts' -> Rec f ts' go Rec Proxy ts' RNil = Rec f ts' forall u (f :: u -> *). Rec f '[] RNil go (Proxy r _ :& Rec Proxy rs xs) = f r forall (a :: u). c a => f a f f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rec Proxy rs -> Rec f rs forall (ts' :: [u]). AllConstrained c ts' => Rec Proxy ts' -> Rec f ts' go Rec Proxy rs xs -- | 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 rpureConstraints :: proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts rpureConstraints proxy cs _ forall a. AllSatisfied cs a => f a f = Rec Maybe ts -> Rec f ts forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts' go ((forall x. Maybe x) -> Rec Maybe ts forall u (rs :: [u]) (f :: u -> *). RecApplicative rs => (forall (x :: u). f x) -> Rec f rs rpure forall x. Maybe x Nothing) where go :: AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts' go :: Rec Maybe ts' -> Rec f ts' go Rec Maybe ts' RNil = Rec f ts' forall u (f :: u -> *). Rec f '[] RNil go (Maybe r _ :& Rec Maybe rs xs) = f r forall a. AllSatisfied cs a => f a f f r -> Rec f rs -> Rec f (r : rs) forall a (f :: a -> *) (r :: a) (rs :: [a]). f r -> Rec f rs -> Rec f (r : rs) :& Rec Maybe rs -> Rec f rs forall (ts' :: [*]). AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts' go Rec Maybe rs xs