{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Strict variant of SOP -- -- This does not currently attempt to be exhaustive. module Data.SOP.Strict ( -- * NP NP (..) , hd , singletonNP , tl -- * NS , NS (..) , index_NS , unZ -- * Injections , Injection , injections -- * Re-exports from @sop-core@ , module Data.SOP , module Data.SOP.Constraint ) where import Data.Coerce import Data.Kind (Type) import NoThunks.Class (NoThunks (..), allNoThunks) import Data.SOP hiding (Injection, NP (..), NS (..), hd, injections, shiftInjection, tl, unZ) import Data.SOP.Classes (Same) import Data.SOP.Constraint {------------------------------------------------------------------------------- NP -------------------------------------------------------------------------------} data NP :: (k -> Type) -> [k] -> Type where Nil :: NP f '[] (:*) :: !(f x) -> !(NP f xs) -> NP f (x ': xs) infixr 5 :* type instance CollapseTo NP a = [a] type instance AllN NP c = All c type instance AllZipN NP c = AllZip c type instance Prod NP = NP type instance SListIN NP = SListI type instance Same NP = NP singletonNP :: f x -> NP f '[x] singletonNP :: f x -> NP f '[x] singletonNP f x fx = f x fx f x -> NP f '[] -> NP f '[x] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP f '[] forall k (f :: k -> *). NP f '[] Nil hd :: NP f (x ': xs) -> f x hd :: NP f (x : xs) -> f x hd (f x x :* NP f xs _) = f x f x x tl :: NP f (x ': xs) -> NP f xs tl :: NP f (x : xs) -> NP f xs tl (f x _ :* NP f xs xs) = NP f xs NP f xs xs ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs ap_NP NP (f -.-> g) xs Nil NP f xs Nil = NP g xs forall k (f :: k -> *). NP f '[] Nil ap_NP (Fn f x -> g x f :* NP (f -.-> g) xs fs) (f x x :* NP f xs xs) = f x -> g x f f x f x x g x -> NP g xs -> NP g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (f -.-> g) xs -> NP f xs -> NP g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NP f xs -> NP g xs ap_NP NP (f -.-> g) xs fs NP f xs NP f xs xs pure_NP :: SListI xs => (forall a. f a) -> NP f xs pure_NP :: (forall (a :: k). f a) -> NP f xs pure_NP = Proxy Top -> (forall (a :: k). Top a => f a) -> NP f xs forall k (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). All c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs cpure_NP (Proxy Top forall k (t :: k). Proxy t Proxy @Top) cpure_NP :: forall c xs proxy f. All c xs => proxy c -> (forall a. c a => f a) -> NP f xs cpure_NP :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs cpure_NP proxy c _ forall (a :: k). c a => f a f = SList xs -> NP f xs forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: All c xs' => SList xs' -> NP f xs' go :: SList xs' -> NP f xs' go SList xs' SNil = NP f xs' forall k (f :: k -> *). NP f '[] Nil go SList xs' SCons = f x forall (a :: k). c a => f a f f x -> NP f xs -> NP f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* SList xs -> NP f xs forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList collapse_NP :: NP (K a) xs -> [a] collapse_NP :: NP (K a) xs -> [a] collapse_NP = NP (K a) xs -> [a] forall k a (xs :: [k]). NP (K a) xs -> [a] go where go :: NP (K a) xs -> [a] go :: NP (K a) xs -> [a] go NP (K a) xs Nil = [] go (K a x :* NP (K a) xs xs) = a x a -> [a] -> [a] forall a. a -> [a] -> [a] : NP (K a) xs -> [a] forall k a (xs :: [k]). NP (K a) xs -> [a] go NP (K a) xs xs ctraverse'_NP :: forall c proxy xs f f' g. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) ctraverse'_NP :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) ctraverse'_NP proxy c _ forall (a :: k). c a => f a -> g (f' a) f = NP f xs -> g (NP f' xs) forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys) go where go :: All c ys => NP f ys -> g (NP f' ys) go :: NP f ys -> g (NP f' ys) go NP f ys Nil = NP f' '[] -> g (NP f' '[]) forall (f :: * -> *) a. Applicative f => a -> f a pure NP f' '[] forall k (f :: k -> *). NP f '[] Nil go (f x x :* NP f xs xs) = f' x -> NP f' xs -> NP f' (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) (:*) (f' x -> NP f' xs -> NP f' (x : xs)) -> g (f' x) -> g (NP f' xs -> NP f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f x -> g (f' x) forall (a :: k). c a => f a -> g (f' a) f f x x g (NP f' xs -> NP f' (x : xs)) -> g (NP f' xs) -> g (NP f' (x : xs)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> NP f xs -> g (NP f' xs) forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys) go NP f xs xs ctraverse__NP :: forall c proxy xs f g. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g () ctraverse__NP :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () ctraverse__NP proxy c _ forall (a :: k). c a => f a -> g () f = NP f xs -> g () forall (ys :: [k]). All c ys => NP f ys -> g () go where go :: All c ys => NP f ys -> g () go :: NP f ys -> g () go NP f ys Nil = () -> g () forall (f :: * -> *) a. Applicative f => a -> f a pure () go (f x x :* NP f xs xs) = f x -> g () forall (a :: k). c a => f a -> g () f f x x g () -> g () -> g () forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b *> NP f xs -> g () forall (ys :: [k]). All c ys => NP f ys -> g () go NP f xs xs traverse__NP :: forall xs f g. (SListI xs, Applicative g) => (forall a. f a -> g ()) -> NP f xs -> g () traverse__NP :: (forall (a :: k). f a -> g ()) -> NP f xs -> g () traverse__NP forall (a :: k). f a -> g () f = Proxy Top -> (forall (a :: k). Top a => f a -> g ()) -> NP f xs -> g () forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (g :: * -> *). (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () ctraverse__NP (Proxy Top forall k (t :: k). Proxy t Proxy @Top) forall (a :: k). f a -> g () forall (a :: k). Top a => f a -> g () f trans_NP :: AllZip c xs ys => proxy c -> (forall x y . c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP :: proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP proxy c _ forall (x :: k) (y :: k). c x y => f x -> g y _t NP f xs Nil = NP g ys forall k (f :: k -> *). NP f '[] Nil trans_NP proxy c p forall (x :: k) (y :: k). c x y => f x -> g y t (f x x :* NP f xs xs) = f x -> g (Head ys) forall (x :: k) (y :: k). c x y => f x -> g y t f x x g (Head ys) -> NP g (Tail ys) -> NP g (Head ys : Tail ys) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NP f xs -> NP g (Tail ys) forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *). AllZip c xs ys => proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP proxy c p forall (x :: k) (y :: k). c x y => f x -> g y t NP f xs xs coerce_NP :: forall f g xs ys . AllZip (LiftedCoercible f g) xs ys => NP f xs -> NP g ys coerce_NP :: NP f xs -> NP g ys coerce_NP = Proxy (LiftedCoercible f g) -> (forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y) -> NP f xs -> NP g ys forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *). AllZip c xs ys => proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP (Proxy (LiftedCoercible f g) forall k (t :: k). Proxy t Proxy @(LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y coerce instance HPure NP where hpure :: (forall (a :: k). f a) -> NP f xs hpure = (forall (a :: k). f a) -> NP f xs forall k (xs :: [k]) (f :: k -> *). SListI xs => (forall (a :: k). f a) -> NP f xs pure_NP hcpure :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs hcpure = proxy c -> (forall (a :: k). c a => f a) -> NP f xs forall k (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). All c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs cpure_NP instance HAp NP where hap :: Prod NP (f -.-> g) xs -> NP f xs -> NP g xs hap = Prod NP (f -.-> g) xs -> NP f xs -> NP g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NP f xs -> NP g xs ap_NP instance HCollapse NP where hcollapse :: NP (K a) xs -> CollapseTo NP a hcollapse = NP (K a) xs -> CollapseTo NP a forall k a (xs :: [k]). NP (K a) xs -> [a] collapse_NP instance HSequence NP where hctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) hctraverse' = proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) ctraverse'_NP htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) htraverse' = Proxy Top -> (forall (a :: k). Top a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> h f xs -> g (h f' xs) hctraverse' (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hsequence' :: NP (f :.: g) xs -> f (NP g xs) hsequence' = (forall (a :: k). (:.:) f g a -> f (g a)) -> NP (f :.: g) xs -> f (NP g xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, SListIN h xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs) htraverse' forall (a :: k). (:.:) f g a -> f (g a) forall l k (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp instance HTraverse_ NP where hctraverse_ :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (g :: * -> *). (All c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () ctraverse__NP htraverse_ :: (forall (a :: k). f a -> g ()) -> NP f xs -> g () htraverse_ = (forall (a :: k). f a -> g ()) -> NP f xs -> g () forall k (xs :: [k]) (f :: k -> *) (g :: * -> *). (SListI xs, Applicative g) => (forall (a :: k). f a -> g ()) -> NP f xs -> g () traverse__NP instance HTrans NP NP where htrans :: proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys htrans = proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *). AllZip c xs ys => proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NP f xs -> NP g ys trans_NP hcoerce :: NP f xs -> NP g ys hcoerce = NP f xs -> NP g ys forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZip (LiftedCoercible f g) xs ys => NP f xs -> NP g ys coerce_NP {------------------------------------------------------------------------------- NS -------------------------------------------------------------------------------} data NS :: (k -> Type) -> [k] -> Type where Z :: !(f x) -> NS f (x ': xs) S :: !(NS f xs) -> NS f (x ': xs) type instance CollapseTo NS a = a type instance AllN NS c = All c type instance Prod NS = NP type instance SListIN NS = SListI type instance Same NS = NS unZ :: NS f '[x] -> f x unZ :: NS f '[x] -> f x unZ (Z f x x) = f x f x x index_NS :: forall f xs . NS f xs -> Int index_NS :: NS f xs -> Int index_NS = Int -> NS f xs -> Int forall (ys :: [k]). Int -> NS f ys -> Int go Int 0 where go :: forall ys . Int -> NS f ys -> Int go :: Int -> NS f ys -> Int go !Int acc (Z f x _) = Int acc go !Int acc (S NS f xs x) = Int -> NS f xs -> Int forall (ys :: [k]). Int -> NS f ys -> Int go (Int acc Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) NS f xs x expand_NS :: SListI xs => (forall x. f x) -> NS f xs -> NP f xs expand_NS :: (forall (x :: k). f x) -> NS f xs -> NP f xs expand_NS = Proxy Top -> (forall (x :: k). Top x => f x) -> NS f xs -> NP f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS (Proxy Top forall k (t :: k). Proxy t Proxy @Top) cexpand_NS :: forall c proxy f xs. All c xs => proxy c -> (forall x. c x => f x) -> NS f xs -> NP f xs cexpand_NS :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS proxy c p forall (x :: k). c x => f x d = NS f xs -> NP f xs forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs' go where go :: forall xs'. All c xs' => NS f xs' -> NP f xs' go :: NS f xs' -> NP f xs' go (Z f x x) = f x x f x -> NP f xs -> NP f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* proxy c -> (forall (x :: k). c x => f x) -> NP f xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs hcpure proxy c p forall (x :: k). c x => f x d go (S NS f xs i) = f x forall (x :: k). c x => f x d f x -> NP f xs -> NP f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NS f xs -> NP f xs forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs' go NS f xs i ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS = NP (f -.-> g) xs -> NS f xs -> NS g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NS f xs -> NS g xs go where go :: NP (f -.-> g) xs -> NS f xs -> NS g xs go :: NP (f -.-> g) xs -> NS f xs -> NS g xs go ((-.->) f g x f :* NP (f -.-> g) xs _) (Z f x x) = g x -> NS g (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (g x -> NS g (x : xs)) -> g x -> NS g (x : xs) forall a b. (a -> b) -> a -> b $ (-.->) f g x -> f x -> g x forall k (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f g x f f x f x x go ((-.->) f g x _ :* NP (f -.-> g) xs fs) (S NS f xs xs) = NS g xs -> NS g (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS g xs -> NS g (x : xs)) -> NS g xs -> NS g (x : xs) forall a b. (a -> b) -> a -> b $ NP (f -.-> g) xs -> NS f xs -> NS g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NS f xs -> NS g xs go NP (f -.-> g) xs fs NS f xs NS f xs xs go NP (f -.-> g) xs Nil NS f xs x = case NS f xs x of {} collapse_NS :: NS (K a) xs -> a collapse_NS :: NS (K a) xs -> a collapse_NS = NS (K a) xs -> a forall k a (xs :: [k]). NS (K a) xs -> a go where go :: NS (K a) xs -> a go :: NS (K a) xs -> a go (Z (K a x)) = a x go (S NS (K a) xs xs) = NS (K a) xs -> a forall k a (xs :: [k]). NS (K a) xs -> a go NS (K a) xs xs ctraverse'_NS :: forall c proxy xs f f' g. (All c xs, Functor g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS proxy c _ forall (a :: k). c a => f a -> g (f' a) f = NS f xs -> g (NS f' xs) forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys) go where go :: All c ys => NS f ys -> g (NS f' ys) go :: NS f ys -> g (NS f' ys) go (Z f x x) = f' x -> NS f' (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f' x -> NS f' (x : xs)) -> g (f' x) -> g (NS f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f x -> g (f' x) forall (a :: k). c a => f a -> g (f' a) f f x x go (S NS f xs xs) = NS f' xs -> NS f' (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS f' xs -> NS f' (x : xs)) -> g (NS f' xs) -> g (NS f' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NS f xs -> g (NS f' xs) forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys) go NS f xs xs trans_NS :: forall proxy c f g xs ys. AllZip c xs ys => proxy c -> (forall x y . c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS :: proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS proxy c _ forall (x :: k) (y :: k). c x y => f x -> g y t = NS f xs -> NS g ys forall (xs' :: [k]) (ys' :: [k]). AllZip c xs' ys' => NS f xs' -> NS g ys' go where go :: AllZip c xs' ys' => NS f xs' -> NS g ys' go :: NS f xs' -> NS g ys' go (Z f x x) = g (Head ys') -> NS g (Head ys' : Tail ys') forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z (f x -> g (Head ys') forall (x :: k) (y :: k). c x y => f x -> g y t f x x) go (S NS f xs x) = NS g (Tail ys') -> NS g (Head ys' : Tail ys') forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS f xs -> NS g (Tail ys') forall (xs' :: [k]) (ys' :: [k]). AllZip c xs' ys' => NS f xs' -> NS g ys' go NS f xs x) -- TODO: @sop-core@ defines this in terms of @unsafeCoerce@. Currently we -- don't make much use of this function, so I prefer this more strongly -- typed version. coerce_NS :: forall f g xs ys. AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys coerce_NS :: NS f xs -> NS g ys coerce_NS = Proxy (LiftedCoercible f g) -> (forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y) -> NS f xs -> NS g ys forall k k (proxy :: (k -> k -> Constraint) -> *) (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZip c xs ys => proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS (Proxy (LiftedCoercible f g) forall k (t :: k). Proxy t Proxy @(LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y coerce instance HExpand NS where hexpand :: (forall (x :: k). f x) -> NS f xs -> Prod NS f xs hexpand = (forall (x :: k). f x) -> NS f xs -> Prod NS f xs forall k (xs :: [k]) (f :: k -> *). SListI xs => (forall (x :: k). f x) -> NS f xs -> NP f xs expand_NS hcexpand :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs hcexpand = proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs cexpand_NS instance HAp NS where hap :: Prod NS (f -.-> g) xs -> NS f xs -> NS g xs hap = Prod NS (f -.-> g) xs -> NS f xs -> NS g xs forall k (f :: k -> *) (g :: k -> *) (xs :: [k]). NP (f -.-> g) xs -> NS f xs -> NS g xs ap_NS instance HCollapse NS where hcollapse :: NS (K a) xs -> CollapseTo NS a hcollapse = NS (K a) xs -> CollapseTo NS a forall k a (xs :: [k]). NS (K a) xs -> a collapse_NS instance HSequence NS where hctraverse' :: proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) hctraverse' = proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *). (All c xs, Functor g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) ctraverse'_NS htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) htraverse' = Proxy Top -> (forall (a :: k). Top a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> h f xs -> g (h f' xs) hctraverse' (Proxy Top forall k (t :: k). Proxy t Proxy @Top) hsequence' :: NS (f :.: g) xs -> f (NS g xs) hsequence' = (forall (a :: k). (:.:) f g a -> f (g a)) -> NS (f :.: g) xs -> f (NS g xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (HSequence h, SListIN h xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs) htraverse' forall (a :: k). (:.:) f g a -> f (g a) forall l k (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp instance HTrans NS NS where htrans :: proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g ys htrans = proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g ys forall k k (proxy :: (k -> k -> Constraint) -> *) (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZip c xs ys => proxy c -> (forall (x :: k) (y :: k). c x y => f x -> g y) -> NS f xs -> NS g ys trans_NS hcoerce :: NS f xs -> NS g ys hcoerce = NS f xs -> NS g ys forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]). AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys coerce_NS {------------------------------------------------------------------------------- Injections -------------------------------------------------------------------------------} type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs) injections :: forall xs f. SListI xs => NP (Injection f xs) xs injections :: NP (Injection f xs) xs injections = SList xs -> NP (Injection f xs) xs forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList where go :: SList xs' -> NP (Injection f xs') xs' go :: SList xs' -> NP (Injection f xs') xs' go SList xs' SNil = NP (Injection f xs') xs' forall k (f :: k -> *). NP f '[] Nil go SList xs' SCons = (f x -> K (NS f (x : xs)) x) -> (-.->) f (K (NS f (x : xs))) x forall k (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn (NS f (x : xs) -> K (NS f (x : xs)) x forall k a (b :: k). a -> K a b K (NS f (x : xs) -> K (NS f (x : xs)) x) -> (f x -> NS f (x : xs)) -> f x -> K (NS f (x : xs)) x forall b c a. (b -> c) -> (a -> b) -> a -> c . f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z) (-.->) f (K (NS f (x : xs))) x -> NP (f -.-> K (NS f (x : xs))) xs -> NP (f -.-> K (NS f (x : xs))) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (forall (a :: k). Injection f xs a -> (-.->) f (K (NS f (x : xs))) a) -> NP (Injection f xs) xs -> NP (f -.-> K (NS f (x : xs))) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap forall (a :: k). Injection f xs a -> (-.->) f (K (NS f (x : xs))) a forall a (f :: a -> *) (xs :: [a]) (a :: a) (x :: a). Injection f xs a -> Injection f (x : xs) a shiftInjection (SList xs -> NP (Injection f xs) xs forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs' go SList xs forall k (xs :: [k]). SListI xs => SList xs sList) shiftInjection :: Injection f xs a -> Injection f (x ': xs) a shiftInjection :: Injection f xs a -> Injection f (x : xs) a shiftInjection (Fn f a -> K (NS f xs) a f) = (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a forall k (f :: k -> *) (g :: k -> *) (a :: k). (f a -> g a) -> (-.->) f g a Fn ((f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a) -> (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a forall a b. (a -> b) -> a -> b $ NS f (x : xs) -> K (NS f (x : xs)) a forall k a (b :: k). a -> K a b K (NS f (x : xs) -> K (NS f (x : xs)) a) -> (f a -> NS f (x : xs)) -> f a -> K (NS f (x : xs)) a forall b c a. (b -> c) -> (a -> b) -> a -> c . NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) S (NS f xs -> NS f (x : xs)) -> (f a -> NS f xs) -> f a -> NS f (x : xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . K (NS f xs) a -> NS f xs forall k a (b :: k). K a b -> a unK (K (NS f xs) a -> NS f xs) -> (f a -> K (NS f xs) a) -> f a -> NS f xs forall b c a. (b -> c) -> (a -> b) -> a -> c . f a -> K (NS f xs) a f {------------------------------------------------------------------------------- Instances -------------------------------------------------------------------------------} deriving instance All (Show `Compose` f) xs => Show (NS f xs) deriving instance All (Eq `Compose` f) xs => Eq (NS f xs) deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs) -- | Copied from sop-core -- -- Not derived, since derived instance ignores associativity info instance All (Show `Compose` f) xs => Show (NP f xs) where showsPrec :: Int -> NP f xs -> ShowS showsPrec Int _ NP f xs Nil = String -> ShowS showString String "Nil" showsPrec Int d (f x f :* NP f xs fs) = Bool -> ShowS -> ShowS showParen (Int d Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int 5) (ShowS -> ShowS) -> ShowS -> ShowS forall a b. (a -> b) -> a -> b $ Int -> f x -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int 5 Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) f x f ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> ShowS showString String " :* " ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> NP f xs -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int 5 NP f xs fs deriving instance All (Eq `Compose` f) xs => Eq (NP f xs) deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs) {------------------------------------------------------------------------------- NoThunks -------------------------------------------------------------------------------} instance All (Compose NoThunks f) xs => NoThunks (NS (f :: k -> Type) (xs :: [k])) where showTypeOf :: Proxy (NS f xs) -> String showTypeOf Proxy (NS f xs) _ = String "NS" wNoThunks :: Context -> NS f xs -> IO (Maybe ThunkInfo) wNoThunks Context ctxt = \case Z f x l -> Context -> f x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "Z" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) f x l S NS f xs r -> Context -> NS f xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "S" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) NS f xs r instance All (Compose NoThunks f) xs => NoThunks (NP (f :: k -> Type) (xs :: [k])) where showTypeOf :: Proxy (NP f xs) -> String showTypeOf Proxy (NP f xs) _ = String "NP" wNoThunks :: Context -> NP f xs -> IO (Maybe ThunkInfo) wNoThunks Context ctxt = \case NP f xs Nil -> Maybe ThunkInfo -> IO (Maybe ThunkInfo) forall (m :: * -> *) a. Monad m => a -> m a return Maybe ThunkInfo forall a. Maybe a Nothing f x x :* NP f xs xs -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo) allNoThunks [ Context -> f x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "fst" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) f x x , Context -> NP f xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks (String "snd" String -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) NP f xs xs ]