packages feed

hetero-parameter-list (empty) → 0.1.0.17

raw patch · 8 files changed

+690/−0 lines, 8 filesdep +basedep +data-defaultdep +template-haskellsetup-changed

Dependencies added: base, data-default, template-haskell, try-hetero-parameter-list

Files

+ CHANGELOG.md view
@@ -0,0 +1,11 @@+# Changelog for `try-hetero-parameter-list`++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to the+[Haskell Package Versioning Policy](https://pvp.haskell.org/).++## Unreleased++## 0.1.0.0 - YYYY-MM-DD
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Yoshikuni Jujo (c) 2023++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Yoshikuni Jujo nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,3 @@+# hetero-parameter-list++hetero list with parameter list
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ hetero-parameter-list.cabal view
@@ -0,0 +1,56 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.37.0.+--+-- see: https://github.com/sol/hpack++name:           hetero-parameter-list+version:        0.1.0.17+synopsis:       hetero list with parameter list+description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/hetero-parameter-list#readme>+category:       Data+homepage:       https://github.com/YoshikuniJujo/try-hetero-parameter-list#readme+bug-reports:    https://github.com/YoshikuniJujo/try-hetero-parameter-list/issues+author:         Yoshikuni Jujo+maintainer:     yoshikuni.jujo@gmail.com+copyright:      2023 Yoshikuni Jujo+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/YoshikuniJujo/try-hetero-parameter-list++library+  exposed-modules:+      Data.HeteroParList+      Data.HeteroParList.Constrained+  other-modules:+      Paths_hetero_parameter_list+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base >=4.7 && <5+    , data-default <1+    , template-haskell <3+  default-language: Haskell2010++test-suite try-hetero-parameter-list-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Paths_hetero_parameter_list+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , data-default <1+    , template-haskell <3+    , try-hetero-parameter-list+  default-language: Haskell2010
+ src/Data/HeteroParList.hs view
@@ -0,0 +1,563 @@+{-# 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 :* xs <- Id x :** xs where x :* xs = Id x :** xs++newtype Id a = Id a deriving 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 :*. xs <- Dummy x :** xs where x :*. xs = Dummy x :** xs++newtype Dummy a (d :: ()) = Dummy a deriving 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 Nil = "Nil"++instance (Show (t s), Show (PL t ss)) =>+	Show (PL t (s ': ss)) where+	show (x :** xs) = show x ++ " :** " ++ show xs++instance Eq (PL t '[]) where Nil == Nil = True++instance (Eq (t s), Eq (PL t ss)) =>+	Eq (PL t (s ': ss)) where+	(x :** xs) == (y :** ys) = x == y && xs == ys++{-# COMPLETE Singleton #-}++pattern Singleton :: t s -> PL t '[s]+pattern Singleton x <- (x :** Nil) where+	Singleton x = x :** Nil++pattern Singleton2 :: t s -> PL2 t '[ '[s]]+pattern Singleton2 x <- Singleton (Singleton x) where+	Singleton2 x = Singleton $ Singleton x++pattern Singleton3 :: t s -> PL3 t '[ '[ '[s]]]+pattern Singleton3 x <- Singleton (Singleton2 x) where+	Singleton3 x = Singleton $ Singleton2 x++pattern Singleton4 :: t s -> PL4 t '[ '[ '[ '[s]]]]+pattern Singleton4 x <- Singleton (Singleton3 x) where+	Singleton4 x = Singleton $ Singleton3 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 _ [] = Nil+	fromList _ _ = error "bad"++instance FromList ss => FromList (s ': ss) where+	fromList f (x : xs) = f x :** fromList f xs+	fromList _ _ = error "bad"++toList :: (forall (s :: k) . t s -> a) -> PL t ss -> [a]+toList _ Nil = []+toList f (x :** xs) = f x : toList f xs+ +toList2 :: (forall (s :: k) . t s -> a) -> PL2 t sss -> [[a]]+toList2 f = toList $ toList f++toList3 :: (forall (s :: k) . t s -> a) -> PL3 t ssss -> [[[a]]]+toList3 f = toList $ toList2 f++toListM :: Applicative m => (forall (s :: k) . t s -> m a) -> PL t ss -> m [a]+toListM _ Nil = pure []+toListM f (x :** xs) = (:) <$> f x <*> toListM f xs++toListM2 :: Applicative m =>+	(forall (s :: k) . t s -> m a) -> PL2 t sss -> m [[a]]+toListM2 f = toListM $ toListM f++toListM3 :: Applicative m =>+	(forall (s :: k) . t s -> m a) -> PL3 t sss -> m [[[a]]]+toListM3 f = toListM $ toListM2 f++toListM_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL t ss -> m ()+toListM_ _ Nil = pure ()+toListM_ f (x :** xs) = f x *> toListM_ f xs++toListM2_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL2 t ss -> m ()+toListM2_ f = toListM_ $ toListM_ f++toListM3_ :: Applicative m => (forall (s :: k) . t s -> m a) -> PL3 t ss -> m ()+toListM3_ f = toListM_ $ toListM2_ 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 _ Nil = []++instance ToListT2 k1 k2 ss => ToListT2 k1 k2 ('(s1, s2) ': ss) where+	toListT2 f (x :** xs) = f x : toListT2 f 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 _ Nil = []++instance ToListT3 k1 k2 k3 ss => ToListT3 k1 k2 k3 ('(s1, s2, s3) ': ss) where+	toListT3 f (x :** xs) = f x : toListT3 f xs++zipToList :: (forall (s :: k) (s' :: k') . t s -> t' s' -> a) ->+	PL t ss -> PL t' ss' -> [a]+zipToList _ Nil _ = []+zipToList _ _ Nil = []+zipToList f (x :** xs) (y :** ys) = f x y : zipToList f xs 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 _ Nil _ _ = []+zip3ToList _ _ Nil _ = []+zip3ToList _ _ _ Nil = []+zip3ToList f (x :** xs) (y :** ys) (z :** zs) = f x y z : zip3ToList f xs ys 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 _ Nil _ _ _ = []+zip4ToList _ _ Nil _ _ = []+zip4ToList _ _ _ Nil _ = []+zip4ToList _ _ _ _ Nil = []+zip4ToList f (x :** xs) (y :** ys) (z :** zs) (w :** ws) =+	f x y z w : zip4ToList f xs ys zs ws++zipList :: (forall (s :: k) . t s -> t' s -> a) ->+	PL t ss -> PL t' ss -> [a]+zipList _ Nil Nil = []+zipList f (x :** xs) (y :** ys) = f x y : zipList f xs ys++zipList2 :: (forall (s :: k) . t s -> t' s -> a) ->+	PL2 t ss -> PL2 t' ss -> [[a]]+zipList2 f = zipList $ zipList f++zipList3 :: (forall (s :: k) . t s -> t' s -> a) ->+	PL3 t ss -> PL3 t' ss -> [[[a]]]+zipList3 f = zipList $ zipList2 f++zipListM :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL t ss -> PL t' ss -> m [a]+zipListM _ Nil Nil = pure []+zipListM f (x :** xs) (y :** ys) = (:) <$> f x y <*> zipListM f xs ys++zipListM2 :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL2 t ss -> PL2 t' ss -> m [[a]]+zipListM2 f = zipListM $ zipListM f++zipListM3 :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL3 t ss -> PL3 t' ss -> m [[[a]]]+zipListM3 f = zipListM $ zipListM2 f++zipListM_ :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL t ss -> PL t' ss -> m ()+zipListM_ _ Nil Nil = pure ()+zipListM_ f (x :** xs) (y :** ys) = f x y *> zipListM_ f xs ys++zipListM2_ :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL2 t ss -> PL2 t' ss -> m ()+zipListM2_ f = zipListM_ $ zipListM_ f++zipListM3_ :: Applicative m =>+	(forall (s :: k) . t s -> t' s -> m a) ->+	PL3 t ss -> PL3 t' ss -> m ()+zipListM3_ f = zipListM_ $ zipListM2_ f++class HomoList (s :: k) ss where+	homoListFromList :: [t s] -> PL t ss+	homoListToList :: PL t ss -> [t s]++instance HomoList s '[] where+	homoListFromList = \case [] -> Nil; _ -> error "bad"+	homoListToList Nil = []++instance HomoList s ss => HomoList s (s ': ss) where+	homoListFromList =+		\case x : xs -> x :** homoListFromList xs; _ -> error "bad"+	homoListToList (x :** xs) = x : homoListToList 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 = \case [] -> Nil; _ -> error "bad"+	mapHomoListNM _ Nil = pure Nil+	mapHomoListNMWithI _ _ Nil = pure Nil+	zipWithHomoListNM _ Nil Nil = pure Nil+	zipWithHomoListNM_ _ Nil Nil = pure ()++instance HomoListN ds => HomoListN (d ': ds) where+	type Replicate (d ': ds) s = s ': Replicate ds s+	homoListNFromList = \case+		(x : xs) -> x :** (homoListNFromList @_ @ds xs); _ -> error "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 f (x :** xs) = (:**) <$> f x <*> mapHomoListNM @_ @ds f 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 i f (x :** xs) =+		(:**) <$> f i x <*> mapHomoListNMWithI @_ @ds (i + 1) f xs+	zipWithHomoListNM a (x :** xs) (y :** ys) =+		(:**) <$> a x y <*> zipWithHomoListNM @_ @ds a xs ys+	zipWithHomoListNM_ a (x :** xs) (y :** ys) =+		a x y >> zipWithHomoListNM_ @_ @ds a xs ys++type Num a = [a]++tnum :: [a] -> (forall (n :: Num ()) . HomoListN n => Proxy n -> b) -> b+tnum [] f = f (Proxy :: Proxy '[])+tnum (_ : xs) f = tnum xs \(Proxy :: Proxy n) -> f (Proxy :: Proxy ('() ': n))++-- Index++class TypeIndex (obj :: k) objs where typeIndex :: PL t objs -> t obj+instance TypeIndex obj (obj ': objs) where typeIndex (ln :** _lns) = ln++instance {-# OVERLAPPABLE #-} TypeIndex obj objs =>+	TypeIndex obj (obj' ': objs) where+	typeIndex (_ :** lns) = typeIndex @_ @obj @objs lns++index :: Integral i => PL t ss -> i -> (forall s . t s -> a) -> a+index Nil _ _ = error "index too large"+index (x :** _) 0 f = f x+index (_ :** xs) i f | i > 0 = index xs (i - 1) f+index _ _ _ = error "negative index"++homoListIndex :: forall s {t} {ss} {i} .+	(HomoList s ss, Integral i) => PL t ss -> i -> t s+homoListIndex xs i = homoListToList xs `genericIndex` i++-- Map and Replicate++map :: (forall s . t s -> t' s) -> PL t ss -> PL t' ss+map f = \case+	Nil -> Nil+	x :** xs -> f x :** map f xs++mapM :: Applicative m => (forall s . t s -> m (t' s)) -> PL t ss -> m (PL t' ss)+mapM f = \case+	Nil -> pure Nil+	x :** xs -> (:**) <$> f x <*> mapM f xs++mapM_ :: Applicative m => (forall s . t s -> m a) -> PL t ss -> m ()+mapM_ f = \case+	Nil -> pure ()+	x :** xs -> f x *> mapM_ f 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' _ Nil = pure Nil++instance MapM' f ss => MapM' f (s ': ss) where+	type Ss' f (s ': ss) = f s ': Ss' f ss+	mapM' g (x :** xs) = (:**) <$> g x <*> mapM' g 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 _ f = f Nil++instance {-# OVERLAPPABLE #-} Rep (n - 1) => Rep n where+	rep x f = x \v -> rep @(n - 1) x \vs -> f $ v :** 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 _ f = f Nil++instance {-# OVERLAPPABLE #-} RepM (n - 1) => RepM n where+	repM x f = x \v -> repM @(n - 1) x \vs -> f $ v :** vs++instance RepM '[] where repM _ f = f Nil++instance {-# OVERLAPPABLE #-} RepM n => RepM ('() ': n) where+	repM x f = x \v -> repM @n x \vs -> f $ v :** vs++replicate :: Int -> (forall a . (forall s . t s -> a) -> a) ->+	(forall ss . PL t ss -> b) -> b+replicate 0 _ f = f Nil+replicate n x f = x \v -> replicate (n - 1) x \vs -> f $ v :** vs++replicateM :: Int -> (forall a . (forall s . t s -> m a) -> m a) ->+	(forall ss . PL t ss -> m b) -> m b+replicateM 0 _ f = f Nil+replicateM n x f = x \v -> replicateM (n - 1) x \vs ->+	f $ v :** vs++replicateMWithI :: Int -> (forall a . Int -> (forall s . t s -> m a) -> m a) ->+	(forall ss . PL t ss -> m b) -> m b+replicateMWithI = go 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 _ 0 _ f = f Nil+	go i n x f = x i \v -> go (i + 1) (n - 1) x \vs -> f $ v :** vs++-- Default++instance Default (PL t '[]) where def = Nil++instance (Default (t s), Default (PL t ss)) => Default (PL t (s ': ss)) where+	def = def :** def++instance Default a => Default (Id a) where def = Id def++instance Default a => Default (Dummy a d) where def = Dummy def++-- Flatten++class ToListWithC c ss where+	toListWithC :: (forall s . c s => t s -> a) -> PL t ss -> [a]++instance ToListWithC c '[] where toListWithC _ Nil = []++instance (c s, ToListWithC c ss) => ToListWithC c (s ': ss) where+	toListWithC f (x :** xs) = f x : toListWithC @c f xs++class ToListWithC2 c sss where+	toListWithC2 :: (forall s . c s => t s -> a) -> PL2 t sss -> [[a]]++instance ToListWithC2 c '[] where toListWithC2 _ Nil = []++instance (ToListWithC c ss, ToListWithC2 c sss) =>+	ToListWithC2 c (ss ': sss) where+	toListWithC2 f (xs :** xss) =+		toListWithC @c f xs : toListWithC2 @c f 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 _ Nil Nil = []++instance (c s, ZipListWithC c ss) => ZipListWithC c (s ': ss) where+	zipListWithC f (x :** xs) (y :** ys) = f x y : zipListWithC @c f xs 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 _ Nil Nil = []++instance (ZipListWithC c ss, ZipListWithC2 c sss) =>+	ZipListWithC2 c (ss ': sss) where+	zipListWithC2 f (xs :** xss) (ys :** yss) =+		zipListWithC @c f xs ys : zipListWithC2 @c f xss 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 _ Nil Nil = []++instance (ZipListWithC2 c sss, ZipListWithC3 c ssss) =>+	ZipListWithC3 c (sss ': ssss) where+	zipListWithC3 f (xss :** xsss) (yss :** ysss) =+		zipListWithC2 @c f xss yss : zipListWithC3 @c f xsss 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 _ Nil = pure []++instance (c s, ToListWithCM c ss) => ToListWithCM c (s ': ss) where+	toListWithCM f (x :** xs) = (:) <$> f x <*> toListWithCM @c f 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' _ Nil = pure []++instance (c (t' s), ToListWithCM' c t' ss) =>+	ToListWithCM' c t' (s ': ss) where+	toListWithCM' f (x :** xs) =+		(:) <$> f x <*> toListWithCM' @_ @_ @c @t' f 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 _ Nil g = g []++instance (c n, ToListWithCCpsM c ns) =>+	ToListWithCCpsM c (n ': ns) where+	toListWithCCpsM f (x :** xs) g =+		f x \y -> toListWithCCpsM @c f xs \ys -> g $ y : 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' _ Nil = ($ [])++instance (c (t' n), ToListWithCCpsM' c t' ns) =>+	ToListWithCCpsM' c t' (n ': ns) where+	toListWithCCpsM' f (x :** xs) g =+		f x \y -> toListWithCCpsM' @_ @_ @c @t' f xs \ys -> g $ y : 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' xs f = toListWithCCpsM' @_ @_ @c @t' f xs
+ src/Data/HeteroParList/Constrained.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds, PolyKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.HeteroParList.Constrained where++import Data.Kind++data PL c (t :: k -> Type) (ss :: [k]) where+	Nil :: PL c t '[]+	(:^*) :: c s => t s -> PL c t ss -> PL c t (s ': ss)++instance Show (PL c t '[]) where show Nil = "Nil"++instance (Show (t s), Show (PL c t ss)) =>+	Show (PL c t (s ': ss)) where+	show (x :^* xs) = show x ++ " :^* " ++ show xs++null :: PL c t ss -> Bool+null = \case Nil -> True; _ :^* _ -> False
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"