{-# LANGUAGE BlockArguments, LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications, RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs, TypeFamilies, DataKinds, ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.HeteroParList (

	-- * Hetero List

	L, pattern (:*), Id(..),

	-- * Lengthed List
	
	LL, LL', pattern (:*.), Dummy(..), Dummies, ToDummies,

	-- * Hetero Parameter List

	PL(..), PL2, PL3, PL4,
	pattern Singleton, pattern Singleton2,
	pattern Singleton3, pattern Singleton4,

	-- * From/To List

	-- ** Hetero List

	-- *** fromList

	FromList(..),

	-- *** toList

	toList, toList2, toList3,
	toListM, toListM2, toListM3, toListM_, toListM2_, toListM3_,
	ToListT2(..), ToListT3(..),

	-- *** zipToList

	zipToList, zip3ToList, zip4ToList,

--	-- *** zipList

--	zipList, zipList2, zipList3,
--	zipListM, zipListM2, zipListM3, zipListM_, zipListM2_, zipListM3_,

	-- *** with constraint

	ToListWithC(..), ToListWithC2(..),
	ZipListWithC(..), ZipListWithC2(..), ZipListWithC3(..),

	ToListWithCM(..), ToListWithCM'(..),
	ToListWithCCpsM(..), ToListWithCCpsM'(..), withListWithCCpsM',

	-- ** Homo List

	-- *** Homo List

	HomoList(..),

	-- *** Homo List With Num

	HomoListN(..), Num, tnum,

	-- * Index

	TypeIndex(..), index, homoListIndex,

	-- * Map and ReplicateM

	map, mapM, mapM_, MapM'(..),
	Rep(..), RepM(..), replicate, replicateM, replicateMWithI

	) where

import Prelude hiding (map, mapM, mapM_, replicate, Num)

import GHC.TypeLits
import Data.Kind
import Data.Proxy
import Data.Default
import Data.List (genericIndex)

-- Hetero List

type L as = PL Id as

{-# COMPLETE (:*) #-}

infixr 5 :*

pattern (:*) :: a -> L as -> L (a ': as)
pattern x $m:* :: forall {r} {a} {as :: [*]}.
L (a : as) -> (a -> L as -> r) -> ((# #) -> r) -> r
$b:* :: forall a (as :: [*]). a -> L as -> L (a : as)
:* xs <- Id x :** xs where a
x :* L as
xs = a -> Id a
forall a. a -> Id a
Id a
x Id a -> L as -> PL Id (a : as)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** L as
xs

newtype Id a = Id a deriving Int -> Id a -> ShowS
[Id a] -> ShowS
Id a -> String
(Int -> Id a -> ShowS)
-> (Id a -> String) -> ([Id a] -> ShowS) -> Show (Id a)
forall a. Show a => Int -> Id a -> ShowS
forall a. Show a => [Id a] -> ShowS
forall a. Show a => Id a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Id a -> ShowS
showsPrec :: Int -> Id a -> ShowS
$cshow :: forall a. Show a => Id a -> String
show :: Id a -> String
$cshowList :: forall a. Show a => [Id a] -> ShowS
showList :: [Id a] -> ShowS
Show

-- Lengthed List

type LL a ds = PL (Dummy a) ds
type LL' a n = PL (Dummy a) (Dummies n)

{-# COMPLETE (:*.) #-}

infixr 5 :*.

pattern (:*.) :: a -> LL a ds -> LL a ('() ': ds)
pattern x $m:*. :: forall {r} {a} {ds :: [()]}.
LL a ('() : ds) -> (a -> LL a ds -> r) -> ((# #) -> r) -> r
$b:*. :: forall a (ds :: [()]). a -> LL a ds -> LL a ('() : ds)
:*. xs <- Dummy x :** xs where a
x :*. LL a ds
xs = a -> Dummy a '()
forall a (d :: ()). a -> Dummy a d
Dummy a
x Dummy a '() -> LL a ds -> PL (Dummy a) ('() : ds)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** LL a ds
xs

newtype Dummy a (d :: ()) = Dummy a deriving Int -> Dummy a d -> ShowS
[Dummy a d] -> ShowS
Dummy a d -> String
(Int -> Dummy a d -> ShowS)
-> (Dummy a d -> String)
-> ([Dummy a d] -> ShowS)
-> Show (Dummy a d)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a (d :: ()). Show a => Int -> Dummy a d -> ShowS
forall a (d :: ()). Show a => [Dummy a d] -> ShowS
forall a (d :: ()). Show a => Dummy a d -> String
$cshowsPrec :: forall a (d :: ()). Show a => Int -> Dummy a d -> ShowS
showsPrec :: Int -> Dummy a d -> ShowS
$cshow :: forall a (d :: ()). Show a => Dummy a d -> String
show :: Dummy a d -> String
$cshowList :: forall a (d :: ()). Show a => [Dummy a d] -> ShowS
showList :: [Dummy a d] -> ShowS
Show

type family Dummies n where
	Dummies 0 = '[]
	Dummies n = '() ': Dummies (n - 1)

type family ToDummies xs where
	ToDummies '[] = '[]
	ToDummies (x ': xs) = '() ': ToDummies xs

-- Hetero Parameter List

infixr 5 :**

data PL (t :: k -> Type) (ss :: [k]) where
	Nil :: PL t '[]
	(:**) :: t s -> PL t ss -> PL t (s ': ss)

instance Show (PL t '[]) where show :: PL t '[] -> String
show PL t '[]
Nil = String
"Nil"

instance (Show (t s), Show (PL t ss)) =>
	Show (PL t (s ': ss)) where
	show :: PL t (s : ss) -> String
show (t s
x :** PL t ss
xs) = t s -> String
forall a. Show a => a -> String
show t s
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ PL t ss -> String
forall a. Show a => a -> String
show PL t ss
xs

instance Eq (PL t '[]) where PL t '[]
Nil == :: PL t '[] -> PL t '[] -> Bool
== PL t '[]
Nil = Bool
True

instance (Eq (t s), Eq (PL t ss)) =>
	Eq (PL t (s ': ss)) where
	(t s
x :** PL t ss
xs) == :: PL t (s : ss) -> PL t (s : ss) -> Bool
== (t s
y :** PL t ss
ys) = t s
x t s -> t s -> Bool
forall a. Eq a => a -> a -> Bool
== t s
t s
y Bool -> Bool -> Bool
&& PL t ss
xs PL t ss -> PL t ss -> Bool
forall a. Eq a => a -> a -> Bool
== PL t ss
PL t ss
ys

{-# COMPLETE Singleton #-}

pattern Singleton :: t s -> PL t '[s]
pattern $mSingleton :: forall {r} {k} {t :: k -> *} {s :: k}.
PL t '[s] -> (t s -> r) -> ((# #) -> r) -> r
$bSingleton :: forall {k} (t :: k -> *) (s :: k). t s -> PL t '[s]
Singleton x <- (x :** Nil) where
	Singleton t s
x = t s
x t s -> PL t '[] -> PL t '[s]
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil

pattern Singleton2 :: t s -> PL2 t '[ '[s]]
pattern $mSingleton2 :: forall {r} {k} {t :: k -> *} {s :: k}.
PL2 t '[ '[s]] -> (t s -> r) -> ((# #) -> r) -> r
$bSingleton2 :: forall {k} (t :: k -> *) (s :: k). t s -> PL2 t '[ '[s]]
Singleton2 x <- Singleton (Singleton x) where
	Singleton2 t s
x = PL t '[s] -> PL (PL t) '[ '[s]]
forall {k} (t :: k -> *) (s :: k). t s -> PL t '[s]
Singleton (PL t '[s] -> PL (PL t) '[ '[s]])
-> PL t '[s] -> PL (PL t) '[ '[s]]
forall a b. (a -> b) -> a -> b
$ t s -> PL t '[s]
forall {k} (t :: k -> *) (s :: k). t s -> PL t '[s]
Singleton t s
x

pattern Singleton3 :: t s -> PL3 t '[ '[ '[s]]]
pattern $mSingleton3 :: forall {r} {k} {t :: k -> *} {s :: k}.
PL3 t '[ '[ '[s]]] -> (t s -> r) -> ((# #) -> r) -> r
$bSingleton3 :: forall {k} (t :: k -> *) (s :: k). t s -> PL3 t '[ '[ '[s]]]
Singleton3 x <- Singleton (Singleton2 x) where
	Singleton3 t s
x = PL2 t '[ '[s]] -> PL (PL2 t) '[ '[ '[s]]]
forall {k} (t :: k -> *) (s :: k). t s -> PL t '[s]
Singleton (PL2 t '[ '[s]] -> PL (PL2 t) '[ '[ '[s]]])
-> PL2 t '[ '[s]] -> PL (PL2 t) '[ '[ '[s]]]
forall a b. (a -> b) -> a -> b
$ t s -> PL2 t '[ '[s]]
forall {k} (t :: k -> *) (s :: k). t s -> PL2 t '[ '[s]]
Singleton2 t s
x

pattern Singleton4 :: t s -> PL4 t '[ '[ '[ '[s]]]]
pattern $mSingleton4 :: forall {r} {k} {t :: k -> *} {s :: k}.
PL4 t '[ '[ '[ '[s]]]] -> (t s -> r) -> ((# #) -> r) -> r
$bSingleton4 :: forall {k} (t :: k -> *) (s :: k). t s -> PL4 t '[ '[ '[ '[s]]]]
Singleton4 x <- Singleton (Singleton3 x) where
	Singleton4 t s
x = PL3 t '[ '[ '[s]]] -> PL (PL3 t) '[ '[ '[ '[s]]]]
forall {k} (t :: k -> *) (s :: k). t s -> PL t '[s]
Singleton (PL3 t '[ '[ '[s]]] -> PL (PL3 t) '[ '[ '[ '[s]]]])
-> PL3 t '[ '[ '[s]]] -> PL (PL3 t) '[ '[ '[ '[s]]]]
forall a b. (a -> b) -> a -> b
$ t s -> PL3 t '[ '[ '[s]]]
forall {k} (t :: k -> *) (s :: k). t s -> PL3 t '[ '[ '[s]]]
Singleton3 t s
x

type PL2 t = PL (PL t)
type PL3 t = PL (PL2 t)
type PL4 t = PL (PL3 t)

-- From/To List

class FromList (ss :: [k]) where
	fromList :: (forall (s :: k) . a -> t s) -> [a] -> PL t ss

instance FromList '[] where
	fromList :: forall a (t :: k -> *).
(forall (s :: k). a -> t s) -> [a] -> PL t '[]
fromList forall (s :: k). a -> t s
_ [] = PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	fromList forall (s :: k). a -> t s
_ [a]
_ = String -> PL t '[]
forall a. HasCallStack => String -> a
error String
"bad"

instance FromList ss => FromList (s ': ss) where
	fromList :: forall a (t :: k -> *).
(forall (s :: k). a -> t s) -> [a] -> PL t (s : ss)
fromList forall (s :: k). a -> t s
f (a
x : [a]
xs) = a -> t s
forall (s :: k). a -> t s
f a
x t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** (forall (s :: k). a -> t s) -> [a] -> PL t ss
forall k (ss :: [k]) a (t :: k -> *).
FromList ss =>
(forall (s :: k). a -> t s) -> [a] -> PL t ss
forall a (t :: k -> *).
(forall (s :: k). a -> t s) -> [a] -> PL t ss
fromList a -> t s
forall (s :: k). a -> t s
f [a]
xs
	fromList forall (s :: k). a -> t s
_ [a]
_ = String -> PL t (s : ss)
forall a. HasCallStack => String -> a
error String
"bad"

toList :: (forall (s :: k) . t s -> a) -> PL t ss -> [a]
toList :: forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
toList forall (s :: k). t s -> a
_ PL t ss
Nil = []
toList forall (s :: k). t s -> a
f (t s
x :** PL t ss
xs) = t s -> a
forall (s :: k). t s -> a
f t s
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s :: k). t s -> a) -> PL t ss -> [a]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
toList t s -> a
forall (s :: k). t s -> a
f PL t ss
xs
 
toList2 :: (forall (s :: k) . t s -> a) -> PL2 t sss -> [[a]]
toList2 :: forall k (t :: k -> *) a (sss :: [[k]]).
(forall (s :: k). t s -> a) -> PL2 t sss -> [[a]]
toList2 forall (s :: k). t s -> a
f = (forall (s :: [k]). PL t s -> [a]) -> PL (PL t) sss -> [[a]]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
toList ((forall (s :: [k]). PL t s -> [a]) -> PL (PL t) sss -> [[a]])
-> (forall (s :: [k]). PL t s -> [a]) -> PL (PL t) sss -> [[a]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> a) -> PL t s -> [a]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
toList t s -> a
forall (s :: k). t s -> a
f

toList3 :: (forall (s :: k) . t s -> a) -> PL3 t ssss -> [[[a]]]
toList3 :: forall k (t :: k -> *) a (ssss :: [[[k]]]).
(forall (s :: k). t s -> a) -> PL3 t ssss -> [[[a]]]
toList3 forall (s :: k). t s -> a
f = (forall (s :: [[k]]). PL2 t s -> [[a]])
-> PL (PL2 t) ssss -> [[[a]]]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
toList ((forall (s :: [[k]]). PL2 t s -> [[a]])
 -> PL (PL2 t) ssss -> [[[a]]])
-> (forall (s :: [[k]]). PL2 t s -> [[a]])
-> PL (PL2 t) ssss
-> [[[a]]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> a) -> PL2 t s -> [[a]]
forall k (t :: k -> *) a (sss :: [[k]]).
(forall (s :: k). t s -> a) -> PL2 t sss -> [[a]]
toList2 t s -> a
forall (s :: k). t s -> a
f

toListM :: Applicative m => (forall (s :: k) . t s -> m a) -> PL t ss -> m [a]
toListM :: forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m [a]
toListM forall (s :: k). t s -> m a
_ PL t ss
Nil = [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
toListM forall (s :: k). t s -> m a
f (t s
x :** PL t ss
xs) = (:) (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> m a
forall (s :: k). t s -> m a
f t s
x m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (s :: k). t s -> m a) -> PL t ss -> m [a]
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m [a]
toListM t s -> m a
forall (s :: k). t s -> m a
f PL t ss
xs

toListM2 :: Applicative m =>
	(forall (s :: k) . t s -> m a) -> PL2 t sss -> m [[a]]
toListM2 :: forall (m :: * -> *) k (t :: k -> *) a (sss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL2 t sss -> m [[a]]
toListM2 forall (s :: k). t s -> m a
f = (forall (s :: [k]). PL t s -> m [a]) -> PL (PL t) sss -> m [[a]]
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m [a]
toListM ((forall (s :: [k]). PL t s -> m [a]) -> PL (PL t) sss -> m [[a]])
-> (forall (s :: [k]). PL t s -> m [a]) -> PL (PL t) sss -> m [[a]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> m a) -> PL t s -> m [a]
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m [a]
toListM t s -> m a
forall (s :: k). t s -> m a
f

toListM3 :: Applicative m =>
	(forall (s :: k) . t s -> m a) -> PL3 t sss -> m [[[a]]]
toListM3 :: forall (m :: * -> *) k (t :: k -> *) a (sss :: [[[k]]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL3 t sss -> m [[[a]]]
toListM3 forall (s :: k). t s -> m a
f = (forall (s :: [[k]]). PL2 t s -> m [[a]])
-> PL (PL2 t) sss -> m [[[a]]]
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m [a]
toListM ((forall (s :: [[k]]). PL2 t s -> m [[a]])
 -> PL (PL2 t) sss -> m [[[a]]])
-> (forall (s :: [[k]]). PL2 t s -> m [[a]])
-> PL (PL2 t) sss
-> m [[[a]]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> m a) -> PL2 t s -> m [[a]]
forall (m :: * -> *) k (t :: k -> *) a (sss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL2 t sss -> m [[a]]
toListM2 t s -> m a
forall (s :: k). t s -> m a
f

toListM_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL t ss -> m ()
toListM_ :: forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
toListM_ forall (s :: k). t s -> m a
_ PL t ss
Nil = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
toListM_ forall (s :: k). t s -> m a
f (t s
x :** PL t ss
xs) = t s -> m a
forall (s :: k). t s -> m a
f t s
x m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (forall (s :: k). t s -> m a) -> PL t ss -> m ()
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
toListM_ t s -> m a
forall (s :: k). t s -> m a
f PL t ss
xs

toListM2_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL2 t ss -> m ()
toListM2_ :: forall (m :: * -> *) k (t :: k -> *) a (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL2 t ss -> m ()
toListM2_ forall (s :: k). t s -> m a
f = (forall (s :: [k]). PL t s -> m ()) -> PL (PL t) ss -> m ()
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
toListM_ ((forall (s :: [k]). PL t s -> m ()) -> PL (PL t) ss -> m ())
-> (forall (s :: [k]). PL t s -> m ()) -> PL (PL t) ss -> m ()
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> m a) -> PL t s -> m ()
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
toListM_ t s -> m a
forall (s :: k). t s -> m a
f

toListM3_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL3 t ss -> m ()
toListM3_ :: forall (m :: * -> *) k (t :: k -> *) a (ss :: [[[k]]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL3 t ss -> m ()
toListM3_ forall (s :: k). t s -> m a
f = (forall (s :: [[k]]). PL2 t s -> m ()) -> PL (PL2 t) ss -> m ()
forall (m :: * -> *) k (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
toListM_ ((forall (s :: [[k]]). PL2 t s -> m ()) -> PL (PL2 t) ss -> m ())
-> (forall (s :: [[k]]). PL2 t s -> m ()) -> PL (PL2 t) ss -> m ()
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> m a) -> PL (PL t) s -> m ()
forall (m :: * -> *) k (t :: k -> *) a (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL2 t ss -> m ()
toListM2_ t s -> m a
forall (s :: k). t s -> m a
f

class ToListT2 k1 k2 (ss :: [(k1, k2)]) where
	toListT2 ::
		(forall (s1 :: k1) (s2 :: k2) . t '(s1, s2) -> a) ->
		PL t ss -> [a]

instance ToListT2 k1 k2 '[] where toListT2 :: forall (t :: (k1, k2) -> *) a.
(forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a) -> PL t '[] -> [a]
toListT2 forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a
_ PL t '[]
Nil = []

instance ToListT2 k1 k2 ss => ToListT2 k1 k2 ('(s1, s2) ': ss) where
	toListT2 :: forall (t :: (k1, k2) -> *) a.
(forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a)
-> PL t ('(s1, s2) : ss) -> [a]
toListT2 forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a
f (t s
x :** PL t ss
xs) = t '(s1, s2) -> a
forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a
f t s
t '(s1, s2)
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a) -> PL t ss -> [a]
forall k1 k2 (ss :: [(k1, k2)]) (t :: (k1, k2) -> *) a.
ToListT2 k1 k2 ss =>
(forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a) -> PL t ss -> [a]
forall (t :: (k1, k2) -> *) a.
(forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a) -> PL t ss -> [a]
toListT2 t '(s1, s2) -> a
forall (s1 :: k1) (s2 :: k2). t '(s1, s2) -> a
f PL t ss
xs

class ToListT3 k1 k2 k3 (ss :: [(k1, k2, k3)]) where
	toListT3 ::
		(forall (s1 :: k1) (s2 :: k2) (s3 :: k3) .
			t '(s1, s2, s3) -> a) -> PL t ss -> [a]

instance ToListT3 k1 k2 k3 '[] where toListT3 :: forall (t :: (k1, k2, k3) -> *) a.
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a)
-> PL t '[] -> [a]
toListT3 forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a
_ PL t '[]
Nil = []

instance ToListT3 k1 k2 k3 ss => ToListT3 k1 k2 k3 ('(s1, s2, s3) ': ss) where
	toListT3 :: forall (t :: (k1, k2, k3) -> *) a.
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a)
-> PL t ('(s1, s2, s3) : ss) -> [a]
toListT3 forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a
f (t s
x :** PL t ss
xs) = t '(s1, s2, s3) -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a
f t s
t '(s1, s2, s3)
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a)
-> PL t ss -> [a]
forall k1 k2 k3 (ss :: [(k1, k2, k3)]) (t :: (k1, k2, k3) -> *) a.
ToListT3 k1 k2 k3 ss =>
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a)
-> PL t ss -> [a]
forall (t :: (k1, k2, k3) -> *) a.
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a)
-> PL t ss -> [a]
toListT3 t '(s1, s2, s3) -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3). t '(s1, s2, s3) -> a
f PL t ss
xs

zipToList :: (forall (s :: k) (s' :: k') . t s -> t' s' -> a) ->
	PL t ss -> PL t' ss' -> [a]
zipToList :: forall k k' (t :: k -> *) (t' :: k' -> *) a (ss :: [k])
       (ss' :: [k']).
(forall (s :: k) (s' :: k'). t s -> t' s' -> a)
-> PL t ss -> PL t' ss' -> [a]
zipToList forall (s :: k) (s' :: k'). t s -> t' s' -> a
_ PL t ss
Nil PL t' ss'
_ = []
zipToList forall (s :: k) (s' :: k'). t s -> t' s' -> a
_ PL t ss
_ PL t' ss'
Nil = []
zipToList forall (s :: k) (s' :: k'). t s -> t' s' -> a
f (t s
x :** PL t ss
xs) (t' s
y :** PL t' ss
ys) = t s -> t' s -> a
forall (s :: k) (s' :: k'). t s -> t' s' -> a
f t s
x t' s
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s :: k) (s' :: k'). t s -> t' s' -> a)
-> PL t ss -> PL t' ss -> [a]
forall k k' (t :: k -> *) (t' :: k' -> *) a (ss :: [k])
       (ss' :: [k']).
(forall (s :: k) (s' :: k'). t s -> t' s' -> a)
-> PL t ss -> PL t' ss' -> [a]
zipToList t s -> t' s' -> a
forall (s :: k) (s' :: k'). t s -> t' s' -> a
f PL t ss
xs PL t' ss
ys

zip3ToList :: (forall (s1 :: k1) (s2 :: k2) (s3 :: k3) .
	t1 s1 -> t2 s2 -> t3 s3 -> a) ->
	PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> [a]
zip3ToList :: forall k1 k2 k3 (t1 :: k1 -> *) (t2 :: k2 -> *) (t3 :: k3 -> *) a
       (ss1 :: [k1]) (ss2 :: [k2]) (ss3 :: [k3]).
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
 t1 s1 -> t2 s2 -> t3 s3 -> a)
-> PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> [a]
zip3ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
_ PL t1 ss1
Nil PL t2 ss2
_ PL t3 ss3
_ = []
zip3ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
_ PL t1 ss1
_ PL t2 ss2
Nil PL t3 ss3
_ = []
zip3ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
_ PL t1 ss1
_ PL t2 ss2
_ PL t3 ss3
Nil = []
zip3ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
f (t1 s
x :** PL t1 ss
xs) (t2 s
y :** PL t2 ss
ys) (t3 s
z :** PL t3 ss
zs) = t1 s -> t2 s -> t3 s -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
f t1 s
x t2 s
y t3 s
z a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
 t1 s1 -> t2 s2 -> t3 s3 -> a)
-> PL t1 ss -> PL t2 ss -> PL t3 ss -> [a]
forall k1 k2 k3 (t1 :: k1 -> *) (t2 :: k2 -> *) (t3 :: k3 -> *) a
       (ss1 :: [k1]) (ss2 :: [k2]) (ss3 :: [k3]).
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
 t1 s1 -> t2 s2 -> t3 s3 -> a)
-> PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> [a]
zip3ToList t1 s1 -> t2 s2 -> t3 s3 -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3).
t1 s1 -> t2 s2 -> t3 s3 -> a
f PL t1 ss
xs PL t2 ss
ys PL t3 ss
zs

zip4ToList :: (forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4) .
	t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a) ->
	PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> PL t4 ss4 -> [a]
zip4ToList :: forall k1 k2 k3 k4 (t1 :: k1 -> *) (t2 :: k2 -> *) (t3 :: k3 -> *)
       (t4 :: k4 -> *) a (ss1 :: [k1]) (ss2 :: [k2]) (ss3 :: [k3])
       (ss4 :: [k4]).
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
 t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a)
-> PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> PL t4 ss4 -> [a]
zip4ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
_ PL t1 ss1
Nil PL t2 ss2
_ PL t3 ss3
_ PL t4 ss4
_ = []
zip4ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
_ PL t1 ss1
_ PL t2 ss2
Nil PL t3 ss3
_ PL t4 ss4
_ = []
zip4ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
_ PL t1 ss1
_ PL t2 ss2
_ PL t3 ss3
Nil PL t4 ss4
_ = []
zip4ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
_ PL t1 ss1
_ PL t2 ss2
_ PL t3 ss3
_ PL t4 ss4
Nil = []
zip4ToList forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
f (t1 s
x :** PL t1 ss
xs) (t2 s
y :** PL t2 ss
ys) (t3 s
z :** PL t3 ss
zs) (t4 s
w :** PL t4 ss
ws) =
	t1 s -> t2 s -> t3 s -> t4 s -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
f t1 s
x t2 s
y t3 s
z t4 s
w a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
 t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a)
-> PL t1 ss -> PL t2 ss -> PL t3 ss -> PL t4 ss -> [a]
forall k1 k2 k3 k4 (t1 :: k1 -> *) (t2 :: k2 -> *) (t3 :: k3 -> *)
       (t4 :: k4 -> *) a (ss1 :: [k1]) (ss2 :: [k2]) (ss3 :: [k3])
       (ss4 :: [k4]).
(forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
 t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a)
-> PL t1 ss1 -> PL t2 ss2 -> PL t3 ss3 -> PL t4 ss4 -> [a]
zip4ToList t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
forall (s1 :: k1) (s2 :: k2) (s3 :: k3) (s4 :: k4).
t1 s1 -> t2 s2 -> t3 s3 -> t4 s4 -> a
f PL t1 ss
xs PL t2 ss
ys PL t3 ss
zs PL t4 ss
ws

zipList :: (forall (s :: k) . t s -> t' s -> a) ->
	PL t ss -> PL t' ss -> [a]
zipList :: forall k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
zipList forall (s :: k). t s -> t' s -> a
_ PL t ss
Nil PL t' ss
Nil = []
zipList forall (s :: k). t s -> t' s -> a
f (t s
x :** PL t ss
xs) (t' s
y :** PL t' ss
ys) = t s -> t' s -> a
forall (s :: k). t s -> t' s -> a
f t s
x t' s
t' s
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
forall k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
zipList t s -> t' s -> a
forall (s :: k). t s -> t' s -> a
f PL t ss
xs PL t' ss
PL t' ss
ys

zipList2 :: (forall (s :: k) . t s -> t' s -> a) ->
	PL2 t ss -> PL2 t' ss -> [[a]]
zipList2 :: forall k (t :: k -> *) (t' :: k -> *) a (ss :: [[k]]).
(forall (s :: k). t s -> t' s -> a)
-> PL2 t ss -> PL2 t' ss -> [[a]]
zipList2 forall (s :: k). t s -> t' s -> a
f = (forall (s :: [k]). PL t s -> PL t' s -> [a])
-> PL (PL t) ss -> PL (PL t') ss -> [[a]]
forall k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
zipList ((forall (s :: [k]). PL t s -> PL t' s -> [a])
 -> PL (PL t) ss -> PL (PL t') ss -> [[a]])
-> (forall (s :: [k]). PL t s -> PL t' s -> [a])
-> PL (PL t) ss
-> PL (PL t') ss
-> [[a]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> a) -> PL t s -> PL t' s -> [a]
forall k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
zipList t s -> t' s -> a
forall (s :: k). t s -> t' s -> a
f

zipList3 :: (forall (s :: k) . t s -> t' s -> a) ->
	PL3 t ss -> PL3 t' ss -> [[[a]]]
zipList3 :: forall k (t :: k -> *) (t' :: k -> *) a (ss :: [[[k]]]).
(forall (s :: k). t s -> t' s -> a)
-> PL3 t ss -> PL3 t' ss -> [[[a]]]
zipList3 forall (s :: k). t s -> t' s -> a
f = (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> [[a]])
-> PL (PL2 t) ss -> PL (PL2 t') ss -> [[[a]]]
forall k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> t' s -> a) -> PL t ss -> PL t' ss -> [a]
zipList ((forall (s :: [[k]]). PL2 t s -> PL2 t' s -> [[a]])
 -> PL (PL2 t) ss -> PL (PL2 t') ss -> [[[a]]])
-> (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> [[a]])
-> PL (PL2 t) ss
-> PL (PL2 t') ss
-> [[[a]]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> a) -> PL2 t s -> PL2 t' s -> [[a]]
forall k (t :: k -> *) (t' :: k -> *) a (ss :: [[k]]).
(forall (s :: k). t s -> t' s -> a)
-> PL2 t ss -> PL2 t' ss -> [[a]]
zipList2 t s -> t' s -> a
forall (s :: k). t s -> t' s -> a
f

zipListM :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL t ss -> PL t' ss -> m [a]
zipListM :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
zipListM forall (s :: k). t s -> t' s -> m a
_ PL t ss
Nil PL t' ss
Nil = [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
zipListM forall (s :: k). t s -> t' s -> m a
f (t s
x :** PL t ss
xs) (t' s
y :** PL t' ss
ys) = (:) (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f t s
x t' s
t' s
y m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
zipListM t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f PL t ss
xs PL t' ss
PL t' ss
ys

zipListM2 :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL2 t ss -> PL2 t' ss -> m [[a]]
zipListM2 :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL2 t ss -> PL2 t' ss -> m [[a]]
zipListM2 forall (s :: k). t s -> t' s -> m a
f = (forall (s :: [k]). PL t s -> PL t' s -> m [a])
-> PL (PL t) ss -> PL (PL t') ss -> m [[a]]
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
zipListM ((forall (s :: [k]). PL t s -> PL t' s -> m [a])
 -> PL (PL t) ss -> PL (PL t') ss -> m [[a]])
-> (forall (s :: [k]). PL t s -> PL t' s -> m [a])
-> PL (PL t) ss
-> PL (PL t') ss
-> m [[a]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> m a) -> PL t s -> PL t' s -> m [a]
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
zipListM t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f

zipListM3 :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL3 t ss -> PL3 t' ss -> m [[[a]]]
zipListM3 :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[[k]]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL3 t ss -> PL3 t' ss -> m [[[a]]]
zipListM3 forall (s :: k). t s -> t' s -> m a
f = (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m [[a]])
-> PL (PL2 t) ss -> PL (PL2 t') ss -> m [[[a]]]
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m [a]
zipListM ((forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m [[a]])
 -> PL (PL2 t) ss -> PL (PL2 t') ss -> m [[[a]]])
-> (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m [[a]])
-> PL (PL2 t) ss
-> PL (PL2 t') ss
-> m [[[a]]]
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> m a)
-> PL2 t s -> PL2 t' s -> m [[a]]
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL2 t ss -> PL2 t' ss -> m [[a]]
zipListM2 t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f

zipListM_ :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL t ss -> PL t' ss -> m ()
zipListM_ :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
zipListM_ forall (s :: k). t s -> t' s -> m a
_ PL t ss
Nil PL t' ss
Nil = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
zipListM_ forall (s :: k). t s -> t' s -> m a
f (t s
x :** PL t ss
xs) (t' s
y :** PL t' ss
ys) = t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f t s
x t' s
t' s
y m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
zipListM_ t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f PL t ss
xs PL t' ss
PL t' ss
ys

zipListM2_ :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL2 t ss -> PL2 t' ss -> m ()
zipListM2_ :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL2 t ss -> PL2 t' ss -> m ()
zipListM2_ forall (s :: k). t s -> t' s -> m a
f = (forall (s :: [k]). PL t s -> PL t' s -> m ())
-> PL (PL t) ss -> PL (PL t') ss -> m ()
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
zipListM_ ((forall (s :: [k]). PL t s -> PL t' s -> m ())
 -> PL (PL t) ss -> PL (PL t') ss -> m ())
-> (forall (s :: [k]). PL t s -> PL t' s -> m ())
-> PL (PL t) ss
-> PL (PL t') ss
-> m ()
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> m a) -> PL t s -> PL t' s -> m ()
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
zipListM_ t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f

zipListM3_ :: Applicative m =>
	(forall (s :: k) . t s -> t' s -> m a) ->
	PL3 t ss -> PL3 t' ss -> m ()
zipListM3_ :: forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[[k]]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL3 t ss -> PL3 t' ss -> m ()
zipListM3_ forall (s :: k). t s -> t' s -> m a
f = (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m ())
-> PL (PL2 t) ss -> PL (PL2 t') ss -> m ()
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL t ss -> PL t' ss -> m ()
zipListM_ ((forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m ())
 -> PL (PL2 t) ss -> PL (PL2 t') ss -> m ())
-> (forall (s :: [[k]]). PL2 t s -> PL2 t' s -> m ())
-> PL (PL2 t) ss
-> PL (PL2 t') ss
-> m ()
forall a b. (a -> b) -> a -> b
$ (forall (s :: k). t s -> t' s -> m a)
-> PL (PL t) s -> PL (PL t') s -> m ()
forall (m :: * -> *) k (t :: k -> *) (t' :: k -> *) a
       (ss :: [[k]]).
Applicative m =>
(forall (s :: k). t s -> t' s -> m a)
-> PL2 t ss -> PL2 t' ss -> m ()
zipListM2_ t s -> t' s -> m a
forall (s :: k). t s -> t' s -> m a
f

class HomoList (s :: k) ss where
	homoListFromList :: [t s] -> PL t ss
	homoListToList :: PL t ss -> [t s]

instance HomoList s '[] where
	homoListFromList :: forall (t :: k -> *). [t s] -> PL t '[]
homoListFromList = \case [] -> PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil; [t s]
_ -> String -> PL t '[]
forall a. HasCallStack => String -> a
error String
"bad"
	homoListToList :: forall (t :: k -> *). PL t '[] -> [t s]
homoListToList PL t '[]
Nil = []

instance HomoList s ss => HomoList s (s ': ss) where
	homoListFromList :: forall (t :: a -> *). [t s] -> PL t (s : ss)
homoListFromList =
		\case t s
x : [t s]
xs -> t s
x t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** [t s] -> PL t ss
forall k (s :: k) (ss :: [k]) (t :: k -> *).
HomoList s ss =>
[t s] -> PL t ss
forall (t :: a -> *). [t s] -> PL t ss
homoListFromList [t s]
xs; [t s]
_ -> String -> PL t (s : ss)
forall a. HasCallStack => String -> a
error String
"bad"
	homoListToList :: forall (t :: a -> *). PL t (s : ss) -> [t s]
homoListToList (t s
x :** PL t ss
xs) = t s
t s
x t s -> [t s] -> [t s]
forall a. a -> [a] -> [a]
: PL t ss -> [t s]
forall k (s :: k) (ss :: [k]) (t :: k -> *).
HomoList s ss =>
PL t ss -> [t s]
forall (t :: a -> *). PL t ss -> [t s]
homoListToList PL t ss
xs

-- Homo List With Num

class HomoListN (n :: Num k) where
	type Replicate n (s :: k') :: [k']
	homoListNFromList :: [t s] -> PL t (Replicate n s)
	mapHomoListNM :: Monad m => (t a -> m (u b)) ->
		PL t (Replicate n a) -> m (PL u (Replicate n b))
	mapHomoListNMWithI :: Monad m => Int -> (Int -> t a -> m (u b)) ->
		PL t (Replicate n a) -> m (PL u (Replicate n b))
	zipWithHomoListNM :: Monad m => (t a -> u b -> m (v c)) ->
		PL t (Replicate n a) -> PL u (Replicate n b) ->
		m (PL v (Replicate n c))
	zipWithHomoListNM_ :: Monad m => (t a -> u b -> m c) ->
		PL t (Replicate n a) -> PL u (Replicate n b) ->
		m ()

instance HomoListN '[] where
	type Replicate '[] s = '[]
	homoListNFromList :: forall {k'} (t :: k' -> *) (s :: k').
[t s] -> PL t (Replicate '[] s)
homoListNFromList = \case [] -> PL t '[]
PL t (Replicate '[] s)
forall {k} (t :: k -> *). PL t '[]
Nil; [t s]
_ -> String -> PL t '[]
forall a. HasCallStack => String -> a
error String
"bad"
	mapHomoListNM :: forall {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k').
Monad m =>
(t a -> m (u b))
-> PL t (Replicate '[] a) -> m (PL u (Replicate '[] b))
mapHomoListNM t a -> m (u b)
_ PL t (Replicate '[] a)
Nil = PL u '[] -> m (PL u '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL u '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	mapHomoListNMWithI :: forall {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k').
Monad m =>
Int
-> (Int -> t a -> m (u b))
-> PL t (Replicate '[] a)
-> m (PL u (Replicate '[] b))
mapHomoListNMWithI Int
_ Int -> t a -> m (u b)
_ PL t (Replicate '[] a)
Nil = PL u '[] -> m (PL u '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL u '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	zipWithHomoListNM :: forall {k'} {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k') (v :: k' -> *) (c :: k').
Monad m =>
(t a -> u b -> m (v c))
-> PL t (Replicate '[] a)
-> PL u (Replicate '[] b)
-> m (PL v (Replicate '[] c))
zipWithHomoListNM t a -> u b -> m (v c)
_ PL t (Replicate '[] a)
Nil PL u (Replicate '[] b)
Nil = PL v '[] -> m (PL v '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL v '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	zipWithHomoListNM_ :: forall {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k') c.
Monad m =>
(t a -> u b -> m c)
-> PL t (Replicate '[] a) -> PL u (Replicate '[] b) -> m ()
zipWithHomoListNM_ t a -> u b -> m c
_ PL t (Replicate '[] a)
Nil PL u (Replicate '[] b)
Nil = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance HomoListN ds => HomoListN (d ': ds) where
	type Replicate (d ': ds) s = s ': Replicate ds s
	homoListNFromList :: forall {k'} (t :: k' -> *) (s :: k').
[t s] -> PL t (Replicate (d : ds) s)
homoListNFromList = \case
		(t s
x : [t s]
xs) -> t s
x t s -> PL t (Replicate ds s) -> PL t (s : Replicate ds s)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** (forall k (n :: Num k) {k'} (t :: k' -> *) (s :: k').
HomoListN n =>
[t s] -> PL t (Replicate n s)
homoListNFromList @_ @ds [t s]
xs); [t s]
_ -> String -> PL t (s : Replicate ds s)
forall a. HasCallStack => String -> a
error String
"bad"
	mapHomoListNM :: forall t a u b m . Monad m =>
		(t a -> m (u b)) -> PL t (Replicate (d ': ds) a) ->
		m (PL u (Replicate (d ': ds) b))
	mapHomoListNM :: forall {k'} {k'} (t :: k' -> *) (a :: k') (u :: k' -> *) (b :: k')
       (m :: * -> *).
Monad m =>
(t a -> m (u b))
-> PL t (Replicate (d : ds) a) -> m (PL u (Replicate (d : ds) b))
mapHomoListNM t a -> m (u b)
f (t s
x :** PL t ss
xs) = u b -> PL u (Replicate ds b) -> PL u (b : Replicate ds b)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
(:**) (u b -> PL u (Replicate ds b) -> PL u (b : Replicate ds b))
-> m (u b)
-> m (PL u (Replicate ds b) -> PL u (b : Replicate ds b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a -> m (u b)
f t a
t s
x m (PL u (Replicate ds b) -> PL u (b : Replicate ds b))
-> m (PL u (Replicate ds b)) -> m (PL u (b : Replicate ds b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (n :: Num k) {k'} {k'} (m :: * -> *) (t :: k' -> *)
       (a :: k') (u :: k' -> *) (b :: k').
(HomoListN n, Monad m) =>
(t a -> m (u b))
-> PL t (Replicate n a) -> m (PL u (Replicate n b))
mapHomoListNM @_ @ds t a -> m (u b)
f PL t ss
PL t (Replicate ds a)
xs
	mapHomoListNMWithI :: forall t a u b m . Monad m =>
		Int -> (Int -> t a -> m (u b)) ->
		PL t (Replicate (d ': ds) a) ->
		m (PL u (Replicate (d ': ds) b))
	mapHomoListNMWithI :: forall {k'} {k'} (t :: k' -> *) (a :: k') (u :: k' -> *) (b :: k')
       (m :: * -> *).
Monad m =>
Int
-> (Int -> t a -> m (u b))
-> PL t (Replicate (d : ds) a)
-> m (PL u (Replicate (d : ds) b))
mapHomoListNMWithI Int
i Int -> t a -> m (u b)
f (t s
x :** PL t ss
xs) =
		u b -> PL u (Replicate ds b) -> PL u (b : Replicate ds b)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
(:**) (u b -> PL u (Replicate ds b) -> PL u (b : Replicate ds b))
-> m (u b)
-> m (PL u (Replicate ds b) -> PL u (b : Replicate ds b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> t a -> m (u b)
f Int
i t a
t s
x m (PL u (Replicate ds b) -> PL u (b : Replicate ds b))
-> m (PL u (Replicate ds b)) -> m (PL u (b : Replicate ds b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (n :: Num k) {k'} {k'} (m :: * -> *) (t :: k' -> *)
       (a :: k') (u :: k' -> *) (b :: k').
(HomoListN n, Monad m) =>
Int
-> (Int -> t a -> m (u b))
-> PL t (Replicate n a)
-> m (PL u (Replicate n b))
mapHomoListNMWithI @_ @ds (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> t a -> m (u b)
f PL t ss
PL t (Replicate ds a)
xs
	zipWithHomoListNM :: forall {k'} {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k') (v :: k' -> *) (c :: k').
Monad m =>
(t a -> u b -> m (v c))
-> PL t (Replicate (d : ds) a)
-> PL u (Replicate (d : ds) b)
-> m (PL v (Replicate (d : ds) c))
zipWithHomoListNM t a -> u b -> m (v c)
a (t s
x :** PL t ss
xs) (u s
y :** PL u ss
ys) =
		v c -> PL v (Replicate ds c) -> PL v (c : Replicate ds c)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
(:**) (v c -> PL v (Replicate ds c) -> PL v (c : Replicate ds c))
-> m (v c)
-> m (PL v (Replicate ds c) -> PL v (c : Replicate ds c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a -> u b -> m (v c)
a t a
t s
x u b
u s
y m (PL v (Replicate ds c) -> PL v (c : Replicate ds c))
-> m (PL v (Replicate ds c)) -> m (PL v (c : Replicate ds c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (n :: Num k) {k'} {k'} {k'} (m :: * -> *) (t :: k' -> *)
       (a :: k') (u :: k' -> *) (b :: k') (v :: k' -> *) (c :: k').
(HomoListN n, Monad m) =>
(t a -> u b -> m (v c))
-> PL t (Replicate n a)
-> PL u (Replicate n b)
-> m (PL v (Replicate n c))
zipWithHomoListNM @_ @ds t a -> u b -> m (v c)
a PL t ss
PL t (Replicate ds a)
xs PL u ss
PL u (Replicate ds b)
ys
	zipWithHomoListNM_ :: forall {k'} {k'} (m :: * -> *) (t :: k' -> *) (a :: k')
       (u :: k' -> *) (b :: k') c.
Monad m =>
(t a -> u b -> m c)
-> PL t (Replicate (d : ds) a)
-> PL u (Replicate (d : ds) b)
-> m ()
zipWithHomoListNM_ t a -> u b -> m c
a (t s
x :** PL t ss
xs) (u s
y :** PL u ss
ys) =
		t a -> u b -> m c
a t a
t s
x u b
u s
y m c -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall k (n :: Num k) {k'} {k'} (m :: * -> *) (t :: k' -> *)
       (a :: k') (u :: k' -> *) (b :: k') c.
(HomoListN n, Monad m) =>
(t a -> u b -> m c)
-> PL t (Replicate n a) -> PL u (Replicate n b) -> m ()
zipWithHomoListNM_ @_ @ds t a -> u b -> m c
a PL t ss
PL t (Replicate ds a)
xs PL u ss
PL u (Replicate ds b)
ys

type Num a = [a]

tnum :: [a] -> (forall (n :: Num ()) . HomoListN n => Proxy n -> b) -> b
tnum :: forall a b.
[a] -> (forall (n :: [()]). HomoListN n => Proxy n -> b) -> b
tnum [] forall (n :: [()]). HomoListN n => Proxy n -> b
f = Proxy '[] -> b
forall (n :: [()]). HomoListN n => Proxy n -> b
f (Proxy '[]
forall {k}. Proxy '[]
forall {k} (t :: k). Proxy t
Proxy :: Proxy '[])
tnum (a
_ : [a]
xs) forall (n :: [()]). HomoListN n => Proxy n -> b
f = [a] -> (forall (n :: [()]). HomoListN n => Proxy n -> b) -> b
forall a b.
[a] -> (forall (n :: [()]). HomoListN n => Proxy n -> b) -> b
tnum [a]
xs \(Proxy n
Proxy :: Proxy n) -> Proxy ('() : n) -> b
forall (n :: [()]). HomoListN n => Proxy n -> b
f (Proxy ('() : n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy ('() ': n))

-- Index

class TypeIndex (obj :: k) objs where typeIndex :: PL t objs -> t obj
instance TypeIndex obj (obj ': objs) where typeIndex :: forall (t :: a -> *). PL t (obj : objs) -> t obj
typeIndex (t s
ln :** PL t ss
_lns) = t obj
t s
ln

instance {-# OVERLAPPABLE #-} TypeIndex obj objs =>
	TypeIndex obj (obj' ': objs) where
	typeIndex :: forall (t :: a -> *). PL t (obj' : objs) -> t obj
typeIndex (t s
_ :** PL t ss
lns) = forall k (obj :: k) (objs :: [k]) (t :: k -> *).
TypeIndex obj objs =>
PL t objs -> t obj
typeIndex @_ @obj @objs PL t objs
PL t ss
lns

index :: Integral i => PL t ss -> i -> (forall s . t s -> a) -> a
index :: forall {k} i (t :: k -> *) (ss :: [k]) a.
Integral i =>
PL t ss -> i -> (forall (s :: k). t s -> a) -> a
index PL t ss
Nil i
_ forall (s :: k). t s -> a
_ = String -> a
forall a. HasCallStack => String -> a
error String
"index too large"
index (t s
x :** PL t ss
_) i
0 forall (s :: k). t s -> a
f = t s -> a
forall (s :: k). t s -> a
f t s
x
index (t s
_ :** PL t ss
xs) i
i forall (s :: k). t s -> a
f | i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
> i
0 = PL t ss -> i -> (forall (s :: k). t s -> a) -> a
forall {k} i (t :: k -> *) (ss :: [k]) a.
Integral i =>
PL t ss -> i -> (forall (s :: k). t s -> a) -> a
index PL t ss
xs (i
i i -> i -> i
forall a. Num a => a -> a -> a
- i
1) t s -> a
forall (s :: k). t s -> a
f
index PL t ss
_ i
_ forall (s :: k). t s -> a
_ = String -> a
forall a. HasCallStack => String -> a
error String
"negative index"

homoListIndex :: forall s {t} {ss} {i} .
	(HomoList s ss, Integral i) => PL t ss -> i -> t s
homoListIndex :: forall {k} (s :: k) {t :: k -> *} {ss :: [k]} {i}.
(HomoList s ss, Integral i) =>
PL t ss -> i -> t s
homoListIndex PL t ss
xs i
i = PL t ss -> [t s]
forall k (s :: k) (ss :: [k]) (t :: k -> *).
HomoList s ss =>
PL t ss -> [t s]
forall (t :: k -> *). PL t ss -> [t s]
homoListToList PL t ss
xs [t s] -> i -> t s
forall i a. Integral i => [a] -> i -> a
`genericIndex` i
i

-- Map and Replicate

map :: (forall s . t s -> t' s) -> PL t ss -> PL t' ss
map :: forall {k} (t :: k -> *) (t' :: k -> *) (ss :: [k]).
(forall (s :: k). t s -> t' s) -> PL t ss -> PL t' ss
map forall (s :: k). t s -> t' s
f = \case
	PL t ss
Nil -> PL t' ss
PL t' '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	t s
x :** PL t ss
xs -> t s -> t' s
forall (s :: k). t s -> t' s
f t s
x t' s -> PL t' ss -> PL t' (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** (forall (s :: k). t s -> t' s) -> PL t ss -> PL t' ss
forall {k} (t :: k -> *) (t' :: k -> *) (ss :: [k]).
(forall (s :: k). t s -> t' s) -> PL t ss -> PL t' ss
map t s -> t' s
forall (s :: k). t s -> t' s
f PL t ss
xs

mapM :: Applicative m => (forall s . t s -> m (t' s)) -> PL t ss -> m (PL t' ss)
mapM :: forall {k} (m :: * -> *) (t :: k -> *) (t' :: k -> *) (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m (t' s)) -> PL t ss -> m (PL t' ss)
mapM forall (s :: k). t s -> m (t' s)
f = \case
	PL t ss
Nil -> PL t' ss -> m (PL t' ss)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL t' ss
PL t' '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	t s
x :** PL t ss
xs -> t' s -> PL t' ss -> PL t' ss
t' s -> PL t' ss -> PL t' (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
(:**) (t' s -> PL t' ss -> PL t' ss)
-> m (t' s) -> m (PL t' ss -> PL t' ss)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> m (t' s)
forall (s :: k). t s -> m (t' s)
f t s
x m (PL t' ss -> PL t' ss) -> m (PL t' ss) -> m (PL t' ss)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (s :: k). t s -> m (t' s)) -> PL t ss -> m (PL t' ss)
forall {k} (m :: * -> *) (t :: k -> *) (t' :: k -> *) (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m (t' s)) -> PL t ss -> m (PL t' ss)
mapM t s -> m (t' s)
forall (s :: k). t s -> m (t' s)
f PL t ss
xs

mapM_ :: Applicative m => (forall s . t s -> m a) -> PL t ss -> m ()
mapM_ :: forall {k} (m :: * -> *) (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
mapM_ forall (s :: k). t s -> m a
f = \case
	PL t ss
Nil -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
	t s
x :** PL t ss
xs -> t s -> m a
forall (s :: k). t s -> m a
f t s
x m a -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (forall (s :: k). t s -> m a) -> PL t ss -> m ()
forall {k} (m :: * -> *) (t :: k -> *) a (ss :: [k]).
Applicative m =>
(forall (s :: k). t s -> m a) -> PL t ss -> m ()
mapM_ t s -> m a
forall (s :: k). t s -> m a
f PL t ss
xs

class MapM' (f :: k -> k') ss where
	type Ss' f ss :: [k']
	mapM' :: Applicative m => (forall s . t s -> m (t' (f s))) ->
		PL t ss -> m (PL t' (Ss' f ss))

instance MapM' f '[] where type Ss' f '[] = '[]; mapM' :: forall (m :: * -> *) (t :: k -> *) (t' :: k' -> *).
Applicative m =>
(forall (s :: k). t s -> m (t' (f s)))
-> PL t '[] -> m (PL t' (Ss' f '[]))
mapM' forall (s :: k). t s -> m (t' (f s))
_ PL t '[]
Nil = PL t' '[] -> m (PL t' '[])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL t' '[]
forall {k} (t :: k -> *). PL t '[]
Nil

instance MapM' f ss => MapM' f (s ': ss) where
	type Ss' f (s ': ss) = f s ': Ss' f ss
	mapM' :: forall (m :: * -> *) (t :: a -> *) (t' :: k' -> *).
Applicative m =>
(forall (s :: a). t s -> m (t' (f s)))
-> PL t (s : ss) -> m (PL t' (Ss' f (s : ss)))
mapM' forall (s :: a). t s -> m (t' (f s))
g (t s
x :** PL t ss
xs) = t' (f s) -> PL t' (Ss' f ss) -> PL t' (f s : Ss' f ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
(:**) (t' (f s) -> PL t' (Ss' f ss) -> PL t' (f s : Ss' f ss))
-> m (t' (f s)) -> m (PL t' (Ss' f ss) -> PL t' (f s : Ss' f ss))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> m (t' (f s))
forall (s :: a). t s -> m (t' (f s))
g t s
x m (PL t' (Ss' f ss) -> PL t' (f s : Ss' f ss))
-> m (PL t' (Ss' f ss)) -> m (PL t' (f s : Ss' f ss))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (s :: a). t s -> m (t' (f s)))
-> PL t ss -> m (PL t' (Ss' f ss))
forall k k' (f :: k -> k') (ss :: [k]) (m :: * -> *) (t :: k -> *)
       (t' :: k' -> *).
(MapM' f ss, Applicative m) =>
(forall (s :: k). t s -> m (t' (f s)))
-> PL t ss -> m (PL t' (Ss' f ss))
forall (m :: * -> *) (t :: a -> *) (t' :: k' -> *).
Applicative m =>
(forall (s :: a). t s -> m (t' (f s)))
-> PL t ss -> m (PL t' (Ss' f ss))
mapM' t s -> m (t' (f s))
forall (s :: a). t s -> m (t' (f s))
g PL t ss
xs

class Rep n where
	rep :: (forall a . (forall s . t s -> a) -> a) ->
		(forall ss . PL t ss -> b) -> b

instance Rep 0 where rep :: forall {k} (t :: k -> *) b.
(forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b) -> b
rep forall a. (forall (s :: k). t s -> a) -> a
_ forall (ss :: [k]). PL t ss -> b
f = PL t '[] -> b
forall (ss :: [k]). PL t ss -> b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil

instance {-# OVERLAPPABLE #-} Rep (n - 1) => Rep n where
	rep :: forall {k} (t :: k -> *) b.
(forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b) -> b
rep forall a. (forall (s :: k). t s -> a) -> a
x forall (ss :: [k]). PL t ss -> b
f = (forall (s :: k). t s -> b) -> b
forall a. (forall (s :: k). t s -> a) -> a
x \t s
v -> forall (n :: Natural) {k} (t :: k -> *) b.
Rep n =>
(forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b) -> b
forall {k} (n :: k) {k} (t :: k -> *) b.
Rep n =>
(forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b) -> b
rep @(n - 1) (forall (s :: k). t s -> a) -> a
forall a. (forall (s :: k). t s -> a) -> a
x \PL t ss
vs -> PL t (s : ss) -> b
forall (ss :: [k]). PL t ss -> b
f (PL t (s : ss) -> b) -> PL t (s : ss) -> b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

class RepM n where
	repM :: (forall a . (forall s . t s -> m a) -> m a) ->
		(forall ss . PL t ss -> m b) -> m b

instance RepM 0 where repM :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM forall (a :: k). (forall (s :: k). t s -> m a) -> m a
_ forall (ss :: [k]). PL t ss -> m b
f = PL t '[] -> m b
forall (ss :: [k]). PL t ss -> m b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil

instance {-# OVERLAPPABLE #-} RepM (n - 1) => RepM n where
	repM :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x forall (ss :: [k]). PL t ss -> m b
f = (forall (s :: k). t s -> m b) -> m b
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \t s
v -> forall (n :: Natural) {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
RepM n =>
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
forall {k} (n :: k) {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
RepM n =>
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM @(n - 1) (forall (s :: k). t s -> m a) -> m a
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \PL t ss
vs -> PL t (s : ss) -> m b
forall (ss :: [k]). PL t ss -> m b
f (PL t (s : ss) -> m b) -> PL t (s : ss) -> m b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

instance RepM '[] where repM :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM forall (a :: k). (forall (s :: k). t s -> m a) -> m a
_ forall (ss :: [k]). PL t ss -> m b
f = PL t '[] -> m b
forall (ss :: [k]). PL t ss -> m b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil

instance {-# OVERLAPPABLE #-} RepM n => RepM ('() ': n) where
	repM :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x forall (ss :: [k]). PL t ss -> m b
f = (forall (s :: k). t s -> m b) -> m b
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \t s
v -> forall (n :: [()]) {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
RepM n =>
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
forall {k} (n :: k) {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
RepM n =>
(forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b) -> m b
repM @n (forall (s :: k). t s -> m a) -> m a
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \PL t ss
vs -> PL t (s : ss) -> m b
forall (ss :: [k]). PL t ss -> m b
f (PL t (s : ss) -> m b) -> PL t (s : ss) -> m b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

replicate :: Int -> (forall a . (forall s . t s -> a) -> a) ->
	(forall ss . PL t ss -> b) -> b
replicate :: forall {k} (t :: k -> *) b.
Int
-> (forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b)
-> b
replicate Int
0 forall a. (forall (s :: k). t s -> a) -> a
_ forall (ss :: [k]). PL t ss -> b
f = PL t '[] -> b
forall (ss :: [k]). PL t ss -> b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil
replicate Int
n forall a. (forall (s :: k). t s -> a) -> a
x forall (ss :: [k]). PL t ss -> b
f = (forall (s :: k). t s -> b) -> b
forall a. (forall (s :: k). t s -> a) -> a
x \t s
v -> Int
-> (forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b)
-> b
forall {k} (t :: k -> *) b.
Int
-> (forall a. (forall (s :: k). t s -> a) -> a)
-> (forall (ss :: [k]). PL t ss -> b)
-> b
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (forall (s :: k). t s -> a) -> a
forall a. (forall (s :: k). t s -> a) -> a
x \PL t ss
vs -> PL t (s : ss) -> b
forall (ss :: [k]). PL t ss -> b
f (PL t (s : ss) -> b) -> PL t (s : ss) -> b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

replicateM :: Int -> (forall a . (forall s . t s -> m a) -> m a) ->
	(forall ss . PL t ss -> m b) -> m b
replicateM :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> (forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
replicateM Int
0 forall (a :: k). (forall (s :: k). t s -> m a) -> m a
_ forall (ss :: [k]). PL t ss -> m b
f = PL t '[] -> m b
forall (ss :: [k]). PL t ss -> m b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil
replicateM Int
n forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x forall (ss :: [k]). PL t ss -> m b
f = (forall (s :: k). t s -> m b) -> m b
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \t s
v -> Int
-> (forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> (forall (a :: k). (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
replicateM (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (forall (s :: k). t s -> m a) -> m a
forall (a :: k). (forall (s :: k). t s -> m a) -> m a
x \PL t ss
vs ->
	PL t (s : ss) -> m b
forall (ss :: [k]). PL t ss -> m b
f (PL t (s : ss) -> m b) -> PL t (s : ss) -> m b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

replicateMWithI :: Int -> (forall a . Int -> (forall s . t s -> m a) -> m a) ->
	(forall ss . PL t ss -> m b) -> m b
replicateMWithI :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
replicateMWithI = Int
-> Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
go Int
0
	where
	go :: Int -> Int -> (forall a . Int -> (forall s . t s -> m a) -> m a) ->
		(forall ss . PL t ss -> m b) -> m b
	go :: forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
go Int
_ Int
0 forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a
_ forall (ss :: [k]). PL t ss -> m b
f = PL t '[] -> m b
forall (ss :: [k]). PL t ss -> m b
f PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil
	go Int
i Int
n forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a
x forall (ss :: [k]). PL t ss -> m b
f = Int -> (forall (s :: k). t s -> m b) -> m b
forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a
x Int
i \t s
v -> Int
-> Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
forall {k} {k} (t :: k -> *) (m :: k -> *) (b :: k).
Int
-> Int
-> (forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a)
-> (forall (ss :: [k]). PL t ss -> m b)
-> m b
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> (forall (s :: k). t s -> m a) -> m a
forall (a :: k). Int -> (forall (s :: k). t s -> m a) -> m a
x \PL t ss
vs -> PL t (s : ss) -> m b
forall (ss :: [k]). PL t ss -> m b
f (PL t (s : ss) -> m b) -> PL t (s : ss) -> m b
forall a b. (a -> b) -> a -> b
$ t s
v t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
vs

-- Default

instance Default (PL t '[]) where def :: PL t '[]
def = PL t '[]
forall {k} (t :: k -> *). PL t '[]
Nil

instance (Default (t s), Default (PL t ss)) => Default (PL t (s ': ss)) where
	def :: PL t (s : ss)
def = t s
forall a. Default a => a
def t s -> PL t ss -> PL t (s : ss)
forall {k} (t :: k -> *) (s :: k) (ss :: [k]).
t s -> PL t ss -> PL t (s : ss)
:** PL t ss
forall a. Default a => a
def

instance Default a => Default (Id a) where def :: Id a
def = a -> Id a
forall a. a -> Id a
Id a
forall a. Default a => a
def

instance Default a => Default (Dummy a d) where def :: Dummy a d
def = a -> Dummy a d
forall a (d :: ()). a -> Dummy a d
Dummy a
forall a. Default a => a
def

-- Flatten

class ToListWithC c ss where
	toListWithC :: (forall s . c s => t s -> a) -> PL t ss -> [a]

instance ToListWithC c '[] where toListWithC :: forall (t :: k -> *) a.
(forall (s :: k). c s => t s -> a) -> PL t '[] -> [a]
toListWithC forall (s :: k). c s => t s -> a
_ PL t '[]
Nil = []

instance (c s, ToListWithC c ss) => ToListWithC c (s ': ss) where
	toListWithC :: forall (t :: a -> *) a.
(forall (s :: a). c s => t s -> a) -> PL t (s : ss) -> [a]
toListWithC forall (s :: a). c s => t s -> a
f (t s
x :** PL t ss
xs) = t s -> a
forall (s :: a). c s => t s -> a
f t s
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: forall {k} (c :: k -> Constraint) (ss :: [k]) (t :: k -> *) a.
ToListWithC c ss =>
(forall (s :: k). c s => t s -> a) -> PL t ss -> [a]
forall (c :: a -> Constraint) (ss :: [a]) (t :: a -> *) a.
ToListWithC c ss =>
(forall (s :: a). c s => t s -> a) -> PL t ss -> [a]
toListWithC @c t s -> a
forall (s :: a). c s => t s -> a
f PL t ss
xs

class ToListWithC2 c sss where
	toListWithC2 :: (forall s . c s => t s -> a) -> PL2 t sss -> [[a]]

instance ToListWithC2 c '[] where toListWithC2 :: forall (t :: k -> *) a.
(forall (s :: k). c s => t s -> a) -> PL2 t '[] -> [[a]]
toListWithC2 forall (s :: k). c s => t s -> a
_ PL (PL t) '[]
Nil = []

instance (ToListWithC c ss, ToListWithC2 c sss) =>
	ToListWithC2 c (ss ': sss) where
	toListWithC2 :: forall (t :: k -> *) a.
(forall (s :: k). c s => t s -> a) -> PL2 t (ss : sss) -> [[a]]
toListWithC2 forall (s :: k). c s => t s -> a
f (PL t s
xs :** PL (PL t) ss
xss) =
		forall {k} (c :: k -> Constraint) (ss :: [k]) (t :: k -> *) a.
ToListWithC c ss =>
(forall (s :: k). c s => t s -> a) -> PL t ss -> [a]
forall (c :: k -> Constraint) (ss :: [k]) (t :: k -> *) a.
ToListWithC c ss =>
(forall (s :: k). c s => t s -> a) -> PL t ss -> [a]
toListWithC @c t s -> a
forall (s :: k). c s => t s -> a
f PL t s
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: forall {k} (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *) a.
ToListWithC2 c sss =>
(forall (s :: k). c s => t s -> a) -> PL2 t sss -> [[a]]
forall (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *) a.
ToListWithC2 c sss =>
(forall (s :: k). c s => t s -> a) -> PL2 t sss -> [[a]]
toListWithC2 @c t s -> a
forall (s :: k). c s => t s -> a
f PL (PL t) ss
xss

class ZipListWithC c ss where
	zipListWithC :: (forall s . c s => t s -> t' s -> a) ->
		PL t ss -> PL t' ss -> [a]

instance ZipListWithC c '[] where zipListWithC :: forall (t :: k -> *) (t' :: k -> *) a.
(forall (s :: k). c s => t s -> t' s -> a)
-> PL t '[] -> PL t' '[] -> [a]
zipListWithC forall (s :: k). c s => t s -> t' s -> a
_ PL t '[]
Nil PL t' '[]
Nil = []

instance (c s, ZipListWithC c ss) => ZipListWithC c (s ': ss) where
	zipListWithC :: forall (t :: a -> *) (t' :: a -> *) a.
(forall (s :: a). c s => t s -> t' s -> a)
-> PL t (s : ss) -> PL t' (s : ss) -> [a]
zipListWithC forall (s :: a). c s => t s -> t' s -> a
f (t s
x :** PL t ss
xs) (t' s
y :** PL t' ss
ys) = t s -> t' s -> a
forall (s :: a). c s => t s -> t' s -> a
f t s
x t' s
t' s
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: forall {k} (c :: k -> Constraint) (ss :: [k]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC c ss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL t ss -> PL t' ss -> [a]
forall (c :: a -> Constraint) (ss :: [a]) (t :: a -> *)
       (t' :: a -> *) a.
ZipListWithC c ss =>
(forall (s :: a). c s => t s -> t' s -> a)
-> PL t ss -> PL t' ss -> [a]
zipListWithC @c t s -> t' s -> a
forall (s :: a). c s => t s -> t' s -> a
f PL t ss
xs PL t' ss
PL t' ss
ys

class ZipListWithC2 c sss where
	zipListWithC2 :: (forall s . c s => t s -> t' s -> a) ->
		PL2 t sss -> PL2 t' sss -> [[a]]

instance ZipListWithC2 c '[] where zipListWithC2 :: forall (t :: k -> *) (t' :: k -> *) a.
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t '[] -> PL2 t' '[] -> [[a]]
zipListWithC2 forall (s :: k). c s => t s -> t' s -> a
_ PL (PL t) '[]
Nil PL (PL t') '[]
Nil = []

instance (ZipListWithC c ss, ZipListWithC2 c sss) =>
	ZipListWithC2 c (ss ': sss) where
	zipListWithC2 :: forall (t :: k -> *) (t' :: k -> *) a.
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t (ss : sss) -> PL2 t' (ss : sss) -> [[a]]
zipListWithC2 forall (s :: k). c s => t s -> t' s -> a
f (PL t s
xs :** PL (PL t) ss
xss) (PL t' s
ys :** PL (PL t') ss
yss) =
		forall {k} (c :: k -> Constraint) (ss :: [k]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC c ss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL t ss -> PL t' ss -> [a]
forall (c :: k -> Constraint) (ss :: [k]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC c ss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL t ss -> PL t' ss -> [a]
zipListWithC @c t s -> t' s -> a
forall (s :: k). c s => t s -> t' s -> a
f PL t s
xs PL t' s
PL t' s
ys [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: forall {k} (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC2 c sss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t sss -> PL2 t' sss -> [[a]]
forall (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC2 c sss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t sss -> PL2 t' sss -> [[a]]
zipListWithC2 @c t s -> t' s -> a
forall (s :: k). c s => t s -> t' s -> a
f PL (PL t) ss
xss PL2 t' ss
PL (PL t') ss
yss

class ZipListWithC3 c ssss where
	zipListWithC3 :: (forall s . c s => t s -> t' s -> a) ->
		PL3 t ssss -> PL3 t' ssss -> [[[a]]]

instance ZipListWithC3 c '[] where zipListWithC3 :: forall (t :: k -> *) (t' :: k -> *) a.
(forall (s :: k). c s => t s -> t' s -> a)
-> PL3 t '[] -> PL3 t' '[] -> [[[a]]]
zipListWithC3 forall (s :: k). c s => t s -> t' s -> a
_ PL (PL2 t) '[]
Nil PL (PL2 t') '[]
Nil = []

instance (ZipListWithC2 c sss, ZipListWithC3 c ssss) =>
	ZipListWithC3 c (sss ': ssss) where
	zipListWithC3 :: forall (t :: k -> *) (t' :: k -> *) a.
(forall (s :: k). c s => t s -> t' s -> a)
-> PL3 t (sss : ssss) -> PL3 t' (sss : ssss) -> [[[a]]]
zipListWithC3 forall (s :: k). c s => t s -> t' s -> a
f (PL2 t s
xss :** PL (PL2 t) ss
xsss) (PL2 t' s
yss :** PL (PL2 t') ss
ysss) =
		forall {k} (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC2 c sss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t sss -> PL2 t' sss -> [[a]]
forall (c :: k -> Constraint) (sss :: [[k]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC2 c sss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL2 t sss -> PL2 t' sss -> [[a]]
zipListWithC2 @c t s -> t' s -> a
forall (s :: k). c s => t s -> t' s -> a
f PL2 t s
xss PL2 t' s
PL2 t' s
yss [[a]] -> [[[a]]] -> [[[a]]]
forall a. a -> [a] -> [a]
: forall {k} (c :: k -> Constraint) (ssss :: [[[k]]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC3 c ssss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL3 t ssss -> PL3 t' ssss -> [[[a]]]
forall (c :: k -> Constraint) (ssss :: [[[k]]]) (t :: k -> *)
       (t' :: k -> *) a.
ZipListWithC3 c ssss =>
(forall (s :: k). c s => t s -> t' s -> a)
-> PL3 t ssss -> PL3 t' ssss -> [[[a]]]
zipListWithC3 @c t s -> t' s -> a
forall (s :: k). c s => t s -> t' s -> a
f PL (PL2 t) ss
xsss PL3 t' ss
PL (PL2 t') ss
ysss

class ToListWithCM c ss where
	toListWithCM :: Applicative m =>
		(forall s . c s => t s -> m a) -> PL t ss -> m [a]

instance ToListWithCM c '[] where toListWithCM :: forall (m :: * -> *) (t :: k -> *) a.
Applicative m =>
(forall (s :: k). c s => t s -> m a) -> PL t '[] -> m [a]
toListWithCM forall (s :: k). c s => t s -> m a
_ PL t '[]
Nil = [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

instance (c s, ToListWithCM c ss) => ToListWithCM c (s ': ss) where
	toListWithCM :: forall (m :: * -> *) (t :: a -> *) a.
Applicative m =>
(forall (s :: a). c s => t s -> m a) -> PL t (s : ss) -> m [a]
toListWithCM forall (s :: a). c s => t s -> m a
f (t s
x :** PL t ss
xs) = (:) (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> m a
forall (s :: a). c s => t s -> m a
f t s
x m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (c :: k -> Constraint) (ss :: [k]) (m :: * -> *)
       (t :: k -> *) a.
(ToListWithCM c ss, Applicative m) =>
(forall (s :: k). c s => t s -> m a) -> PL t ss -> m [a]
forall (c :: a -> Constraint) (ss :: [a]) (m :: * -> *)
       (t :: a -> *) a.
(ToListWithCM c ss, Applicative m) =>
(forall (s :: a). c s => t s -> m a) -> PL t ss -> m [a]
toListWithCM @c t s -> m a
forall (s :: a). c s => t s -> m a
f PL t ss
xs

class ToListWithCM' c (t' :: k -> k') (ss :: [k]) where
	toListWithCM' :: Applicative m =>
		(forall (s :: k) . c (t' s) => t s -> m a) -> PL t ss -> m [a]

instance ToListWithCM' c t' '[] where toListWithCM' :: forall (m :: * -> *) (t :: k -> *) a.
Applicative m =>
(forall (s :: k). c (t' s) => t s -> m a) -> PL t '[] -> m [a]
toListWithCM' forall (s :: k). c (t' s) => t s -> m a
_ PL t '[]
Nil = [a] -> m [a]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

instance (c (t' s), ToListWithCM' c t' ss) =>
	ToListWithCM' c t' (s ': ss) where
	toListWithCM' :: forall (m :: * -> *) (t :: a -> *) a.
Applicative m =>
(forall (s :: a). c (t' s) => t s -> m a) -> PL t (s : ss) -> m [a]
toListWithCM' forall (s :: a). c (t' s) => t s -> m a
f (t s
x :** PL t ss
xs) =
		(:) (a -> [a] -> [a]) -> m a -> m ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t s -> m a
forall (s :: a). c (t' s) => t s -> m a
f t s
x m ([a] -> [a]) -> m [a] -> m [a]
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k k' (c :: k' -> Constraint) (t' :: k -> k') (ss :: [k])
       (m :: * -> *) (t :: k -> *) a.
(ToListWithCM' c t' ss, Applicative m) =>
(forall (s :: k). c (t' s) => t s -> m a) -> PL t ss -> m [a]
toListWithCM' @_ @_ @c @t' t s -> m a
forall (s :: a). c (t' s) => t s -> m a
f PL t ss
xs

class ToListWithCCpsM c ns where
	toListWithCCpsM ::
		(forall s . c s => t s -> (a -> m b) -> m b) -> PL t ns ->
		([a] -> m b) -> m b

instance ToListWithCCpsM c '[] where toListWithCCpsM :: forall {k} (t :: k -> *) a (m :: k -> *) (b :: k).
(forall (s :: k). c s => t s -> (a -> m b) -> m b)
-> PL t '[] -> ([a] -> m b) -> m b
toListWithCCpsM forall (s :: k). c s => t s -> (a -> m b) -> m b
_ PL t '[]
Nil [a] -> m b
g = [a] -> m b
g []

instance (c n, ToListWithCCpsM c ns) =>
	ToListWithCCpsM c (n ': ns) where
	toListWithCCpsM :: forall {k} (t :: a -> *) a (m :: k -> *) (b :: k).
(forall (s :: a). c s => t s -> (a -> m b) -> m b)
-> PL t (n : ns) -> ([a] -> m b) -> m b
toListWithCCpsM forall (s :: a). c s => t s -> (a -> m b) -> m b
f (t s
x :** PL t ss
xs) [a] -> m b
g =
		t s -> (a -> m b) -> m b
forall (s :: a). c s => t s -> (a -> m b) -> m b
f t s
x \a
y -> forall {k} (c :: k -> Constraint) (ns :: [k]) {k} (t :: k -> *) a
       (m :: k -> *) (b :: k).
ToListWithCCpsM c ns =>
(forall (s :: k). c s => t s -> (a -> m b) -> m b)
-> PL t ns -> ([a] -> m b) -> m b
forall (c :: a -> Constraint) (ns :: [a]) {k} (t :: a -> *) a
       (m :: k -> *) (b :: k).
ToListWithCCpsM c ns =>
(forall (s :: a). c s => t s -> (a -> m b) -> m b)
-> PL t ns -> ([a] -> m b) -> m b
toListWithCCpsM @c t s -> (a -> m b) -> m b
forall (s :: a). c s => t s -> (a -> m b) -> m b
f PL t ss
xs \[a]
ys -> [a] -> m b
g ([a] -> m b) -> [a] -> m b
forall a b. (a -> b) -> a -> b
$ a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys

class ToListWithCCpsM' c (t' :: k -> k') (ns :: [k]) where
	toListWithCCpsM' ::
		(forall (s :: k) . c (t' s) => t s -> (a -> m b) -> m b) ->
		PL t ns -> ([a] -> m b) -> m b

instance ToListWithCCpsM' c t' '[] where toListWithCCpsM' :: forall {k} (t :: k -> *) a (m :: k -> *) (b :: k).
(forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b)
-> PL t '[] -> ([a] -> m b) -> m b
toListWithCCpsM' forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b
_ PL t '[]
Nil = (([a] -> m b) -> [a] -> m b
forall a b. (a -> b) -> a -> b
$ [])

instance (c (t' n), ToListWithCCpsM' c t' ns) =>
	ToListWithCCpsM' c t' (n ': ns) where
	toListWithCCpsM' :: forall {k} (t :: a -> *) a (m :: k -> *) (b :: k).
(forall (s :: a). c (t' s) => t s -> (a -> m b) -> m b)
-> PL t (n : ns) -> ([a] -> m b) -> m b
toListWithCCpsM' forall (s :: a). c (t' s) => t s -> (a -> m b) -> m b
f (t s
x :** PL t ss
xs) [a] -> m b
g =
		t s -> (a -> m b) -> m b
forall (s :: a). c (t' s) => t s -> (a -> m b) -> m b
f t s
x \a
y -> forall k k' (c :: k' -> Constraint) (t' :: k -> k') (ns :: [k]) {k}
       (t :: k -> *) a (m :: k -> *) (b :: k).
ToListWithCCpsM' c t' ns =>
(forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b)
-> PL t ns -> ([a] -> m b) -> m b
toListWithCCpsM' @_ @_ @c @t' t s -> (a -> m b) -> m b
forall (s :: a). c (t' s) => t s -> (a -> m b) -> m b
f PL t ss
xs \[a]
ys -> [a] -> m b
g ([a] -> m b) -> [a] -> m b
forall a b. (a -> b) -> a -> b
$ a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys

withListWithCCpsM' :: forall k c t' ns t m a b .
	ToListWithCCpsM' c t' ns =>
	PL t ns ->
	(forall (s :: k) . c (t' s) => t s -> (a -> m b) -> m b) ->
	([a] -> m b) -> m b
withListWithCCpsM' :: forall {k'} {k} k (c :: k' -> Constraint) (t' :: k -> k')
       (ns :: [k]) (t :: k -> *) (m :: k -> *) a (b :: k).
ToListWithCCpsM' c t' ns =>
PL t ns
-> (forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b)
-> ([a] -> m b)
-> m b
withListWithCCpsM' PL t ns
xs forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b
f = forall k k' (c :: k' -> Constraint) (t' :: k -> k') (ns :: [k]) {k}
       (t :: k -> *) a (m :: k -> *) (b :: k).
ToListWithCCpsM' c t' ns =>
(forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b)
-> PL t ns -> ([a] -> m b) -> m b
toListWithCCpsM' @_ @_ @c @t' t s -> (a -> m b) -> m b
forall (s :: k). c (t' s) => t s -> (a -> m b) -> m b
f PL t ns
xs