{-# 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
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
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
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