{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE NoStarIsType #-}

module Torch.HList where

import Control.Applicative (Applicative (liftA2))
import Data.Kind
  ( Type,
  )
import GHC.Exts (IsList (..))
import GHC.TypeLits (Nat, type (+), type (-), type (<=))
import Prelude hiding (id, (.))

type family ListLength (xs :: [k]) :: Nat where
  ListLength '[] = 0
  ListLength (_h ': t) = 1 + ListLength t

data family HList (xs :: [k])

data instance HList '[] = HNil

newtype instance HList ((x :: Type) ': xs) = HCons (x, HList xs)

pattern (:.) :: forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
pattern $b:. :: forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
$m:. :: forall {r} {x} {xs :: [Type]}.
HList (x : xs) -> (x -> HList xs -> r) -> ((# #) -> r) -> r
(:.) x xs = HCons (x, xs)

infixr 2 :.

instance Show (HList '[]) where
  show :: HList '[] -> String
show HList '[]
_ = String
"H[]"

instance (Show e, Show (HList l)) => Show (HList (e ': l)) where
  show :: HList (e : l) -> String
show (e
x :. HList l
l) =
    let Char
'H' : Char
'[' : String
s = forall a. Show a => a -> String
show HList l
l
     in String
"H[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show e
x forall a. [a] -> [a] -> [a]
++ (if String
s forall a. Eq a => a -> a -> Bool
== String
"]" then String
s else String
"," forall a. [a] -> [a] -> [a]
++ String
s)

instance Eq (HList '[]) where
  HList '[]
R:HListk[] k
HNil == :: HList '[] -> HList '[] -> Bool
== HList '[]
R:HListk[] k
HNil = Bool
True

instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs)) where
  (x
x :. HList xs
xs) == :: HList (x : xs) -> HList (x : xs) -> Bool
== (x
y :. HList xs
ys) = x
x forall a. Eq a => a -> a -> Bool
== x
y Bool -> Bool -> Bool
&& HList xs
xs forall a. Eq a => a -> a -> Bool
== HList xs
ys

instance Semigroup (HList '[]) where
  HList '[]
_ <> :: HList '[] -> HList '[] -> HList '[]
<> HList '[]
_ = forall k. HList '[]
HNil

instance (Semigroup a, Semigroup (HList as)) => Semigroup (HList (a ': as)) where
  (a
x :. HList as
xs) <> :: HList (a : as) -> HList (a : as) -> HList (a : as)
<> (a
y :. HList as
ys) = (a
x forall a. Semigroup a => a -> a -> a
<> a
y) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. (HList as
xs forall a. Semigroup a => a -> a -> a
<> HList as
ys)

instance Monoid (HList '[]) where
  mempty :: HList '[]
mempty = forall k. HList '[]
HNil
  mappend :: HList '[] -> HList '[] -> HList '[]
mappend HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil

instance (Monoid a, Monoid (HList as)) => Monoid (HList (a ': as)) where
  mempty :: HList (a : as)
mempty = forall a. Monoid a => a
mempty forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall a. Monoid a => a
mempty
  mappend :: HList (a : as) -> HList (a : as) -> HList (a : as)
mappend (a
x :. HList as
xs) (a
y :. HList as
ys) = forall a. Monoid a => a -> a -> a
mappend a
x a
y forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall a. Monoid a => a -> a -> a
mappend HList as
xs HList as
ys

{- HLINT ignore "Redundant bracket" -}
instance IsList (Maybe (HList '[(a :: Type)])) where
  type Item (Maybe (HList '[(a :: Type)])) = a
  fromList :: [Item (Maybe (HList '[a]))] -> Maybe (HList '[a])
fromList [Item (Maybe (HList '[a]))
x] = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) (forall a. a -> Maybe a
Just Item (Maybe (HList '[a]))
x) (forall a. a -> Maybe a
Just forall k. HList '[]
HNil)
  fromList [Item (Maybe (HList '[a]))]
_ = forall a. Maybe a
Nothing
  toList :: Maybe (HList '[a]) -> [Item (Maybe (HList '[a]))]
toList Maybe (HList '[a])
Nothing = []
  toList (Just (a
x :. HList '[]
R:HListk[] Type
HNil)) = [a
x]

instance
  ( IsList (Maybe (HList (a ': as))),
    a ~ Item (Maybe (HList (a ': as)))
  ) =>
  IsList (Maybe (HList ((a :: Type) ': a ': as)))
  where
  type Item (Maybe (HList (a ': a ': as))) = a
  fromList :: [Item (Maybe (HList (a : a : as)))] -> Maybe (HList (a : a : as))
fromList (Item (Maybe (HList (a : a : as)))
x : [Item (Maybe (HList (a : a : as)))]
xs) = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) (forall a. a -> Maybe a
Just Item (Maybe (HList (a : a : as)))
x) (forall l. IsList l => [Item l] -> l
fromList [Item (Maybe (HList (a : a : as)))]
xs)
  fromList [Item (Maybe (HList (a : a : as)))]
_ = forall a. Maybe a
Nothing
  toList :: Maybe (HList (a : a : as)) -> [Item (Maybe (HList (a : a : as)))]
toList Maybe (HList (a : a : as))
Nothing = []
  toList (Just (a
x :. HList (a : as)
xs)) = a
x forall a. a -> [a] -> [a]
: forall l. IsList l => l -> [Item l]
toList (forall a. a -> Maybe a
Just HList (a : as)
xs)

class Apply f a b where
  apply :: f -> a -> b

-- | Stronger version of `Apply` that allows for better inference of the return type
class Apply' f a b | f a -> b where
  apply' :: f -> a -> b

data AFst = AFst

instance Apply' AFst (a, b) a where
  apply' :: AFst -> (a, b) -> a
apply' AFst
_ (a
a, b
_) = a
a

data ASnd = ASnd

instance Apply' ASnd (a, b) b where
  apply' :: ASnd -> (a, b) -> b
apply' ASnd
_ (a
_, b
b) = b
b

class HMap f (xs :: [k]) (ys :: [k]) where
  hmap :: f -> HList xs -> HList ys

instance HMap f '[] '[] where
  hmap :: f -> HList '[] -> HList '[]
hmap f
_ HList '[]
_ = forall k. HList '[]
HNil

instance (Apply f x y, HMap f xs ys) => HMap f (x ': xs) (y ': ys) where
  hmap :: f -> HList (x : xs) -> HList (y : ys)
hmap f
f (x
x :. HList xs
xs) = forall f a b. Apply f a b => f -> a -> b
apply f
f x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k f (xs :: [k]) (ys :: [k]).
HMap f xs ys =>
f -> HList xs -> HList ys
hmap f
f HList xs
xs

-- | Alternative version of `HMap` with better type inference based on `Apply'`
class HMap' f (xs :: [k]) (ys :: [k]) | f xs -> ys where
  hmap' :: f -> HList xs -> HList ys

instance HMap' f '[] '[] where
  hmap' :: f -> HList '[] -> HList '[]
hmap' f
_ HList '[]
_ = forall k. HList '[]
HNil

instance (Apply' f x y, HMap' f xs ys) => HMap' f (x ': xs) (y ': ys) where
  hmap' :: f -> HList (x : xs) -> HList (y : ys)
hmap' f
f (x
x :. HList xs
xs) = forall f a b. Apply' f a b => f -> a -> b
apply' f
f x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k f (xs :: [k]) (ys :: [k]).
HMap' f xs ys =>
f -> HList xs -> HList ys
hmap' f
f HList xs
xs

class HMapM m f (xs :: [k]) (ys :: [k]) where
  hmapM :: f -> HList xs -> m (HList ys)

instance (Monad m) => HMapM m f '[] '[] where
  hmapM :: f -> HList '[] -> m (HList '[])
hmapM f
_ HList '[]
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall k. HList '[]
HNil

instance
  ( Monad m,
    Apply f x (m y),
    HMapM m f xs ys
  ) =>
  HMapM m f (x ': xs) (y ': ys)
  where
  hmapM :: f -> HList (x : xs) -> m (HList (y : ys))
hmapM f
f (x
x :. HList xs
xs) = forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall f a b. Apply f a b => f -> a -> b
apply f
f x
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k (m :: Type -> Type) f (xs :: [k]) (ys :: [k]).
HMapM m f xs ys =>
f -> HList xs -> m (HList ys)
hmapM f
f HList xs
xs

class HMapM' m f (xs :: [k]) (ys :: [k]) | f xs -> ys where
  hmapM' :: f -> HList xs -> m (HList ys)

instance (Applicative m) => HMapM' m f '[] '[] where
  hmapM' :: f -> HList '[] -> m (HList '[])
hmapM' f
_ HList '[]
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall k. HList '[]
HNil

instance
  ( Applicative m,
    Apply' f x (m y),
    HMapM' m f xs ys
  ) =>
  HMapM' m f (x ': xs) (y ': ys)
  where
  hmapM' :: f -> HList (x : xs) -> m (HList (y : ys))
hmapM' f
f (x
x :. HList xs
xs) = forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall f a b. Apply' f a b => f -> a -> b
apply' f
f x
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k (m :: Type -> Type) f (xs :: [k]) (ys :: [k]).
HMapM' m f xs ys =>
f -> HList xs -> m (HList ys)
hmapM' f
f HList xs
xs

class
  Applicative f =>
  HSequence f (xs :: [k]) (ys :: [k])
    | xs -> ys,
      ys f -> xs
  where
  hsequence :: HList xs -> f (HList ys)

instance Applicative f => HSequence f '[] '[] where
  hsequence :: HList '[] -> f (HList '[])
hsequence = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure

instance
  ( Applicative g,
    HSequence f xs ys,
    y ~ x,
    f ~ g
  ) =>
  HSequence g (f x ': xs) (y ': ys)
  where
  hsequence :: HList (f x : xs) -> g (HList (y : ys))
hsequence (f x
fx :. HList xs
fxs) = forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f x
fx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k (f :: Type -> Type) (xs :: [k]) (ys :: [k]).
HSequence f xs ys =>
HList xs -> f (HList ys)
hsequence HList xs
fxs

class HFoldr f acc xs res | f acc xs -> res where
  hfoldr :: f -> acc -> HList xs -> res

instance (acc ~ res) => HFoldr f acc '[] res where
  hfoldr :: f -> acc -> HList '[] -> res
hfoldr f
_ acc
acc HList '[]
_ = acc
acc

instance
  ( Apply' f (x, res) res',
    HFoldr f acc xs res
  ) =>
  HFoldr f acc (x ': xs) res'
  where
  hfoldr :: f -> acc -> HList (x : xs) -> res'
hfoldr f
f acc
acc (x
x :. HList xs
xs) = forall f a b. Apply' f a b => f -> a -> b
apply' f
f (x
x, forall {k} f acc (xs :: [k]) res.
HFoldr f acc xs res =>
f -> acc -> HList xs -> res
hfoldr f
f acc
acc HList xs
xs)

class HFoldrM m f acc xs res | m f acc xs -> res where
  hfoldrM :: f -> acc -> HList xs -> m res

instance
  ( Monad m,
    acc ~ res
  ) =>
  HFoldrM m f acc '[] res
  where
  hfoldrM :: f -> acc -> HList '[] -> m res
hfoldrM f
_ acc
acc HList '[]
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure acc
acc

instance
  ( Monad m,
    Apply' f (x, m res) (m res'),
    HFoldrM m f acc xs res
  ) =>
  HFoldrM m f acc (x ': xs) res'
  where
  hfoldrM :: f -> acc -> HList (x : xs) -> m res'
hfoldrM f
f acc
acc (x
x :. HList xs
xs) = forall f a b. Apply' f a b => f -> a -> b
apply' f
f (x
x, forall {k} {k} (m :: k -> Type) f acc (xs :: [k]) (res :: k).
HFoldrM m f acc xs res =>
f -> acc -> HList xs -> m res
hfoldrM f
f acc
acc HList xs
xs :: (m res))

data HNothing = HNothing

newtype HJust x = HJust x

class HUnfold f res xs where
  hunfoldr' :: f -> res -> HList xs

type family HUnfoldRes s xs where
  HUnfoldRes _ '[] = HNothing
  HUnfoldRes s (x ': _) = HJust (x, s)

instance HUnfold f HNothing '[] where
  hunfoldr' :: f -> HNothing -> HList '[]
hunfoldr' f
_ HNothing
_ = forall k. HList '[]
HNil

instance
  ( Apply f s res,
    HUnfold f res xs,
    res ~ HUnfoldRes s xs
  ) =>
  HUnfold f (HJust (x, s)) (x ': xs)
  where
  hunfoldr' :: f -> HJust (x, s) -> HList (x : xs)
hunfoldr' f
f (HJust (x
x, s
s)) = x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall {k} f res (xs :: [k]).
HUnfold f res xs =>
f -> res -> HList xs
hunfoldr' f
f (forall f a b. Apply f a b => f -> a -> b
apply f
f s
s :: res)

hunfoldr ::
  forall f res (xs :: [Type]) a.
  (Apply f a res, HUnfold f res xs, res ~ HUnfoldRes a xs) =>
  f ->
  a ->
  HList xs
hunfoldr :: forall f res (xs :: [Type]) a.
(Apply f a res, HUnfold f res xs, res ~ HUnfoldRes a xs) =>
f -> a -> HList xs
hunfoldr f
f a
s = forall {k} f res (xs :: [k]).
HUnfold f res xs =>
f -> res -> HList xs
hunfoldr' f
f (forall f a b. Apply f a b => f -> a -> b
apply f
f a
s :: res)

class HUnfoldM m f res xs where
  hunfoldrM' :: f -> res -> m (HList xs)

type family HUnfoldMRes m s xs where
  HUnfoldMRes m _ '[] = m HNothing
  HUnfoldMRes m s (x ': _) = m (HJust (x, s))

instance (Monad m) => HUnfoldM m f (m HNothing) '[] where
  hunfoldrM' :: f -> m HNothing -> m (HList '[])
hunfoldrM' f
_ m HNothing
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall k. HList '[]
HNil

instance
  ( Monad m,
    HUnfoldM m f res xs,
    Apply f s res,
    res ~ HUnfoldMRes m s xs
  ) =>
  HUnfoldM m f (m (HJust (x, s))) (x ': xs)
  where
  hunfoldrM' :: f -> m (HJust (x, s)) -> m (HList (x : xs))
hunfoldrM' f
f m (HJust (x, s))
just = do
    HJust (x
x, s
s) <- m (HJust (x, s))
just
    HList xs
xs <- forall {k} (m :: Type -> Type) f res (xs :: [k]).
HUnfoldM m f res xs =>
f -> res -> m (HList xs)
hunfoldrM' f
f (forall f a b. Apply f a b => f -> a -> b
apply f
f s
s :: res)
    forall (m :: Type -> Type) a. Monad m => a -> m a
return (x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList xs
xs)

hunfoldrM ::
  forall (m :: Type -> Type) f res (xs :: [Type]) a.
  (HUnfoldM m f res xs, Apply f a res, res ~ HUnfoldMRes m a xs) =>
  f ->
  a ->
  m (HList xs)
hunfoldrM :: forall (m :: Type -> Type) f res (xs :: [Type]) a.
(HUnfoldM m f res xs, Apply f a res, res ~ HUnfoldMRes m a xs) =>
f -> a -> m (HList xs)
hunfoldrM f
f a
s = forall {k} (m :: Type -> Type) f res (xs :: [k]).
HUnfoldM m f res xs =>
f -> res -> m (HList xs)
hunfoldrM' f
f (forall f a b. Apply f a b => f -> a -> b
apply f
f a
s :: res)

type HReplicate n e = HReplicateFD n e (HReplicateR n e)

hreplicate :: forall n e. HReplicate n e => e -> HList (HReplicateR n e)
hreplicate :: forall (n :: Nat) e. HReplicate n e => e -> HList (HReplicateR n e)
hreplicate = forall (n :: Nat) e (es :: [Type]).
HReplicateFD n e es =>
e -> HList es
hreplicateFD @n

class
  HReplicateFD
    (n :: Nat)
    (e :: Type)
    (es :: [Type])
    | n e -> es
  where
  hreplicateFD :: e -> HList es

instance {-# OVERLAPS #-} HReplicateFD 0 e '[] where
  hreplicateFD :: e -> HList '[]
hreplicateFD e
_ = forall k. HList '[]
HNil

instance
  {-# OVERLAPPABLE #-}
  ( HReplicateFD (n - 1) e es,
    es' ~ (e ': es),
    1 <= n
  ) =>
  HReplicateFD n e es'
  where
  hreplicateFD :: e -> HList es'
hreplicateFD e
e = e
e forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall (n :: Nat) e (es :: [Type]).
HReplicateFD n e es =>
e -> HList es
hreplicateFD @(n - 1) e
e

type family HReplicateR (n :: Nat) (e :: a) :: [a] where
  HReplicateR 0 _ = '[]
  HReplicateR n e = e ': HReplicateR (n - 1) e

type HConcat xs = HConcatFD xs (HConcatR xs)

hconcat :: HConcat xs => HList xs -> HList (HConcatR xs)
hconcat :: forall (xs :: [Type]).
HConcat xs =>
HList xs -> HList (HConcatR xs)
hconcat = forall k (xxs :: [k]) (xs :: [k]).
HConcatFD xxs xs =>
HList xxs -> HList xs
hconcatFD

type family HConcatR (a :: [Type]) :: [Type]

type instance HConcatR '[] = '[]

type instance HConcatR (x ': xs) = UnHList x ++ HConcatR xs

type family UnHList a :: [Type]

type instance UnHList (HList a) = a

class HConcatFD (xxs :: [k]) (xs :: [k]) | xxs -> xs where
  hconcatFD :: HList xxs -> HList xs

instance HConcatFD '[] '[] where
  hconcatFD :: HList '[] -> HList '[]
hconcatFD HList '[]
_ = forall k. HList '[]
HNil

instance (HConcatFD as bs, HAppendFD a bs cs) => HConcatFD (HList a ': as) cs where
  hconcatFD :: HList (HList a : as) -> HList cs
hconcatFD (HList a
x :. HList as
xs) = HList a
x forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
`happendFD` forall k (xxs :: [k]) (xs :: [k]).
HConcatFD xxs xs =>
HList xxs -> HList xs
hconcatFD HList as
xs

type HAppend as bs = HAppendFD as bs (as ++ bs)

happend :: HAppend as bs => HList as -> HList bs -> HList (as ++ bs)
happend :: forall {k} (as :: [k]) (bs :: [k]).
HAppend as bs =>
HList as -> HList bs -> HList (as ++ bs)
happend = forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
happendFD

hunappend ::
  ( cs ~ (as ++ bs),
    HAppend as bs
  ) =>
  HList cs ->
  (HList as, HList bs)
hunappend :: forall {k} (cs :: [k]) (as :: [k]) (bs :: [k]).
(cs ~ (as ++ bs), HAppend as bs) =>
HList cs -> (HList as, HList bs)
hunappend = forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList ab -> (HList a, HList b)
hunappendFD

class HAppendFD (a :: [k]) (b :: [k]) (ab :: [k]) | a b -> ab, a ab -> b where
  happendFD :: HList a -> HList b -> HList ab
  hunappendFD :: HList ab -> (HList a, HList b)

type family (as :: [k]) ++ (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': as ++ bs

instance HAppendFD '[] b b where
  happendFD :: HList '[] -> HList b -> HList b
happendFD HList '[]
_ HList b
b = HList b
b
  hunappendFD :: HList b -> (HList '[], HList b)
hunappendFD HList b
b = (forall k. HList '[]
HNil, HList b
b)

instance
  ( HAppendFD as bs cs
  ) =>
  HAppendFD (a ': as :: [Type]) bs (a ': cs :: [Type])
  where
  happendFD :: HList (a : as) -> HList bs -> HList (a : cs)
happendFD (a
a :. HList as
as) HList bs
bs = a
a forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
happendFD HList as
as HList bs
bs
  hunappendFD :: HList (a : cs) -> (HList (a : as), HList bs)
hunappendFD (a
a :. HList cs
cs) = let (HList as
as, HList bs
bs) = forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList ab -> (HList a, HList b)
hunappendFD HList cs
cs in (a
a forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList as
as, HList bs
bs)

class HZip (xs :: [k]) (ys :: [k]) (zs :: [k]) | xs ys -> zs, zs -> xs ys where
  hzip :: HList xs -> HList ys -> HList zs
  hunzip :: HList zs -> (HList xs, HList ys)

instance HZip '[] '[] '[] where
  hzip :: HList '[] -> HList '[] -> HList '[]
hzip HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil
  hunzip :: HList '[] -> (HList '[], HList '[])
hunzip HList '[]
_ = (forall k. HList '[]
HNil, forall k. HList '[]
HNil)

instance ((x, y) ~ z, HZip xs ys zs) => HZip (x ': xs) (y ': ys) (z ': zs) where
  hzip :: HList (x : xs) -> HList (y : ys) -> HList (z : zs)
hzip (x
x :. HList xs
xs) (y
y :. HList ys
ys) = (x
x, y
y) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZip xs ys zs =>
HList xs -> HList ys -> HList zs
hzip HList xs
xs HList ys
ys
  hunzip :: HList (z : zs) -> (HList (x : xs), HList (y : ys))
hunzip (~(x
x, y
y) :. HList zs
zs) = let ~(HList xs
xs, HList ys
ys) = forall k (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZip xs ys zs =>
HList zs -> (HList xs, HList ys)
hunzip HList zs
zs in (x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList xs
xs, y
y forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList ys
ys)

class HZip' (xs :: [k]) (ys :: [k]) (zs :: [k]) | xs ys -> zs where
  hzip' :: HList xs -> HList ys -> HList zs

instance HZip' '[] '[] '[] where
  hzip' :: HList '[] -> HList '[] -> HList '[]
hzip' HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil

instance
  ( HList (x ': y) ~ z,
    HZip' xs ys zs
  ) =>
  HZip' (x ': xs) (HList y ': ys) (z ': zs)
  where
  hzip' :: HList (x : xs) -> HList (HList y : ys) -> HList (z : zs)
hzip' (x
x :. HList xs
xs) (HList y
y :. HList ys
ys) = (x
x forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList y
y) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZip' xs ys zs =>
HList xs -> HList ys -> HList zs
hzip' HList xs
xs HList ys
ys

data HZipF = HZipF

instance
  ( HZip' a b c,
    x ~ (HList a, HList b),
    y ~ HList c
  ) =>
  Apply' HZipF x y
  where
  apply' :: HZipF -> x -> y
apply' HZipF
_ (HList a
x, HList b
y) = forall k (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZip' xs ys zs =>
HList xs -> HList ys -> HList zs
hzip' HList a
x HList b
y

htranspose ::
  forall (acc :: [Type]) (xs :: [Type]) (xxs :: [Type]) (res :: Type).
  ( HReplicateFD (ListLength xs) (HList ('[] :: [Type])) acc,
    HFoldr HZipF (HList acc) (HList xs : xxs) res
  ) =>
  HList (HList xs : xxs) ->
  res
htranspose :: forall (acc :: [Type]) (xs :: [Type]) (xxs :: [Type]) res.
(HReplicateFD (ListLength xs) (HList '[]) acc,
 HFoldr HZipF (HList acc) (HList xs : xxs) res) =>
HList (HList xs : xxs) -> res
htranspose (HList xs
xs :. HList xxs
xxs) =
  forall {k} f acc (xs :: [k]) res.
HFoldr f acc xs res =>
f -> acc -> HList xs -> res
hfoldr
    HZipF
HZipF
    (forall (n :: Nat) e (es :: [Type]).
HReplicateFD n e es =>
e -> HList es
hreplicateFD @(ListLength xs) (forall k. HList '[]
HNil :: HList ('[] :: [Type])))
    (HList xs
xs forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList xxs
xxs)

class HZipWith f (xs :: [k]) (ys :: [k]) (zs :: [k]) | f xs ys -> zs where
  hzipWith :: f -> HList xs -> HList ys -> HList zs

instance HZipWith f '[] '[] '[] where
  hzipWith :: f -> HList '[] -> HList '[] -> HList '[]
hzipWith f
_ HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil

instance
  ( Apply' f (x, y) z,
    HZipWith f xs ys zs
  ) =>
  HZipWith f (x ': xs) (y ': ys) (z ': zs)
  where
  hzipWith :: f -> HList (x : xs) -> HList (y : ys) -> HList (z : zs)
hzipWith f
f (x
x :. HList xs
xs) (y
y :. HList ys
ys) = forall f a b. Apply' f a b => f -> a -> b
apply' f
f (x
x, y
y) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k f (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZipWith f xs ys zs =>
f -> HList xs -> HList ys -> HList zs
hzipWith f
f HList xs
xs HList ys
ys

class HZipWithM m f (xs :: [k]) (ys :: [k]) (zs :: [k]) | f xs ys -> zs where
  hzipWithM :: f -> HList xs -> HList ys -> m (HList zs)

instance (Applicative m) => HZipWithM m f '[] '[] '[] where
  hzipWithM :: f -> HList '[] -> HList '[] -> m (HList '[])
hzipWithM f
_ HList '[]
_ HList '[]
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall k. HList '[]
HNil

instance
  ( Applicative m,
    Apply' f (x, y) (m z),
    HZipWithM m f xs ys zs
  ) =>
  HZipWithM m f (x ': xs) (y ': ys) (z ': zs)
  where
  hzipWithM :: f -> HList (x : xs) -> HList (y : ys) -> m (HList (z : zs))
hzipWithM f
f (x
x :. HList xs
xs) (y
y :. HList ys
ys) = forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
(:.) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall f a b. Apply' f a b => f -> a -> b
apply' f
f (x
x, y
y) forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall k (m :: Type -> Type) f (xs :: [k]) (ys :: [k]) (zs :: [k]).
HZipWithM m f xs ys zs =>
f -> HList xs -> HList ys -> m (HList zs)
hzipWithM f
f HList xs
xs HList ys
ys

class
  HZip3
    (as :: [k])
    (bs :: [k])
    (cs :: [k])
    (ds :: [k])
    | as bs cs -> ds,
      ds -> as bs cs
  where
  hzip3 :: HList as -> HList bs -> HList cs -> HList ds
  hunzip3 :: HList ds -> (HList as, HList bs, HList cs)

instance HZip3 '[] '[] '[] '[] where
  hzip3 :: HList '[] -> HList '[] -> HList '[] -> HList '[]
hzip3 HList '[]
_ HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil
  hunzip3 :: HList '[] -> (HList '[], HList '[], HList '[])
hunzip3 HList '[]
_ = (forall k. HList '[]
HNil, forall k. HList '[]
HNil, forall k. HList '[]
HNil)

instance
  ( (a, b, c) ~ d,
    HZip3 as bs cs ds
  ) =>
  HZip3 (a ': as) (b ': bs) (c ': cs) (d ': ds)
  where
  hzip3 :: HList (a : as)
-> HList (b : bs) -> HList (c : cs) -> HList (d : ds)
hzip3 (a
a :. HList as
as) (b
b :. HList bs
bs) (c
c :. HList cs
cs) = (a
a, b
b, c
c) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
HZip3 as bs cs ds =>
HList as -> HList bs -> HList cs -> HList ds
hzip3 HList as
as HList bs
bs HList cs
cs
  hunzip3 :: HList (d : ds) -> (HList (a : as), HList (b : bs), HList (c : cs))
hunzip3 (~(a
a, b
b, c
c) :. HList ds
ds) =
    let ~(HList as
as, HList bs
bs, HList cs
cs) = forall k (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
HZip3 as bs cs ds =>
HList ds -> (HList as, HList bs, HList cs)
hunzip3 HList ds
ds in (a
a forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList as
as, b
b forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList bs
bs, c
c forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. HList cs
cs)

class
  HZipWith3
    f
    (as :: [k])
    (bs :: [k])
    (cs :: [k])
    (ds :: [k])
    | f as bs cs -> ds
  where
  hzipWith3 :: f -> HList as -> HList bs -> HList cs -> HList ds

instance HZipWith3 f '[] '[] '[] '[] where
  hzipWith3 :: f -> HList '[] -> HList '[] -> HList '[] -> HList '[]
hzipWith3 f
_ HList '[]
_ HList '[]
_ HList '[]
_ = forall k. HList '[]
HNil

instance
  ( Apply' f (a, b, c) d,
    HZipWith3 f as bs cs ds
  ) =>
  HZipWith3 f (a ': as) (b ': bs) (c ': cs) (d ': ds)
  where
  hzipWith3 :: f
-> HList (a : as)
-> HList (b : bs)
-> HList (c : cs)
-> HList (d : ds)
hzipWith3 f
f (a
a :. HList as
as) (b
b :. HList bs
bs) (c
c :. HList cs
cs) = forall f a b. Apply' f a b => f -> a -> b
apply' f
f (a
a, b
b, c
c) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k f (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
HZipWith3 f as bs cs ds =>
f -> HList as -> HList bs -> HList cs -> HList ds
hzipWith3 f
f HList as
as HList bs
bs HList cs
cs

class HCartesianProduct (xs :: [k]) (ys :: [k]) (zs :: [k]) | xs ys -> zs where
  hproduct :: HList xs -> HList ys -> HList zs

instance HCartesianProduct '[] ys '[] where
  hproduct :: HList '[] -> HList ys -> HList '[]
hproduct HList '[]
_ HList ys
_ = forall k. HList '[]
HNil

class HAttach x (ys :: [k]) (zs :: [k]) | x ys -> zs where
  hattach :: x -> HList ys -> HList zs

instance HAttach x '[] '[] where
  hattach :: x -> HList '[] -> HList '[]
hattach x
_ HList '[]
_ = forall k. HList '[]
HNil

instance (HAttach x ys xys) => HAttach x (y ': ys) ((x, y) ': xys) where
  hattach :: x -> HList (y : ys) -> HList ((x, y) : xys)
hattach x
x (y
y :. HList ys
ys) = (x
x, y
y) forall x (xs :: [Type]). x -> HList xs -> HList (x : xs)
:. forall k x (ys :: [k]) (zs :: [k]).
HAttach x ys zs =>
x -> HList ys -> HList zs
hattach x
x HList ys
ys

instance
  ( HCartesianProduct xs ys zs,
    HAttach x ys xys,
    HAppendFD xys zs zs'
  ) =>
  HCartesianProduct (x ': xs) ys zs'
  where
  hproduct :: HList (x : xs) -> HList ys -> HList zs'
hproduct (x
x :. HList xs
xs) HList ys
ys = forall k x (ys :: [k]) (zs :: [k]).
HAttach x ys zs =>
x -> HList ys -> HList zs
hattach x
x HList ys
ys forall k (a :: [k]) (b :: [k]) (ab :: [k]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
`happendFD` forall k (xs :: [k]) (ys :: [k]) (zs :: [k]).
HCartesianProduct xs ys zs =>
HList xs -> HList ys -> HList zs
hproduct HList xs
xs HList ys
ys