module Cascade.Util.ListKind where
import GHC.Prim (Constraint)
type family All (c :: a -> Constraint) (xs :: [a]) :: Constraint where
All c '[] = ()
All c (a ': as) = (c a, All c as)
type family Last (ts :: [a]) :: a where
Last '[a] = a
Last (a ': as) = Last as
type family Map (f :: a -> b) (ts :: [a]) :: [b] where
Map f '[] = '[]
Map f (a ': as) = f a ': Map f as
type family Tails (as :: [a]) :: [[a]] where
Tails '[] = '[ '[] ]
Tails (a ': as) = (a ': as) ': Tails as
type family Tail (as :: [a]) :: [a] where
Tail (a ': as) = as
type family Init (as :: [a]) :: [a] where
Init '[a] = '[]
Init (a ': as) = a ': Init as
type family RInits (as :: [a]) :: [[a]] where
RInits '[] = '[ '[] ]
RInits (a ': as) = '[] ': Map (Snoc a) (RInits as)
type family Snoc (x :: a) (xs :: [a]) :: [a] where
Snoc x '[] = '[x]
Snoc x (a ': as) = a ': Snoc x as
type family ZipWith (f :: a -> b -> c) (as :: [a]) (bs :: [b]) :: [c] where
ZipWith f '[] '[] = '[]
ZipWith f (a ': as) (b ': bs) = f a b ': ZipWith f as bs
type family Concat (as :: [a]) (bs :: [a]) :: [a] where
Concat '[] bs = bs
Concat (a ': as) bs = a ': Concat as bs