{-# LANGUAGE PolyKinds #-}
module Data.SOP.Classes
(
HPure(..)
, type (-.->)(..)
, fn
, fn_2
, fn_3
, fn_4
, Same
, Prod
, HAp(..)
, hliftA
, hliftA2
, hliftA3
, hmap
, hzipWith
, hzipWith3
, hcliftA
, hcliftA2
, hcliftA3
, hcmap
, hczipWith
, hczipWith3
, CollapseTo
, HCollapse(..)
, HTraverse_(..)
, HSequence(..)
, hcfoldMap
, hcfor_
, hsequence
, hsequenceK
, hctraverse
, hcfor
, HIndex(..)
, UnProd
, HApInjs(..)
, HExpand(..)
, HTrans(..)
, hfromI
, htoI
) where
import Data.Kind (Type)
import Data.SOP.BasicFunctors
import Data.SOP.Constraint
class HPure (h :: (k -> Type) -> (l -> Type)) where
hpure :: SListIN h xs => (forall a. f a) -> h f xs
hcpure :: (AllN h c xs) => proxy c -> (forall a. c a => f a) -> h f xs
newtype (f -.-> g) a = Fn { (-.->) f g a -> f a -> g a
apFn :: f a -> g a }
infixr 1 -.->
fn :: (f a -> f' a) -> (f -.-> f') a
fn_2 :: (f a -> f' a -> f'' a) -> (f -.-> f' -.-> f'') a
fn_3 :: (f a -> f' a -> f'' a -> f''' a) -> (f -.-> f' -.-> f'' -.-> f''') a
fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> f' -.-> f'' -.-> f''' -.-> f'''') a
fn :: (f a -> f' a) -> (-.->) f f' a
fn f a -> f' a
f = (f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> f' a) -> (-.->) f f' a) -> (f a -> f' a) -> (-.->) f f' a
forall a b. (a -> b) -> a -> b
$ \f a
x -> f a -> f' a
f f a
x
fn_2 :: (f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 f a -> f' a -> f'' a
f = (f a -> (-.->) f' f'' a) -> (-.->) f (f' -.-> f'') a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> (-.->) f' f'' a) -> (-.->) f (f' -.-> f'') a)
-> (f a -> (-.->) f' f'' a) -> (-.->) f (f' -.-> f'') a
forall a b. (a -> b) -> a -> b
$ \f a
x -> (f' a -> f'' a) -> (-.->) f' f'' a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f' a -> f'' a) -> (-.->) f' f'' a)
-> (f' a -> f'' a) -> (-.->) f' f'' a
forall a b. (a -> b) -> a -> b
$ \f' a
x' -> f a -> f' a -> f'' a
f f a
x f' a
x'
fn_3 :: (f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
fn_3 f a -> f' a -> f'' a -> f''' a
f = (f a -> (-.->) f' (f'' -.-> f''') a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> (-.->) f' (f'' -.-> f''') a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a)
-> (f a -> (-.->) f' (f'' -.-> f''') a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
forall a b. (a -> b) -> a -> b
$ \f a
x -> (f' a -> (-.->) f'' f''' a) -> (-.->) f' (f'' -.-> f''') a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f' a -> (-.->) f'' f''' a) -> (-.->) f' (f'' -.-> f''') a)
-> (f' a -> (-.->) f'' f''' a) -> (-.->) f' (f'' -.-> f''') a
forall a b. (a -> b) -> a -> b
$ \f' a
x' -> (f'' a -> f''' a) -> (-.->) f'' f''' a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f'' a -> f''' a) -> (-.->) f'' f''' a)
-> (f'' a -> f''' a) -> (-.->) f'' f''' a
forall a b. (a -> b) -> a -> b
$ \f'' a
x'' -> f a -> f' a -> f'' a -> f''' a
f f a
x f' a
x' f'' a
x''
fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a
fn_4 f a -> f' a -> f'' a -> f''' a -> f'''' a
f = (f a -> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a)
-> (f a -> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a)
-> (-.->) f (f' -.-> (f'' -.-> (f''' -.-> f''''))) a
forall a b. (a -> b) -> a -> b
$ \f a
x -> (f' a -> (-.->) f'' (f''' -.-> f'''') a)
-> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f' a -> (-.->) f'' (f''' -.-> f'''') a)
-> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a)
-> (f' a -> (-.->) f'' (f''' -.-> f'''') a)
-> (-.->) f' (f'' -.-> (f''' -.-> f'''')) a
forall a b. (a -> b) -> a -> b
$ \f' a
x' -> (f'' a -> (-.->) f''' f'''' a) -> (-.->) f'' (f''' -.-> f'''') a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f'' a -> (-.->) f''' f'''' a) -> (-.->) f'' (f''' -.-> f'''') a)
-> (f'' a -> (-.->) f''' f'''' a) -> (-.->) f'' (f''' -.-> f'''') a
forall a b. (a -> b) -> a -> b
$ \f'' a
x'' -> (f''' a -> f'''' a) -> (-.->) f''' f'''' a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f''' a -> f'''' a) -> (-.->) f''' f'''' a)
-> (f''' a -> f'''' a) -> (-.->) f''' f'''' a
forall a b. (a -> b) -> a -> b
$ \f''' a
x''' -> f a -> f' a -> f'' a -> f''' a -> f'''' a
f f a
x f' a
x' f'' a
x'' f''' a
x'''
type family Same (h :: (k1 -> Type) -> (l1 -> Type)) :: (k2 -> Type) -> (l2 -> Type)
type family Prod (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)
class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h :: (k -> Type) -> (l -> Type)) where
hap :: Prod h (f -.-> g) xs -> h f xs -> h g xs
hliftA :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs
hliftA2 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs
hliftA3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hliftA :: (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hliftA forall (a :: k). f a -> f' a
f h f xs
xs = (forall (a :: k). (-.->) f f' a) -> Prod h (f -.-> f') xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ((f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn f a -> f' a
forall (a :: k). f a -> f' a
f) Prod h (f -.-> f') xs -> h f xs -> h f' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f xs
xs
hliftA2 :: (forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hliftA2 forall (a :: k). f a -> f' a -> f'' a
f Prod h f xs
xs h f' xs
ys = (forall (a :: k). (-.->) f (f' -.-> f'') a)
-> Prod h (f -.-> (f' -.-> f'')) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ((f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 f a -> f' a -> f'' a
forall (a :: k). f a -> f' a -> f'' a
f) Prod (Prod h) (f -.-> (f' -.-> f'')) xs
-> Prod h f xs -> Prod h (f' -.-> f'') xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f xs
xs Prod h (f' -.-> f'') xs -> h f' xs -> h f'' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f' xs
ys
hliftA3 :: (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
hliftA3 forall (a :: k). f a -> f' a -> f'' a -> f''' a
f Prod h f xs
xs Prod h f' xs
ys h f'' xs
zs = (forall (a :: k). (-.->) f (f' -.-> (f'' -.-> f''')) a)
-> Prod h (f -.-> (f' -.-> (f'' -.-> f'''))) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ((f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
(f''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
fn_3 f a -> f' a -> f'' a -> f''' a
forall (a :: k). f a -> f' a -> f'' a -> f''' a
f) Prod (Prod h) (f -.-> (f' -.-> (f'' -.-> f'''))) xs
-> Prod h f xs -> Prod h (f' -.-> (f'' -.-> f''')) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f xs
xs Prod (Prod h) (f' -.-> (f'' -.-> f''')) xs
-> Prod h f' xs -> Prod h (f'' -.-> f''') xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f' xs
ys Prod h (f'' -.-> f''') xs -> h f'' xs -> h f''' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f'' xs
zs
hmap :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs
hzipWith :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs
hzipWith3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall 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 (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap = (forall (a :: k). f a -> f' a) -> h f xs -> h f' 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
hliftA
hzipWith :: (forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith = (forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *).
(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
hliftA2
hzipWith3 :: (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
hzipWith3 = (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
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(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
hliftA3
hcliftA :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA2 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs
hcliftA3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hcliftA :: proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA proxy c
p forall (a :: k). c a => f a -> f' a
f h f xs
xs = proxy c
-> (forall (a :: k). c a => (-.->) f f' a) -> Prod h (f -.-> 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 ((f a -> f' a) -> (-.->) f f' a
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn f a -> f' a
forall (a :: k). c a => f a -> f' a
f) Prod h (f -.-> f') xs -> h f xs -> h f' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f xs
xs
hcliftA2 :: proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hcliftA2 proxy c
p forall (a :: k). c a => f a -> f' a -> f'' a
f Prod h f xs
xs h f' xs
ys = proxy c
-> (forall (a :: k). c a => (-.->) f (f' -.-> f'') a)
-> Prod h (f -.-> (f' -.-> 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 ((f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 f a -> f' a -> f'' a
forall (a :: k). c a => f a -> f' a -> f'' a
f) Prod (Prod h) (f -.-> (f' -.-> f'')) xs
-> Prod h f xs -> Prod h (f' -.-> f'') xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f xs
xs Prod h (f' -.-> f'') xs -> h f' xs -> h f'' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f' xs
ys
hcliftA3 :: 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
hcliftA3 proxy c
p forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a
f Prod h f xs
xs Prod h f' xs
ys h f'' xs
zs = proxy c
-> (forall (a :: k). c a => (-.->) f (f' -.-> (f'' -.-> f''')) a)
-> Prod h (f -.-> (f' -.-> (f'' -.-> 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 ((f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *)
(f''' :: k -> *).
(f a -> f' a -> f'' a -> f''' a)
-> (-.->) f (f' -.-> (f'' -.-> f''')) a
fn_3 f a -> f' a -> f'' a -> f''' a
forall (a :: k). c a => f a -> f' a -> f'' a -> f''' a
f) Prod (Prod h) (f -.-> (f' -.-> (f'' -.-> f'''))) xs
-> Prod h f xs -> Prod h (f' -.-> (f'' -.-> f''')) xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f xs
xs Prod (Prod h) (f' -.-> (f'' -.-> f''')) xs
-> Prod h f' xs -> Prod h (f'' -.-> f''') xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` Prod h f' xs
ys Prod h (f'' -.-> f''') xs -> h f'' xs -> h f''' xs
forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
(xs :: l).
HAp h =>
Prod h (f -.-> g) xs -> h f xs -> h g xs
`hap` h f'' xs
zs
hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs
hczipWith :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs
hczipWith3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
hcmap :: proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap = proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
(f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcliftA
hczipWith :: proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
hczipWith = proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod h f xs
-> h f' xs
-> h f'' xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *).
(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
hcliftA2
hczipWith3 :: 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
hczipWith3 = 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
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
(f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
(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
hcliftA3
type family CollapseTo (h :: (k -> Type) -> (l -> Type)) (x :: Type) :: Type
class HCollapse (h :: (k -> Type) -> (l -> Type)) where
hcollapse :: SListIN h xs => h (K a) xs -> CollapseTo h a
class HTraverse_ (h :: (k -> Type) -> (l -> Type)) where
hctraverse_ :: (AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> h f xs -> g ()
htraverse_ :: (SListIN h xs, Applicative g) => (forall a. f a -> g ()) -> h f xs -> g ()
hcfor_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g ()) -> g ()
hcfor_ :: proxy c -> h f xs -> (forall (a :: k). c a => f a -> g ()) -> g ()
hcfor_ proxy c
p h f xs
xs forall (a :: k). c a => f a -> g ()
f = proxy c -> (forall (a :: k). c a => f a -> g ()) -> h f xs -> g ()
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
(f :: k -> *).
(HTraverse_ h, AllN h c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> h f xs -> g ()
hctraverse_ proxy c
p forall (a :: k). c a => f a -> g ()
f h f xs
xs
hcfoldMap :: (HTraverse_ h, AllN h c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> h f xs -> m
hcfoldMap :: proxy c -> (forall (a :: k). c a => f a -> m) -> h f xs -> m
hcfoldMap proxy c
p forall (a :: k). c a => f a -> m
f = K m () -> m
forall k a (b :: k). K a b -> a
unK (K m () -> m) -> (h f xs -> K m ()) -> h f xs -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy c
-> (forall (a :: k). c a => f a -> K m ()) -> h f xs -> K m ()
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
(xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
(f :: k -> *).
(HTraverse_ h, AllN h c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> h f xs -> g ()
hctraverse_ proxy c
p (m -> K m ()
forall k a (b :: k). a -> K a b
K (m -> K m ()) -> (f a -> m) -> f a -> K m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> m
forall (a :: k). c a => f a -> m
f)
class HAp h => HSequence (h :: (k -> Type) -> (l -> Type)) where
hsequence' :: (SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs)
hctraverse' :: (AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> h f xs -> g (h f' xs)
htraverse' :: (SListIN h xs, Applicative g) => (forall a. f a -> g (f' a)) -> h f xs -> g (h f' xs)
hctraverse :: (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)
hctraverse :: proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)
hctraverse proxy c
p forall a. c a => f a -> g a
f = proxy c
-> (forall a. c a => f a -> g (I a)) -> h f xs -> g (h I 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 c
p ((a -> I a) -> g a -> g (I a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> I a
forall a. a -> I a
I (g a -> g (I a)) -> (f a -> g a) -> f a -> g (I a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall a. c a => f a -> g a
f)
hcfor :: (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)
hcfor :: proxy c -> h f xs -> (forall a. c a => f a -> g a) -> g (h I xs)
hcfor proxy c
p h f xs
xs forall a. c a => f a -> g a
f = proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)
forall l (h :: (* -> *) -> l -> *) (c :: * -> Constraint) (xs :: l)
(g :: * -> *) (proxy :: (* -> Constraint) -> *) (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)
hctraverse proxy c
p forall a. c a => f a -> g a
f h f xs
xs
hsequence :: (SListIN h xs, SListIN (Prod h) xs, HSequence h) => Applicative f => h f xs -> f (h I xs)
hsequence :: h f xs -> f (h I xs)
hsequence = h (f :.: I) xs -> f (h I xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *)
(g :: k -> *).
(HSequence h, SListIN h xs, Applicative f) =>
h (f :.: g) xs -> f (h g xs)
hsequence' (h (f :.: I) xs -> f (h I xs))
-> (h f xs -> h (f :.: I) xs) -> h f xs -> f (h I xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. f a -> (:.:) f I a) -> h f xs -> h (f :.: I) 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
hliftA (f (I a) -> (:.:) f I a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f (I a) -> (:.:) f I a) -> (f a -> f (I a)) -> f a -> (:.:) f I a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> I a) -> f a -> f (I a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> I a
forall a. a -> I a
I)
hsequenceK :: (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)
hsequenceK :: h (K (f a)) xs -> f (h (K a) xs)
hsequenceK = h (f :.: K a) xs -> f (h (K a) xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *)
(g :: k -> *).
(HSequence h, SListIN h xs, Applicative f) =>
h (f :.: g) xs -> f (h g xs)
hsequence' (h (f :.: K a) xs -> f (h (K a) xs))
-> (h (K (f a)) xs -> h (f :.: K a) xs)
-> h (K (f a)) xs
-> f (h (K a) xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). K (f a) a -> (:.:) f (K a) a)
-> h (K (f a)) xs -> h (f :.: K a) 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
hliftA (f (K a a) -> (:.:) f (K a) a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f (K a a) -> (:.:) f (K a) a)
-> (K (f a) a -> f (K a a)) -> K (f a) a -> (:.:) f (K a) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> K a a) -> f a -> f (K a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> K a a
forall k a (b :: k). a -> K a b
K (f a -> f (K a a)) -> (K (f a) a -> f a) -> K (f a) a -> f (K a a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K (f a) a -> f a
forall k a (b :: k). K a b -> a
unK)
class HIndex (h :: (k -> Type) -> (l -> Type)) where
hindex :: h f xs -> Int
type family UnProd (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)
class (UnProd (Prod h) ~ h) => HApInjs (h :: (k -> Type) -> (l -> Type)) where
hapInjs :: (SListIN h xs) => Prod h f xs -> [h f xs]
class HExpand (h :: (k -> Type) -> (l -> Type)) where
hexpand :: (SListIN (Prod h) xs) => (forall x . f x) -> h f xs -> Prod h f xs
hcexpand :: (AllN (Prod h) c xs) => proxy c -> (forall x . c x => f x) -> h f xs -> Prod h f xs
class (Same h1 ~ h2, Same h2 ~ h1) => HTrans (h1 :: (k1 -> Type) -> (l1 -> Type)) (h2 :: (k2 -> Type) -> (l2 -> Type)) where
htrans ::
AllZipN (Prod h1) c xs ys
=> proxy c
-> (forall x y . c x y => f x -> g y)
-> h1 f xs -> h2 g ys
hcoerce ::
AllZipN (Prod h1) (LiftedCoercible f g) xs ys
=> h1 f xs -> h2 g ys
hfromI ::
(AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2)
=> h1 I xs -> h2 f ys
hfromI :: h1 I xs -> h2 f ys
hfromI = h1 I xs -> h2 f ys
forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *)
(h2 :: (k2 -> *) -> l2 -> *) (f :: k1 -> *) (g :: k2 -> *)
(xs :: l1) (ys :: l2).
(HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) =>
h1 f xs -> h2 g ys
hcoerce
htoI ::
(AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2)
=> h1 f xs -> h2 I ys
htoI :: h1 f xs -> h2 I ys
htoI = h1 f xs -> h2 I ys
forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *)
(h2 :: (k2 -> *) -> l2 -> *) (f :: k1 -> *) (g :: k2 -> *)
(xs :: l1) (ys :: l2).
(HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) =>
h1 f xs -> h2 g ys
hcoerce