generics-sop-0.5.1.4: Generic Programming using True Sums of Products
Safe HaskellNone
LanguageHaskell2010

Generics.SOP.Classes

Documentation

class HPure (h :: (k -> Type) -> l -> Type) where #

Methods

hpure :: forall (xs :: l) f. SListIN h xs => (forall (a :: k). f a) -> h f xs #

hcpure :: forall c (xs :: l) proxy f. AllN h c xs => proxy c -> (forall (a :: k). c a => f a) -> h f xs #

Instances

Instances details
HPure (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hpure :: forall (xs :: [[k]]) f. SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs => (forall (a :: k). f a) -> POP f xs #

hcpure :: forall c (xs :: [[k]]) proxy f. AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs => proxy c -> (forall (a :: k). c a => f a) -> POP f xs #

HPure (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hpure :: forall (xs :: [k]) f. SListIN (NP :: (k -> Type) -> [k] -> Type) xs => (forall (a :: k). f a) -> NP f xs #

hcpure :: forall c (xs :: [k]) proxy f. AllN (NP :: (k -> Type) -> [k] -> Type) c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs #

newtype ((f :: k -> Type) -.-> (g :: k -> Type)) (a :: k) #

Constructors

Fn 

Fields

  • apFn :: f a -> g a
     

Instances

Instances details
Generic ((f -.-> g) a) Source # 
Instance details

Defined in Generics.SOP.Instances

Associated Types

type Code ((f -.-> g) a) 
Instance details

Defined in Generics.SOP.Instances

type Code ((f -.-> g) a) = '['[f a -> g a]]

Methods

from :: (f -.-> g) a -> Rep ((f -.-> g) a) Source #

to :: Rep ((f -.-> g) a) -> (f -.-> g) a Source #

HasDatatypeInfo ((f -.-> g) a) Source # 
Instance details

Defined in Generics.SOP.Instances

Associated Types

type DatatypeInfoOf ((f -.-> g) a) 
Instance details

Defined in Generics.SOP.Instances

type DatatypeInfoOf ((f -.-> g) a) = 'Newtype "Data.SOP.Classes" "-.->" ('Record "Fn" '['FieldInfo "apFn"])

Methods

datatypeInfo :: proxy ((f -.-> g) a) -> DatatypeInfo (Code ((f -.-> g) a)) Source #

type Code ((f -.-> g) a) Source # 
Instance details

Defined in Generics.SOP.Instances

type Code ((f -.-> g) a) = '['[f a -> g a]]
type DatatypeInfoOf ((f -.-> g) a) Source # 
Instance details

Defined in Generics.SOP.Instances

type DatatypeInfoOf ((f -.-> g) a) = 'Newtype "Data.SOP.Classes" "-.->" ('Record "Fn" '['FieldInfo "apFn"])

fn :: forall {k} f (a :: k) f'. (f a -> f' a) -> (f -.-> f') a #

fn_2 :: forall {k} f (a :: k) f' f''. (f a -> f' a -> f'' a) -> (f -.-> (f' -.-> f'')) a #

fn_3 :: forall {k} f (a :: k) f' f'' f'''. (f a -> f' a -> f'' a -> f''' a) -> (f -.-> (f' -.-> (f'' -.-> f'''))) a #

fn_4 :: forall {k} f (a :: k) f' f'' f''' f''''. (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> (f' -.-> (f'' -.-> (f''' -.-> f'''')))) a #

type family Prod (h :: (k -> Type) -> l -> Type) :: (k -> Type) -> l -> Type #

Instances

Instances details
type Prod (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

type Prod (POP :: (k -> Type) -> [[k]] -> Type) = POP :: (k -> Type) -> [[k]] -> Type
type Prod (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

type Prod (SOP :: (k -> Type) -> [[k]] -> Type) = POP :: (k -> Type) -> [[k]] -> Type
type Prod (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

type Prod (NP :: (k -> Type) -> [k] -> Type) = NP :: (k -> Type) -> [k] -> Type
type Prod (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

type Prod (NS :: (k -> Type) -> [k] -> Type) = NP :: (k -> Type) -> [k] -> Type

class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h :: (k -> Type) -> l -> Type) where #

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: l). Prod h (f -.-> g) xs -> h f xs -> h g xs #

Instances

Instances details
HAp (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [[k]]). Prod (POP :: (k -> Type) -> [[k]] -> Type) (f -.-> g) xs -> POP f xs -> POP g xs #

HAp (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [[k]]). Prod (SOP :: (k -> Type) -> [[k]] -> Type) (f -.-> g) xs -> SOP f xs -> SOP g xs #

HAp (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [k]). Prod (NP :: (k -> Type) -> [k] -> Type) (f -.-> g) xs -> NP f xs -> NP g xs #

HAp (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hap :: forall (f :: k -> Type) (g :: k -> Type) (xs :: [k]). Prod (NS :: (k -> Type) -> [k] -> Type) (f -.-> g) xs -> NS f xs -> NS g xs #

hliftA :: forall {k} {l} h (xs :: l) f f'. (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs #

hliftA2 :: forall {k} {l} h (xs :: l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs #

hliftA3 :: forall {k} {l} h (xs :: l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs #

hcliftA :: forall {k} {l} h c (xs :: l) proxy f f'. (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs #

hcliftA2 :: forall {k} {l} h c (xs :: l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall (a :: k). c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs #

hcliftA3 :: forall {k} {l} h c (xs :: l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs #

hmap :: forall {k} {l} h (xs :: l) f f'. (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs #

hzipWith :: forall {k} {l} h (xs :: l) f f' f''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs #

hzipWith3 :: forall {k} {l} h (xs :: l) f f' f'' f'''. (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs #

hcmap :: forall {k} {l} h c (xs :: l) proxy f f'. (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs #

hczipWith :: forall {k} {l} h c (xs :: l) proxy f f' f''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall (a :: k). c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs #

hczipWith3 :: forall {k} {l} h c (xs :: l) proxy f f' f'' f'''. (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs #

type family UnProd (h :: (k -> Type) -> l -> Type) :: (k -> Type) -> l -> Type #

Instances

Instances details
type UnProd (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

type UnProd (POP :: (k -> Type) -> [[k]] -> Type) = SOP :: (k -> Type) -> [[k]] -> Type
type UnProd (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

type UnProd (NP :: (k -> Type) -> [k] -> Type) = NS :: (k -> Type) -> [k] -> Type

class UnProd (Prod h) ~ h => HApInjs (h :: (k -> Type) -> l -> Type) where #

Methods

hapInjs :: forall (xs :: l) (f :: k -> Type). SListIN h xs => Prod h f xs -> [h f xs] #

Instances

Instances details
HApInjs (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hapInjs :: forall (xs :: [[k]]) (f :: k -> Type). SListIN (SOP :: (k -> Type) -> [[k]] -> Type) xs => Prod (SOP :: (k -> Type) -> [[k]] -> Type) f xs -> [SOP f xs] #

HApInjs (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hapInjs :: forall (xs :: [k]) (f :: k -> Type). SListIN (NS :: (k -> Type) -> [k] -> Type) xs => Prod (NS :: (k -> Type) -> [k] -> Type) f xs -> [NS f xs] #

class HIndex (h :: (k -> Type) -> l -> Type) where #

Methods

hindex :: forall (f :: k -> Type) (xs :: l). h f xs -> Int #

Instances

Instances details
HIndex (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hindex :: forall (f :: k -> Type) (xs :: [[k]]). SOP f xs -> Int #

HIndex (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hindex :: forall (f :: k -> Type) (xs :: [k]). NS f xs -> Int #

type family CollapseTo (h :: (k -> Type) -> l -> Type) x #

Instances

Instances details
type CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a 
Instance details

Defined in Data.SOP.NP

type CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a = [[a]]
type CollapseTo (SOP :: (k -> Type) -> [[k]] -> Type) a 
Instance details

Defined in Data.SOP.NS

type CollapseTo (SOP :: (k -> Type) -> [[k]] -> Type) a = [a]
type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a 
Instance details

Defined in Data.SOP.NP

type CollapseTo (NP :: (k -> Type) -> [k] -> Type) a = [a]
type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a 
Instance details

Defined in Data.SOP.NS

type CollapseTo (NS :: (k -> Type) -> [k] -> Type) a = a

class HCollapse (h :: (k -> Type) -> l -> Type) where #

Methods

hcollapse :: forall (xs :: l) a. SListIN h xs => h (K a :: k -> Type) xs -> CollapseTo h a #

Instances

Instances details
HCollapse (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hcollapse :: forall (xs :: [[k]]) a. SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs => POP (K a :: k -> Type) xs -> CollapseTo (POP :: (k -> Type) -> [[k]] -> Type) a #

HCollapse (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hcollapse :: forall (xs :: [[k]]) a. SListIN (SOP :: (k -> Type) -> [[k]] -> Type) xs => SOP (K a :: k -> Type) xs -> CollapseTo (SOP :: (k -> Type) -> [[k]] -> Type) a #

HCollapse (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hcollapse :: forall (xs :: [k]) a. SListIN (NP :: (k -> Type) -> [k] -> Type) xs => NP (K a :: k -> Type) xs -> CollapseTo (NP :: (k -> Type) -> [k] -> Type) a #

HCollapse (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hcollapse :: forall (xs :: [k]) a. SListIN (NS :: (k -> Type) -> [k] -> Type) xs => NS (K a :: k -> Type) xs -> CollapseTo (NS :: (k -> Type) -> [k] -> Type) a #

class HTraverse_ (h :: (k -> Type) -> l -> Type) where #

Methods

hctraverse_ :: forall c (xs :: l) g proxy f. (AllN h c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> h f xs -> g () #

htraverse_ :: forall (xs :: l) g f. (SListIN h xs, Applicative g) => (forall (a :: k). f a -> g ()) -> h f xs -> g () #

Instances

Instances details
HTraverse_ (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hctraverse_ :: forall c (xs :: [[k]]) g proxy f. (AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> POP f xs -> g () #

htraverse_ :: forall (xs :: [[k]]) g f. (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> POP f xs -> g () #

HTraverse_ (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hctraverse_ :: forall c (xs :: [[k]]) g proxy f. (AllN (SOP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> SOP f xs -> g () #

htraverse_ :: forall (xs :: [[k]]) g f. (SListIN (SOP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> SOP f xs -> g () #

HTraverse_ (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hctraverse_ :: forall c (xs :: [k]) g proxy f. (AllN (NP :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g () #

htraverse_ :: forall (xs :: [k]) g f. (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> NP f xs -> g () #

HTraverse_ (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hctraverse_ :: forall c (xs :: [k]) g proxy f. (AllN (NS :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g () #

htraverse_ :: forall (xs :: [k]) g f. (SListIN (NS :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> NS f xs -> g () #

hcfoldMap :: forall {k} {l} h c (xs :: l) m proxy f. (HTraverse_ h, AllN h c xs, Monoid m) => proxy c -> (forall (a :: k). c a => f a -> m) -> h f xs -> m #

hcfor_ :: forall {k} {l} h c (xs :: l) g proxy f. (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall (a :: k). c a => f a -> g ()) -> g () #

class HAp h => HSequence (h :: (k -> Type) -> l -> Type) where #

Methods

hsequence' :: forall (xs :: l) f (g :: k -> Type). (SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs) #

hctraverse' :: forall c (xs :: l) g proxy f f'. (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) #

htraverse' :: forall (xs :: l) g f f'. (SListIN h xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs) #

Instances

Instances details
HSequence (POP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hsequence' :: forall (xs :: [[k]]) f (g :: k -> Type). (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative f) => POP (f :.: g) xs -> f (POP g xs) #

hctraverse' :: forall c (xs :: [[k]]) g proxy f f'. (AllN (POP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> POP f xs -> g (POP f' xs) #

htraverse' :: forall (xs :: [[k]]) g f f'. (SListIN (POP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs) #

HSequence (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hsequence' :: forall (xs :: [[k]]) f (g :: k -> Type). (SListIN (SOP :: (k -> Type) -> [[k]] -> Type) xs, Applicative f) => SOP (f :.: g) xs -> f (SOP g xs) #

hctraverse' :: forall c (xs :: [[k]]) g proxy f f'. (AllN (SOP :: (k -> Type) -> [[k]] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs) #

htraverse' :: forall (xs :: [[k]]) g f f'. (SListIN (SOP :: (k -> Type) -> [[k]] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs) #

HSequence (NP :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

hsequence' :: forall (xs :: [k]) f (g :: k -> Type). (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative f) => NP (f :.: g) xs -> f (NP g xs) #

hctraverse' :: forall c (xs :: [k]) g proxy f f'. (AllN (NP :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

htraverse' :: forall (xs :: [k]) g f f'. (SListIN (NP :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs) #

HSequence (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hsequence' :: forall (xs :: [k]) f (g :: k -> Type). (SListIN (NS :: (k -> Type) -> [k] -> Type) xs, Applicative f) => NS (f :.: g) xs -> f (NS g xs) #

hctraverse' :: forall c (xs :: [k]) g proxy f f'. (AllN (NS :: (k -> Type) -> [k] -> Type) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs) #

htraverse' :: forall (xs :: [k]) g f f'. (SListIN (NS :: (k -> Type) -> [k] -> Type) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs) #

hsequence :: forall {l} h (xs :: l) f. (SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) => h f xs -> f (h I xs) #

hsequenceK :: forall {k} {l} h (xs :: l) f a. (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a) :: k -> Type) xs -> f (h (K a :: k -> Type) xs) #

hctraverse :: forall {l} h c (xs :: l) g proxy f. (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs) #

hcfor :: forall {l} h c (xs :: l) g proxy f. (HSequence h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g a) -> g (h I xs) #

class HExpand (h :: (k -> Type) -> l -> Type) where #

Methods

hexpand :: forall (xs :: l) f. SListIN (Prod h) xs => (forall (x :: k). f x) -> h f xs -> Prod h f xs #

hcexpand :: forall c (xs :: l) proxy f. AllN (Prod h) c xs => proxy c -> (forall (x :: k). c x => f x) -> h f xs -> Prod h f xs #

Instances

Instances details
HExpand (SOP :: (k -> Type) -> [[k]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hexpand :: forall (xs :: [[k]]) f. SListIN (Prod (SOP :: (k -> Type) -> [[k]] -> Type)) xs => (forall (x :: k). f x) -> SOP f xs -> Prod (SOP :: (k -> Type) -> [[k]] -> Type) f xs #

hcexpand :: forall c (xs :: [[k]]) proxy f. AllN (Prod (SOP :: (k -> Type) -> [[k]] -> Type)) c xs => proxy c -> (forall (x :: k). c x => f x) -> SOP f xs -> Prod (SOP :: (k -> Type) -> [[k]] -> Type) f xs #

HExpand (NS :: (k -> Type) -> [k] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

hexpand :: forall (xs :: [k]) f. SListIN (Prod (NS :: (k -> Type) -> [k] -> Type)) xs => (forall (x :: k). f x) -> NS f xs -> Prod (NS :: (k -> Type) -> [k] -> Type) f xs #

hcexpand :: forall c (xs :: [k]) proxy f. AllN (Prod (NS :: (k -> Type) -> [k] -> Type)) c xs => proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod (NS :: (k -> Type) -> [k] -> Type) f xs #

class ((Same h1 :: (k2 -> Type) -> l2 -> Type) ~ h2, (Same h2 :: (k1 -> Type) -> l1 -> Type) ~ h1) => HTrans (h1 :: (k1 -> Type) -> l1 -> Type) (h2 :: (k2 -> Type) -> l2 -> Type) where #

Methods

htrans :: forall c (xs :: l1) (ys :: l2) proxy f g. AllZipN (Prod h1) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> h1 f xs -> h2 g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: l1) (ys :: l2). AllZipN (Prod h1) (LiftedCoercible f g) xs ys => h1 f xs -> h2 g ys #

Instances

Instances details
HTrans (POP :: (k1 -> Type) -> [[k1]] -> Type) (POP :: (k2 -> Type) -> [[k2]] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

htrans :: forall c (xs :: [[k1]]) (ys :: [[k2]]) proxy f g. AllZipN (Prod (POP :: (k1 -> Type) -> [[k1]] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> POP f xs -> POP g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [[k1]]) (ys :: [[k2]]). AllZipN (Prod (POP :: (k1 -> Type) -> [[k1]] -> Type)) (LiftedCoercible f g) xs ys => POP f xs -> POP g ys #

HTrans (SOP :: (k1 -> Type) -> [[k1]] -> Type) (SOP :: (k2 -> Type) -> [[k2]] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

htrans :: forall c (xs :: [[k1]]) (ys :: [[k2]]) proxy f g. AllZipN (Prod (SOP :: (k1 -> Type) -> [[k1]] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> SOP f xs -> SOP g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [[k1]]) (ys :: [[k2]]). AllZipN (Prod (SOP :: (k1 -> Type) -> [[k1]] -> Type)) (LiftedCoercible f g) xs ys => SOP f xs -> SOP g ys #

HTrans (NP :: (k1 -> Type) -> [k1] -> Type) (NP :: (k2 -> Type) -> [k2] -> Type) 
Instance details

Defined in Data.SOP.NP

Methods

htrans :: forall c (xs :: [k1]) (ys :: [k2]) proxy f g. AllZipN (Prod (NP :: (k1 -> Type) -> [k1] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NP f xs -> NP g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [k1]) (ys :: [k2]). AllZipN (Prod (NP :: (k1 -> Type) -> [k1] -> Type)) (LiftedCoercible f g) xs ys => NP f xs -> NP g ys #

HTrans (NS :: (k1 -> Type) -> [k1] -> Type) (NS :: (k2 -> Type) -> [k2] -> Type) 
Instance details

Defined in Data.SOP.NS

Methods

htrans :: forall c (xs :: [k1]) (ys :: [k2]) proxy f g. AllZipN (Prod (NS :: (k1 -> Type) -> [k1] -> Type)) c xs ys => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> NS f xs -> NS g ys #

hcoerce :: forall (f :: k1 -> Type) (g :: k2 -> Type) (xs :: [k1]) (ys :: [k2]). AllZipN (Prod (NS :: (k1 -> Type) -> [k1] -> Type)) (LiftedCoercible f g) xs ys => NS f xs -> NS g ys #

hfromI :: forall {l1} {k2} {l2} h1 (f :: k2 -> Type) (xs :: l1) (ys :: l2) h2. (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) => h1 I xs -> h2 f ys #

htoI :: forall {k1} {l1} {l2} h1 (f :: k1 -> Type) (xs :: l1) (ys :: l2) h2. (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) => h1 f xs -> h2 I ys #

type family Same (h :: (k1 -> Type) -> l1 -> Type) :: (k2 -> Type) -> l2 -> Type #

Instances

Instances details
type Same (POP :: (k1 -> Type) -> [[k1]] -> Type) 
Instance details

Defined in Data.SOP.NP

type Same (POP :: (k1 -> Type) -> [[k1]] -> Type) = POP :: (k2 -> Type) -> [[k2]] -> Type
type Same (SOP :: (k1 -> Type) -> [[k1]] -> Type) 
Instance details

Defined in Data.SOP.NS

type Same (SOP :: (k1 -> Type) -> [[k1]] -> Type) = SOP :: (k2 -> Type) -> [[k2]] -> Type
type Same (NP :: (k1 -> Type) -> [k1] -> Type) 
Instance details

Defined in Data.SOP.NP

type Same (NP :: (k1 -> Type) -> [k1] -> Type) = NP :: (k2 -> Type) -> [k2] -> Type
type Same (NS :: (k1 -> Type) -> [k1] -> Type) 
Instance details

Defined in Data.SOP.NS

type Same (NS :: (k1 -> Type) -> [k1] -> Type) = NS :: (k2 -> Type) -> [k2] -> Type