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