{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | See 'Telescope' -- -- Intended for qualified import -- -- > import Data.SOP.Telescope (Telescope(..)) -- > import qualified Data.SOP.Telescope as Telescope module Data.SOP.Telescope ( -- * Telescope Telescope (..) , sequence -- ** Utilities , fromTZ , fromTip , tip , toAtMost -- ** Bifunctor analogues of SOP functions , bihap , bihczipWith , bihmap , bihzipWith -- * Extension, retraction, alignment , Extend (..) , Retract (..) , align , extend , retract -- ** Simplified API , alignExtend , alignExtendNS , extendIf , retractIf -- * Additional API , ScanNext (..) , SimpleTelescope (..) , scanl ) where import Data.Coerce (coerce) import Data.Functor.Product import Data.Kind import Data.Proxy import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting import Data.SOP.InPairs (InPairs (..), Requiring (..)) import qualified Data.SOP.InPairs as InPairs import Data.SOP.Strict import Data.SOP.Tails (Tails (..)) import qualified Data.SOP.Tails as Tails import GHC.Stack import NoThunks.Class (NoThunks (..), allNoThunks) import Prelude hiding (scanl, sequence, zipWith) {------------------------------------------------------------------------------- Telescope -------------------------------------------------------------------------------} -- | Telescope -- -- A telescope is an extension of an 'NS', where every time we "go right" in the -- sum we have an additional value. -- -- The 'Telescope' API mostly follows @sop-core@ conventions, supporting -- functor ('hmap', 'hcmap'), applicative ('hap', 'hpure'), foldable -- ('hcollapse') and traversable ('hsequence''). However, since 'Telescope' -- is a bi-functor, it cannot reuse the @sop-core@ classes. The naming scheme -- of the functions is adopted from @sop-core@ though; for example: -- -- > bi h (c) zipWith -- > | | | | -- > | | | \ zipWith: the name from base -- > | | | -- > | | \ constrained: version of the function with a constraint parameter -- > | | -- > | \ higher order: 'Telescope' (like 'NS'/'NP') is a /higher order/ functor -- > | -- > \ bifunctor: 'Telescope' (unlike 'NS'/'NP') is a higher order /bifunctor/ -- -- In addition to the standard SOP operators, the new operators that make -- a 'Telescope' a telescope are 'extend', 'retract' and 'align'; see their -- documentation for details. type Telescope :: (k -> Type) -> (k -> Type) -> [k] -> Type data Telescope g f xs where TZ :: !(f x) -> Telescope g f (x ': xs) TS :: !(g x) -> !(Telescope g f xs) -> Telescope g f (x ': xs) {------------------------------------------------------------------------------- SOP class instances for 'Telescope' -------------------------------------------------------------------------------} type instance Prod (Telescope g) = NP type instance SListIN (Telescope g) = SListI type instance AllN (Telescope g) c = All c instance HAp (Telescope g) where hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]). Prod (Telescope g) (f -.-> g) xs -> Telescope g f xs -> Telescope g g xs hap = (Telescope g f xs -> NP (f -.-> g) xs -> Telescope g g xs) -> NP (f -.-> g) xs -> Telescope g f xs -> Telescope g g xs forall a b c. (a -> b -> c) -> b -> a -> c flip Telescope g f xs -> NP (f -.-> g) xs -> Telescope g g xs forall (f :: k -> *) (xs :: [k]) (f' :: k -> *). Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs go where -- We could define this in terms of 'bihap' but we lack 'SListI' go :: Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs go :: forall (f :: k -> *) (xs :: [k]) (f' :: k -> *). Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs go (TZ f x fx) ((-.->) f f' x f :* NP (f -.-> f') xs1 _) = f' x -> Telescope g f' (x : xs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ ((-.->) f f' x -> f x -> f' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f f' x f f x f x fx) go (TS g x gx Telescope g f xs t) ((-.->) f f' x _ :* NP (f -.-> f') xs1 fs) = g x -> Telescope g f' xs -> Telescope g f' (x : xs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs forall (f :: k -> *) (xs :: [k]) (f' :: k -> *). Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs go Telescope g f xs t NP (f -.-> f') xs NP (f -.-> f') xs1 fs) instance HTraverse_ (Telescope g) where hctraverse_ :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (AllN (Telescope g) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> Telescope g f xs -> g () hctraverse_ proxy c p = proxy c -> (forall (x :: k). c x => g x -> g ()) -> (forall (a :: k). c a => f a -> g ()) -> Telescope g f xs -> g () forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m ()) -> (forall (x :: k). c x => f x -> m ()) -> Telescope g f xs -> m () bihctraverse_ proxy c p (\g x _ -> () -> g () forall a. a -> g a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) htraverse_ :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *). (SListIN (Telescope g) xs, Applicative g) => (forall (a :: k). f a -> g ()) -> Telescope g f xs -> g () htraverse_ = (forall (x :: k). g x -> g ()) -> (forall (a :: k). f a -> g ()) -> Telescope g f xs -> g () forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m ()) -> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m () bihtraverse_ (\g x _ -> () -> g () forall a. a -> g a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) instance HSequence (Telescope g) where hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *). (SListIN (Telescope g) xs, Applicative f) => Telescope g (f :.: g) xs -> f (Telescope g g xs) hsequence' = Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs) forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). (SListI xs, Applicative m) => Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs) bihsequence' (Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs)) -> (Telescope g (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs) -> Telescope g (f :.: g) xs -> f (Telescope g g xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (x :: k). g x -> (:.:) f g x) -> (forall (x :: k). (:.:) f g x -> (:.:) f g x) -> Telescope g (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs forall {k} (xs :: [k]) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). SListI xs => (forall (x :: k). g x -> g' x) -> (forall (x :: k). f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihmap (f (g x) -> (:.:) f g x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (f (g x) -> (:.:) f g x) -> (g x -> f (g x)) -> g x -> (:.:) f g x forall b c a. (b -> c) -> (a -> b) -> a -> c . g x -> f (g x) forall a. a -> f a forall (f :: * -> *) a. Applicative f => a -> f a pure) (:.:) f g x -> (:.:) f g x forall (x :: k). (:.:) f g x -> (:.:) f g x forall a. a -> a id hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Telescope g) c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> Telescope g f xs -> g (Telescope g f' xs) hctraverse' proxy c p = proxy c -> (forall (x :: k). c x => g x -> g (g x)) -> (forall (a :: k). c a => f a -> g (f' a)) -> Telescope g f xs -> g (Telescope g f' xs) forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *) (xs :: [k]). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m (g' x)) -> (forall (x :: k). c x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihctraverse' proxy c p g x -> g (g x) forall (x :: k). c x => g x -> g (g x) forall a. a -> g a forall (f :: * -> *) a. Applicative f => a -> f a pure htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (SListIN (Telescope g) xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> Telescope g f xs -> g (Telescope g f' xs) htraverse' = (forall (x :: k). g x -> g (g x)) -> (forall (a :: k). f a -> g (f' a)) -> Telescope g f xs -> g (Telescope g f' xs) forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m (g' x)) -> (forall (x :: k). f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihtraverse' g x -> g (g x) forall (x :: k). g x -> g (g x) forall a. a -> g a forall (f :: * -> *) a. Applicative f => a -> f a pure -- | Specialization of 'hsequence'' with weaker constraints -- ('Functor' rather than 'Applicative') sequence :: forall m g f xs. Functor m => Telescope g (m :.: f) xs -> m (Telescope g f xs) sequence :: forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Functor m => Telescope g (m :.: f) xs -> m (Telescope g f xs) sequence = Telescope g (m :.: f) xs -> m (Telescope g f xs) forall (xs' :: [k]). Telescope g (m :.: f) xs' -> m (Telescope g f xs') go where go :: Telescope g (m :.: f) xs' -> m (Telescope g f xs') go :: forall (xs' :: [k]). Telescope g (m :.: f) xs' -> m (Telescope g f xs') go (TZ (Comp m (f x) fx)) = f x -> Telescope g f xs' f x -> Telescope g f (x : xs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (f x -> Telescope g f xs') -> m (f x) -> m (Telescope g f xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m (f x) fx go (TS g x gx Telescope g (m :.: f) xs t) = g x -> Telescope g f xs -> Telescope g f (x : xs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f xs -> Telescope g f xs') -> m (Telescope g f xs) -> m (Telescope g f xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Telescope g (m :.: f) xs -> m (Telescope g f xs) forall (xs' :: [k]). Telescope g (m :.: f) xs' -> m (Telescope g f xs') go Telescope g (m :.: f) xs t instance (forall x y. LiftedCoercible g g x y) => HTrans (Telescope g) (Telescope g) where htrans :: forall (c :: k2 -> k2 -> Constraint) (xs :: [k2]) (ys :: [k2]) (proxy :: (k2 -> k2 -> Constraint) -> *) (f :: k2 -> *) (g :: k2 -> *). AllZipN (Prod (Telescope g)) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Telescope g f xs -> Telescope g g ys htrans proxy c p forall (x :: k2) (y :: k2). c x y => f x -> g y transf = \case TZ f x fx -> g (Head ys) -> Telescope g g (Head ys : Tail ys) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (g (Head ys) -> Telescope g g (Head ys : Tail ys)) -> g (Head ys) -> Telescope g g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ f x -> g (Head ys) forall (x :: k2) (y :: k2). c x y => f x -> g y transf f x fx TS g x gx Telescope g f xs t -> g (Head ys) -> Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (g x -> g (Head ys) forall a b. Coercible a b => a -> b coerce g x gx) (Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys)) -> Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Telescope g f xs -> Telescope g g (Tail ys) forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (c :: k1 -> k2 -> Constraint) (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *) (g :: k2 -> *). (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall (x :: k1) (y :: k2). c x y => f x -> g y) -> h1 f xs -> h2 g ys forall (c :: k2 -> k2 -> Constraint) (xs :: [k2]) (ys :: [k2]) (proxy :: (k2 -> k2 -> Constraint) -> *) (f :: k2 -> *) (g :: k2 -> *). AllZipN (Prod (Telescope g)) c xs ys => proxy c -> (forall (x :: k2) (y :: k2). c x y => f x -> g y) -> Telescope g f xs -> Telescope g g ys htrans proxy c p f x -> g y forall (x :: k2) (y :: k2). c x y => f x -> g y transf Telescope g f xs t hcoerce :: forall (f :: k2 -> *) (g :: k2 -> *) (xs :: [k2]) (ys :: [k2]). AllZipN (Prod (Telescope g)) (LiftedCoercible f g) xs ys => Telescope g f xs -> Telescope g g ys hcoerce = \case TZ f x fx -> g (Head ys) -> Telescope g g (Head ys : Tail ys) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (g (Head ys) -> Telescope g g (Head ys : Tail ys)) -> g (Head ys) -> Telescope g g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ f x -> g (Head ys) forall a b. Coercible a b => a -> b coerce f x fx TS g x gx Telescope g f xs t -> g (Head ys) -> Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (g x -> g (Head ys) forall a b. Coercible a b => a -> b coerce g x gx) (Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys)) -> Telescope g g (Tail ys) -> Telescope g g (Head ys : Tail ys) forall a b. (a -> b) -> a -> b $ Telescope g f xs -> Telescope g g (Tail ys) forall k1 l1 k2 l2 (h1 :: (k1 -> *) -> l1 -> *) (h2 :: (k2 -> *) -> l2 -> *) (f :: k1 -> *) (g :: k2 -> *) (xs :: l1) (ys :: l2). (HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) => h1 f xs -> h2 g ys forall (f :: k2 -> *) (g :: k2 -> *) (xs :: [k2]) (ys :: [k2]). AllZipN (Prod (Telescope g)) (LiftedCoercible f g) xs ys => Telescope g f xs -> Telescope g g ys hcoerce Telescope g f xs t type instance Same (Telescope g) = Telescope g {------------------------------------------------------------------------------- Bifunctor analogues of class methods -------------------------------------------------------------------------------} -- | Bifunctor analogue of 'hap' bihap :: NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap :: forall {k} (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *). NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap = \NP (g -.-> g') xs gs NP (f -.-> f') xs fs Telescope g f xs t -> Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]) (g' :: k -> *) (f' :: k -> *). Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs go Telescope g f xs t NP (g -.-> g') xs gs NP (f -.-> f') xs fs where go :: Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs go :: forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]) (g' :: k -> *) (f' :: k -> *). Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs go (TZ f x fx) NP (g -.-> g') xs _ ((-.->) f f' x f :* NP (f -.-> f') xs1 _) = f' x -> Telescope g' f' (x : xs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ ((-.->) f f' x -> f x -> f' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f f' x f f x f x fx) go (TS g x gx Telescope g f xs t) ((-.->) g g' x g :* NP (g -.-> g') xs1 gs) ((-.->) f f' x _ :* NP (f -.-> f') xs1 fs) = g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS ((-.->) g g' x -> g x -> g' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) g g' x g g x g x gx) (Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]) (g' :: k -> *) (f' :: k -> *). Telescope g f xs -> NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g' f' xs go Telescope g f xs t NP (g -.-> g') xs NP (g -.-> g') xs1 gs NP (f -.-> f') xs NP (f -.-> f') xs1 fs) -- | Bifunctor analogue of 'hctraverse'' bihctraverse' :: forall proxy c m g g' f f' xs. (All c xs, Applicative m) => proxy c -> (forall x. c x => g x -> m (g' x)) -> (forall x. c x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihctraverse' :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *) (xs :: [k]). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m (g' x)) -> (forall (x :: k). c x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihctraverse' proxy c _ forall (x :: k). c x => g x -> m (g' x) g forall (x :: k). c x => f x -> m (f' x) f = Telescope g f xs -> m (Telescope g' f' xs) forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m (Telescope g' f' xs') go where go :: All c xs' => Telescope g f xs' -> m (Telescope g' f' xs') go :: forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m (Telescope g' f' xs') go (TZ f x fx) = f' x -> Telescope g' f' xs' f' x -> Telescope g' f' (x : xs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (f' x -> Telescope g' f' xs') -> m (f' x) -> m (Telescope g' f' xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> f x -> m (f' x) forall (x :: k). c x => f x -> m (f' x) f f x fx go (TS g x gx Telescope g f xs t) = g' x -> Telescope g' f' xs -> Telescope g' f' xs' g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (g' x -> Telescope g' f' xs -> Telescope g' f' xs') -> m (g' x) -> m (Telescope g' f' xs -> Telescope g' f' xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> g x -> m (g' x) forall (x :: k). c x => g x -> m (g' x) g g x gx m (Telescope g' f' xs -> Telescope g' f' xs') -> m (Telescope g' f' xs) -> m (Telescope g' f' xs') forall a b. m (a -> b) -> m a -> m b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> Telescope g f xs -> m (Telescope g' f' xs) forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m (Telescope g' f' xs') go Telescope g f xs t -- | Bifunctor analogue of 'htraverse'' bihtraverse' :: (SListI xs, Applicative m) => (forall x. g x -> m (g' x)) -> (forall x. f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihtraverse' :: forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m (g' x)) -> (forall (x :: k). f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihtraverse' = Proxy Top -> (forall (x :: k). Top x => g x -> m (g' x)) -> (forall (x :: k). Top x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *) (xs :: [k]). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m (g' x)) -> (forall (x :: k). c x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihctraverse' (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) -- | Bifunctor analogue of 'hsequence'' bihsequence' :: forall m g f xs. (SListI xs, Applicative m) => Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs) bihsequence' :: forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). (SListI xs, Applicative m) => Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs) bihsequence' = (forall (x :: k). (:.:) m g x -> m (g x)) -> (forall (x :: k). (:.:) m f x -> m (f x)) -> Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs) forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m (g' x)) -> (forall (x :: k). f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihtraverse' (:.:) m g x -> m (g x) forall (x :: k). (:.:) m g x -> m (g x) forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp (:.:) m f x -> m (f x) forall (x :: k). (:.:) m f x -> m (f x) forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp -- | Bifunctor analogue of 'hctraverse_' bihctraverse_ :: forall proxy c xs m g f. (All c xs, Applicative m) => proxy c -> (forall x. c x => g x -> m ()) -> (forall x. c x => f x -> m ()) -> Telescope g f xs -> m () bihctraverse_ :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m ()) -> (forall (x :: k). c x => f x -> m ()) -> Telescope g f xs -> m () bihctraverse_ proxy c _ forall (x :: k). c x => g x -> m () g forall (x :: k). c x => f x -> m () f = Telescope g f xs -> m () forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m () go where go :: All c xs' => Telescope g f xs' -> m () go :: forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m () go (TZ f x fx) = f x -> m () forall (x :: k). c x => f x -> m () f f x fx go (TS g x gx Telescope g f xs t) = g x -> m () forall (x :: k). c x => g x -> m () g g x gx m () -> m () -> m () forall a b. m a -> m b -> m b forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b *> Telescope g f xs -> m () forall (xs' :: [k]). All c xs' => Telescope g f xs' -> m () go Telescope g f xs t bihtraverse_ :: (SListI xs, Applicative m) => (forall x. g x -> m ()) -> (forall x. f x -> m ()) -> Telescope g f xs -> m () bihtraverse_ :: forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m ()) -> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m () bihtraverse_ = Proxy Top -> (forall (x :: k). Top x => g x -> m ()) -> (forall (x :: k). Top x => f x -> m ()) -> Telescope g f xs -> m () forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m ()) -> (forall (x :: k). c x => f x -> m ()) -> Telescope g f xs -> m () bihctraverse_ (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) {------------------------------------------------------------------------------- Bifunctor analogues of derived functions -------------------------------------------------------------------------------} -- | Bifunctor analogue of 'hmap' bihmap :: SListI xs => (forall x. g x -> g' x) -> (forall x. f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihmap :: forall {k} (xs :: [k]) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). SListI xs => (forall (x :: k). g x -> g' x) -> (forall (x :: k). f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihmap = Proxy Top -> (forall (x :: k). Top x => g x -> g' x) -> (forall (x :: k). Top x => f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs forall {k} (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). All c xs => proxy c -> (forall (x :: k). c x => g x -> g' x) -> (forall (x :: k). c x => f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihcmap (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) -- | Bifunctor analogue of 'hcmap' bihcmap :: All c xs => proxy c -> (forall x. c x => g x -> g' x) -> (forall x. c x => f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihcmap :: forall {k} (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). All c xs => proxy c -> (forall (x :: k). c x => g x -> g' x) -> (forall (x :: k). c x => f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs bihcmap proxy c p forall (x :: k). c x => g x -> g' x g forall (x :: k). c x => f x -> f' x f = NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs forall {k} (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *). NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap (proxy c -> (forall (a :: k). c a => (-.->) g g' a) -> NP (g -.-> g') xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs forall (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). AllN NP c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs hcpure proxy c p ((g a -> g' a) -> (-.->) g g' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn g a -> g' a forall (x :: k). c x => g x -> g' x g)) (proxy c -> (forall (a :: k). c a => (-.->) f f' a) -> NP (f -.-> f') xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs forall (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). AllN NP c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs hcpure proxy c p ((f a -> f' a) -> (-.->) f f' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn f a -> f' a forall (x :: k). c x => f x -> f' x f)) -- | Bifunctor equivalent of 'hzipWith' bihzipWith :: SListI xs => (forall x. h x -> g x -> g' x) -> (forall x. h x -> f x -> f' x) -> NP h xs -> Telescope g f xs -> Telescope g' f' xs bihzipWith :: forall {k} (xs :: [k]) (h :: k -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). SListI xs => (forall (x :: k). h x -> g x -> g' x) -> (forall (x :: k). h x -> f x -> f' x) -> NP h xs -> Telescope g f xs -> Telescope g' f' xs bihzipWith forall (x :: k). h x -> g x -> g' x g forall (x :: k). h x -> f x -> f' x f NP h xs ns = NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs forall {k} (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *). NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap ((forall (a :: k). h a -> (-.->) g g' a) -> NP h xs -> NP (g -.-> g') xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap ((g a -> g' a) -> (-.->) g g' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((g a -> g' a) -> (-.->) g g' a) -> (h a -> g a -> g' a) -> h a -> (-.->) g g' a forall b c a. (b -> c) -> (a -> b) -> a -> c . h a -> g a -> g' a forall (x :: k). h x -> g x -> g' x g) NP h xs ns) ((forall (a :: k). h a -> (-.->) f f' a) -> NP h xs -> NP (f -.-> f') xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap ((f a -> f' a) -> (-.->) f f' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((f a -> f' a) -> (-.->) f f' a) -> (h a -> f a -> f' a) -> h a -> (-.->) f f' a forall b c a. (b -> c) -> (a -> b) -> a -> c . h a -> f a -> f' a forall (x :: k). h x -> f x -> f' x f) NP h xs ns) -- | Bifunctor equivalent of 'hczipWith' bihczipWith :: All c xs => proxy c -> (forall x. c x => h x -> g x -> g' x) -> (forall x. c x => h x -> f x -> f' x) -> NP h xs -> Telescope g f xs -> Telescope g' f' xs bihczipWith :: forall {k} (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (h :: k -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). All c xs => proxy c -> (forall (x :: k). c x => h x -> g x -> g' x) -> (forall (x :: k). c x => h x -> f x -> f' x) -> NP h xs -> Telescope g f xs -> Telescope g' f' xs bihczipWith proxy c p forall (x :: k). c x => h x -> g x -> g' x g forall (x :: k). c x => h x -> f x -> f' x f NP h xs ns = NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs forall {k} (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *). NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap (proxy c -> (forall (a :: k). c a => h a -> (-.->) g g' a) -> NP h xs -> NP (g -.-> g') xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap proxy c p ((g a -> g' a) -> (-.->) g g' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((g a -> g' a) -> (-.->) g g' a) -> (h a -> g a -> g' a) -> h a -> (-.->) g g' a forall b c a. (b -> c) -> (a -> b) -> a -> c . h a -> g a -> g' a forall (x :: k). c x => h x -> g x -> g' x g) NP h xs ns) (proxy c -> (forall (a :: k). c a => h a -> (-.->) f f' a) -> NP h xs -> NP (f -.-> f') xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs hcmap proxy c p ((f a -> f' a) -> (-.->) f f' a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((f a -> f' a) -> (-.->) f f' a) -> (h a -> f a -> f' a) -> h a -> (-.->) f f' a forall b c a. (b -> c) -> (a -> b) -> a -> c . h a -> f a -> f' a forall (x :: k). c x => h x -> f x -> f' x f) NP h xs ns) {------------------------------------------------------------------------------- Simple telescope This is an internal type that is useful primarily useful as a sanity check of our bifunctor generalizations. -------------------------------------------------------------------------------} -- | 'Telescope' with both functors set to the same @f@ newtype SimpleTelescope f xs = SimpleTelescope { forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope :: Telescope f f xs } type instance Prod SimpleTelescope = NP type instance SListIN SimpleTelescope = SListI type instance AllN SimpleTelescope c = All c type instance CollapseTo SimpleTelescope a = [a] instance HAp SimpleTelescope where hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]). Prod SimpleTelescope (f -.-> g) xs -> SimpleTelescope f xs -> SimpleTelescope g xs hap Prod SimpleTelescope (f -.-> g) xs fs = Telescope g g xs -> SimpleTelescope g xs forall {k} (f :: k -> *) (xs :: [k]). Telescope f f xs -> SimpleTelescope f xs SimpleTelescope (Telescope g g xs -> SimpleTelescope g xs) -> (SimpleTelescope f xs -> Telescope g g xs) -> SimpleTelescope f xs -> SimpleTelescope g xs forall b c a. (b -> c) -> (a -> b) -> a -> c . NP (f -.-> g) xs -> NP (f -.-> g) xs -> Telescope f f xs -> Telescope g g xs forall {k} (g :: k -> *) (g' :: k -> *) (xs :: [k]) (f :: k -> *) (f' :: k -> *). NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs bihap Prod SimpleTelescope (f -.-> g) xs NP (f -.-> g) xs fs Prod SimpleTelescope (f -.-> g) xs NP (f -.-> g) xs fs (Telescope f f xs -> Telescope g g xs) -> (SimpleTelescope f xs -> Telescope f f xs) -> SimpleTelescope f xs -> Telescope g g xs forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope f xs -> Telescope f f xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope instance HTraverse_ SimpleTelescope where hctraverse_ :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (AllN SimpleTelescope c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g ()) -> SimpleTelescope f xs -> g () hctraverse_ proxy c p forall (a :: k). c a => f a -> g () f = proxy c -> (forall (a :: k). c a => f a -> g ()) -> (forall (a :: k). c a => f a -> g ()) -> Telescope f f xs -> g () forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m ()) -> (forall (x :: k). c x => f x -> m ()) -> Telescope g f xs -> m () bihctraverse_ proxy c p f x -> g () forall (a :: k). c a => f a -> g () f f x -> g () forall (a :: k). c a => f a -> g () f (Telescope f f xs -> g ()) -> (SimpleTelescope f xs -> Telescope f f xs) -> SimpleTelescope f xs -> g () forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope f xs -> Telescope f f xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope htraverse_ :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *). (SListIN SimpleTelescope xs, Applicative g) => (forall (a :: k). f a -> g ()) -> SimpleTelescope f xs -> g () htraverse_ forall (a :: k). f a -> g () f = (forall (a :: k). f a -> g ()) -> (forall (a :: k). f a -> g ()) -> Telescope f f xs -> g () forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (f :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m ()) -> (forall (x :: k). f x -> m ()) -> Telescope g f xs -> m () bihtraverse_ f x -> g () forall (a :: k). f a -> g () f f x -> g () forall (a :: k). f a -> g () f (Telescope f f xs -> g ()) -> (SimpleTelescope f xs -> Telescope f f xs) -> SimpleTelescope f xs -> g () forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope f xs -> Telescope f f xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope instance HSequence SimpleTelescope where hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *). (SListIN SimpleTelescope xs, Applicative f) => SimpleTelescope (f :.: g) xs -> f (SimpleTelescope g xs) hsequence' = (Telescope g g xs -> SimpleTelescope g xs) -> f (Telescope g g xs) -> f (SimpleTelescope g xs) forall a b. (a -> b) -> f a -> f b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Telescope g g xs -> SimpleTelescope g xs forall {k} (f :: k -> *) (xs :: [k]). Telescope f f xs -> SimpleTelescope f xs SimpleTelescope (f (Telescope g g xs) -> f (SimpleTelescope g xs)) -> (SimpleTelescope (f :.: g) xs -> f (Telescope g g xs)) -> SimpleTelescope (f :.: g) xs -> f (SimpleTelescope g xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs) forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). (SListI xs, Applicative m) => Telescope (m :.: g) (m :.: f) xs -> m (Telescope g f xs) bihsequence' (Telescope (f :.: g) (f :.: g) xs -> f (Telescope g g xs)) -> (SimpleTelescope (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs) -> SimpleTelescope (f :.: g) xs -> f (Telescope g g xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope (f :.: g) xs -> Telescope (f :.: g) (f :.: g) xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN SimpleTelescope c xs, Applicative g) => proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> SimpleTelescope f xs -> g (SimpleTelescope f' xs) hctraverse' proxy c p forall (a :: k). c a => f a -> g (f' a) f = (Telescope f' f' xs -> SimpleTelescope f' xs) -> g (Telescope f' f' xs) -> g (SimpleTelescope f' xs) forall a b. (a -> b) -> g a -> g b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Telescope f' f' xs -> SimpleTelescope f' xs forall {k} (f :: k -> *) (xs :: [k]). Telescope f f xs -> SimpleTelescope f xs SimpleTelescope (g (Telescope f' f' xs) -> g (SimpleTelescope f' xs)) -> (SimpleTelescope f xs -> g (Telescope f' f' xs)) -> SimpleTelescope f xs -> g (SimpleTelescope f' xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . proxy c -> (forall (a :: k). c a => f a -> g (f' a)) -> (forall (a :: k). c a => f a -> g (f' a)) -> Telescope f f xs -> g (Telescope f' f' xs) forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *) (xs :: [k]). (All c xs, Applicative m) => proxy c -> (forall (x :: k). c x => g x -> m (g' x)) -> (forall (x :: k). c x => f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihctraverse' proxy c p f x -> g (f' x) forall (a :: k). c a => f a -> g (f' a) f f x -> g (f' x) forall (a :: k). c a => f a -> g (f' a) f (Telescope f f xs -> g (Telescope f' f' xs)) -> (SimpleTelescope f xs -> Telescope f f xs) -> SimpleTelescope f xs -> g (Telescope f' f' xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope f xs -> Telescope f f xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *). (SListIN SimpleTelescope xs, Applicative g) => (forall (a :: k). f a -> g (f' a)) -> SimpleTelescope f xs -> g (SimpleTelescope f' xs) htraverse' forall (a :: k). f a -> g (f' a) f = (Telescope f' f' xs -> SimpleTelescope f' xs) -> g (Telescope f' f' xs) -> g (SimpleTelescope f' xs) forall a b. (a -> b) -> g a -> g b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Telescope f' f' xs -> SimpleTelescope f' xs forall {k} (f :: k -> *) (xs :: [k]). Telescope f f xs -> SimpleTelescope f xs SimpleTelescope (g (Telescope f' f' xs) -> g (SimpleTelescope f' xs)) -> (SimpleTelescope f xs -> g (Telescope f' f' xs)) -> SimpleTelescope f xs -> g (SimpleTelescope f' xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall (a :: k). f a -> g (f' a)) -> (forall (a :: k). f a -> g (f' a)) -> Telescope f f xs -> g (Telescope f' f' xs) forall {k} (xs :: [k]) (m :: * -> *) (g :: k -> *) (g' :: k -> *) (f :: k -> *) (f' :: k -> *). (SListI xs, Applicative m) => (forall (x :: k). g x -> m (g' x)) -> (forall (x :: k). f x -> m (f' x)) -> Telescope g f xs -> m (Telescope g' f' xs) bihtraverse' f x -> g (f' x) forall (a :: k). f a -> g (f' a) f f x -> g (f' x) forall (a :: k). f a -> g (f' a) f (Telescope f f xs -> g (Telescope f' f' xs)) -> (SimpleTelescope f xs -> Telescope f f xs) -> SimpleTelescope f xs -> g (Telescope f' f' xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . SimpleTelescope f xs -> Telescope f f xs forall {k} (f :: k -> *) (xs :: [k]). SimpleTelescope f xs -> Telescope f f xs getSimpleTelescope instance HCollapse SimpleTelescope where hcollapse :: forall (xs :: [k]) a. SListIN SimpleTelescope xs => SimpleTelescope (K a) xs -> CollapseTo SimpleTelescope a hcollapse (SimpleTelescope Telescope (K a) (K a) xs t) = Telescope (K a) (K a) xs -> [a] forall {k} a (xs :: [k]). Telescope (K a) (K a) xs -> [a] go Telescope (K a) (K a) xs t where go :: Telescope (K a) (K a) xs -> [a] go :: forall {k} a (xs :: [k]). Telescope (K a) (K a) xs -> [a] go (TZ (K a x)) = [a x] go (TS (K a x) Telescope (K a) (K a) xs xs) = a x a -> [a] -> [a] forall a. a -> [a] -> [a] : Telescope (K a) (K a) xs -> [a] forall {k} a (xs :: [k]). Telescope (K a) (K a) xs -> [a] go Telescope (K a) (K a) xs xs {------------------------------------------------------------------------------- Utilities -------------------------------------------------------------------------------} tip :: Telescope g f xs -> NS f xs tip :: forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs tip (TZ f x l) = f x -> NS f (x : xs) forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NS f (x : xs1) Z f x l tip (TS g x _ Telescope g f xs r) = NS f xs -> NS f (x : xs) forall {k} (f :: k -> *) (xs1 :: [k]) (x :: k). NS f xs1 -> NS f (x : xs1) S (Telescope g f xs -> NS f xs forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs tip Telescope g f xs r) fromTip :: NS f xs -> Telescope (K ()) f xs fromTip :: forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Telescope (K ()) f xs fromTip (Z f x l) = f x -> Telescope (K ()) f (x : xs1) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f x l fromTip (S NS f xs1 r) = K () x -> Telescope (K ()) f xs1 -> Telescope (K ()) f (x : xs1) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (() -> K () x forall k a (b :: k). a -> K a b K ()) (NS f xs1 -> Telescope (K ()) f xs1 forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Telescope (K ()) f xs fromTip NS f xs1 r) toAtMost :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a toAtMost :: forall a (xs :: [*]). Telescope (K a) (K (Maybe a)) xs -> AtMost xs a toAtMost = Telescope (K a) (K (Maybe a)) xs -> AtMost xs a forall a (xs :: [*]). Telescope (K a) (K (Maybe a)) xs -> AtMost xs a go where go :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a go :: forall a (xs :: [*]). Telescope (K a) (K (Maybe a)) xs -> AtMost xs a go (TZ (K Maybe a ma)) = AtMost xs a -> (a -> AtMost xs a) -> Maybe a -> AtMost xs a forall b a. b -> (a -> b) -> Maybe a -> b maybe AtMost xs a forall (xs :: [*]) a. AtMost xs a AtMostNil a -> AtMost xs a a -> AtMost (x : xs) a forall a x (xs :: [*]). a -> AtMost (x : xs) a atMostOne Maybe a ma go (TS (K a a) Telescope (K a) (K (Maybe a)) xs t) = a -> AtMost xs a -> AtMost (x : xs) a forall a (xs1 :: [*]) x. a -> AtMost xs1 a -> AtMost (x : xs1) a AtMostCons a a (Telescope (K a) (K (Maybe a)) xs -> AtMost xs a forall a (xs :: [*]). Telescope (K a) (K (Maybe a)) xs -> AtMost xs a go Telescope (K a) (K (Maybe a)) xs t) fromTZ :: Telescope g f '[x] -> f x fromTZ :: forall {k} (g :: k -> *) (f :: k -> *) (x :: k). Telescope g f '[x] -> f x fromTZ (TZ f x fx) = f x f x fx {------------------------------------------------------------------------------- Extension and retraction -------------------------------------------------------------------------------} newtype Extend m g f x y = Extend { forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). Extend m g f x y -> f x -> m (g x, f y) extendWith :: f x -> m (g x, f y) } -- | Extend the telescope -- -- We will not attempt to extend the telescope past its final segment. extend :: forall m h g f xs. Monad m => InPairs (Requiring h (Extend m g f)) xs -- ^ How to extend -> NP (f -.-> Maybe :.: h) xs -- ^ Where to extend /from/ -> Telescope g f xs -> m (Telescope g f xs) extend :: forall {k} (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => InPairs (Requiring h (Extend m g f)) xs -> NP (f -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) extend = InPairs (Requiring h (Extend m g f)) xs -> NP (f -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) forall (xs' :: [k]). InPairs (Requiring h (Extend m g f)) xs' -> NP (f -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go where go :: InPairs (Requiring h (Extend m g f)) xs' -> NP (f -.-> Maybe :.: h) xs' -> Telescope g f xs' -> m (Telescope g f xs') go :: forall (xs' :: [k]). InPairs (Requiring h (Extend m g f)) xs' -> NP (f -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go InPairs (Requiring h (Extend m g f)) xs' PNil NP (f -.-> (Maybe :.: h)) xs' _ (TZ f x fx) = Telescope g f xs' -> m (Telescope g f xs') forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (f x -> Telescope g f '[x] forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f x fx) go (PCons Requiring h (Extend m g f) x y e InPairs (Requiring h (Extend m g f)) (y : zs) es) ((-.->) f (Maybe :.: h) x p :* NP (f -.-> (Maybe :.: h)) xs1 ps) (TZ f x fx) = case (:.:) Maybe h x -> Maybe (h x) forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp ((:.:) Maybe h x -> Maybe (h x)) -> (:.:) Maybe h x -> Maybe (h x) forall a b. (a -> b) -> a -> b $ (-.->) f (Maybe :.: h) x -> f x -> (:.:) Maybe h x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f (Maybe :.: h) x p f x f x fx of Maybe (h x) Nothing -> Telescope g f xs' -> m (Telescope g f xs') forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (f x -> Telescope g f (x : y : zs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f x fx) Just h x hx -> do (g x gx, f y fy) <- Extend m g f x y -> f x -> m (g x, f y) forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). Extend m g f x y -> f x -> m (g x, f y) extendWith (Requiring h (Extend m g f) x y -> h x -> Extend m g f x y forall {k1} {k2} (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). Requiring h f x y -> h x -> f x y provide Requiring h (Extend m g f) x y e h x h x hx) f x f x fx g x -> Telescope g f (y : zs) -> Telescope g f (x : y : zs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f (y : zs) -> Telescope g f xs') -> m (Telescope g f (y : zs)) -> m (Telescope g f xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> InPairs (Requiring h (Extend m g f)) (y : zs) -> NP (f -.-> (Maybe :.: h)) (y : zs) -> Telescope g f (y : zs) -> m (Telescope g f (y : zs)) forall (xs' :: [k]). InPairs (Requiring h (Extend m g f)) xs' -> NP (f -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go InPairs (Requiring h (Extend m g f)) (y : zs) es NP (f -.-> (Maybe :.: h)) xs1 NP (f -.-> (Maybe :.: h)) (y : zs) ps (f y -> Telescope g f (y : zs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f y fy) go (PCons Requiring h (Extend m g f) x y _ InPairs (Requiring h (Extend m g f)) (y : zs) es) ((-.->) f (Maybe :.: h) x _ :* NP (f -.-> (Maybe :.: h)) xs1 ps) (TS g x gx Telescope g f xs fx) = g x -> Telescope g f (y : zs) -> Telescope g f (x : y : zs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f (y : zs) -> Telescope g f xs') -> m (Telescope g f (y : zs)) -> m (Telescope g f xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> InPairs (Requiring h (Extend m g f)) (y : zs) -> NP (f -.-> (Maybe :.: h)) (y : zs) -> Telescope g f (y : zs) -> m (Telescope g f (y : zs)) forall (xs' :: [k]). InPairs (Requiring h (Extend m g f)) xs' -> NP (f -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go InPairs (Requiring h (Extend m g f)) (y : zs) es NP (f -.-> (Maybe :.: h)) xs1 NP (f -.-> (Maybe :.: h)) (y : zs) ps Telescope g f xs Telescope g f (y : zs) fx newtype Retract m g f x y = Retract { forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). Retract m g f x y -> g x -> f y -> m (f x) retractWith :: g x -> f y -> m (f x) } -- | Retract a telescope retract :: forall m h g f xs. Monad m => Tails (Requiring h (Retract m g f)) xs -- ^ How to retract -> NP (g -.-> Maybe :.: h) xs -- ^ Where to retract /to/ -> Telescope g f xs -> m (Telescope g f xs) retract :: forall {k} (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => Tails (Requiring h (Retract m g f)) xs -> NP (g -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) retract = \Tails (Requiring h (Retract m g f)) xs tails NP (g -.-> (Maybe :.: h)) xs np -> NP (g -.-> (Maybe :.: h)) xs -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (g -.-> (Maybe :.: h)) xs np ((SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs)) -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall a b. (a -> b) -> a -> b $ Tails (Requiring h (Retract m g f)) xs -> NP (g -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) forall (xs' :: [k]). SListI xs' => Tails (Requiring h (Retract m g f)) xs' -> NP (g -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go Tails (Requiring h (Retract m g f)) xs tails NP (g -.-> (Maybe :.: h)) xs np where go :: SListI xs' => Tails (Requiring h (Retract m g f)) xs' -> NP (g -.-> Maybe :.: h) xs' -> Telescope g f xs' -> m (Telescope g f xs') go :: forall (xs' :: [k]). SListI xs' => Tails (Requiring h (Retract m g f)) xs' -> NP (g -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go Tails (Requiring h (Retract m g f)) xs' _ NP (g -.-> (Maybe :.: h)) xs' _ (TZ f x fx) = Telescope g f xs' -> m (Telescope g f xs') forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Telescope g f xs' -> m (Telescope g f xs')) -> Telescope g f xs' -> m (Telescope g f xs') forall a b. (a -> b) -> a -> b $ f x -> Telescope g f (x : xs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f x fx go (TCons NP (Requiring h (Retract m g f) x) xs1 r Tails (Requiring h (Retract m g f)) xs1 rs) ((-.->) g (Maybe :.: h) x p :* NP (g -.-> (Maybe :.: h)) xs1 ps) (TS g x gx Telescope g f xs t) = case (:.:) Maybe h x -> Maybe (h x) forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k). (:.:) f g p -> f (g p) unComp ((-.->) g (Maybe :.: h) x -> g x -> (:.:) Maybe h x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) g (Maybe :.: h) x p g x g x gx) of Just h x hx -> (NS (K (f x)) xs -> Telescope g f xs') -> m (NS (K (f x)) xs) -> m (Telescope g f xs') forall a b. (a -> b) -> m a -> m b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (f x -> Telescope g f xs' f x -> Telescope g f (x : xs1) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (f x -> Telescope g f xs') -> (NS (K (f x)) xs -> f x) -> NS (K (f x)) xs -> Telescope g f xs' forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (K (f x)) xs -> f x NS (K (f x)) xs -> CollapseTo NS (f x) forall (xs :: [k]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse) (m (NS (K (f x)) xs) -> m (Telescope g f xs')) -> m (NS (K (f x)) xs) -> m (Telescope g f xs') forall a b. (a -> b) -> a -> b $ NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs) forall (xs :: [k]) (f :: * -> *) (g :: k -> *). (SListIN NS xs, Applicative f) => NS (f :.: g) xs -> f (NS g xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *) (g :: k -> *). (HSequence h, SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs) hsequence' (NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)) -> NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Requiring h (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a) -> Prod NS (Requiring h (Retract m g f) x) xs -> NS f xs -> NS (m :.: K (f x)) xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hzipWith (h x -> g x -> Requiring h (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a forall {k} (m :: * -> *) (h :: k -> *) (x :: k) (g :: k -> *) (f :: k -> *) (z :: k). Functor m => h x -> g x -> Requiring h (Retract m g f) x z -> f z -> (:.:) m (K (f x)) z retractAux h x h x hx g x g x gx) Prod NS (Requiring h (Retract m g f) x) xs NP (Requiring h (Retract m g f) x) xs1 r (Telescope g f xs -> NS f xs forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs tip Telescope g f xs t) Maybe (h x) Nothing -> g x -> Telescope g f xs1 -> Telescope g f (x : xs1) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f xs1 -> Telescope g f xs') -> m (Telescope g f xs1) -> m (Telescope g f xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Tails (Requiring h (Retract m g f)) xs1 -> NP (g -.-> (Maybe :.: h)) xs1 -> Telescope g f xs1 -> m (Telescope g f xs1) forall (xs' :: [k]). SListI xs' => Tails (Requiring h (Retract m g f)) xs' -> NP (g -.-> (Maybe :.: h)) xs' -> Telescope g f xs' -> m (Telescope g f xs') go Tails (Requiring h (Retract m g f)) xs1 rs NP (g -.-> (Maybe :.: h)) xs1 NP (g -.-> (Maybe :.: h)) xs1 ps Telescope g f xs1 Telescope g f xs t -- | Internal auxiliary to 'retract' and 'alignWith' retractAux :: Functor m => h x -- Proof that we need to retract -> g x -- Era we are retracting to -> Requiring h (Retract m g f) x z -> f z -- Current tip (what we are retracting from) -> (m :.: K (f x)) z retractAux :: forall {k} (m :: * -> *) (h :: k -> *) (x :: k) (g :: k -> *) (f :: k -> *) (z :: k). Functor m => h x -> g x -> Requiring h (Retract m g f) x z -> f z -> (:.:) m (K (f x)) z retractAux h x hx g x gx Requiring h (Retract m g f) x z r f z fz = m (K (f x) z) -> (:.:) m (K (f x)) z forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (m (K (f x) z) -> (:.:) m (K (f x)) z) -> m (K (f x) z) -> (:.:) m (K (f x)) z forall a b. (a -> b) -> a -> b $ f x -> K (f x) z forall k a (b :: k). a -> K a b K (f x -> K (f x) z) -> m (f x) -> m (K (f x) z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Retract m g f x z -> g x -> f z -> m (f x) forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). Retract m g f x y -> g x -> f y -> m (f x) retractWith (Requiring h (Retract m g f) x z -> h x -> Retract m g f x z forall {k1} {k2} (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). Requiring h f x y -> h x -> f x y provide Requiring h (Retract m g f) x z r h x hx) g x gx f z fz -- | Align a telescope with another, then apply a function to the tips -- -- Aligning is a combination of extension and retraction, extending or -- retracting the telescope as required to match up with the other telescope. align :: forall m g' g f' f f'' xs. Monad m => InPairs (Requiring g' (Extend m g f)) xs -- ^ How to extend -> Tails (Requiring f' (Retract m g f)) xs -- ^ How to retract -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip -> Telescope g' f' xs -- ^ Telescope we are aligning with -> Telescope g f xs -> m (Telescope g f'' xs) align :: forall {k} (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f' :: k -> *) (f :: k -> *) (f'' :: k -> *) (xs :: [k]). Monad m => InPairs (Requiring g' (Extend m g f)) xs -> Tails (Requiring f' (Retract m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) align = \InPairs (Requiring g' (Extend m g f)) xs es Tails (Requiring f' (Retract m g f)) xs rs NP (f' -.-> (f -.-> f'')) xs atTip -> NP (f' -.-> (f -.-> f'')) xs -> (SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (f' -.-> (f -.-> f'')) xs atTip ((SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> (SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall a b. (a -> b) -> a -> b $ InPairs (Requiring g' (Extend m g f)) xs -> Tails (Requiring f' (Retract m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall (xs' :: [k]). SListI xs' => InPairs (Requiring g' (Extend m g f)) xs' -> Tails (Requiring f' (Retract m g f)) xs' -> NP (f' -.-> (f -.-> f'')) xs' -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') go InPairs (Requiring g' (Extend m g f)) xs es Tails (Requiring f' (Retract m g f)) xs rs NP (f' -.-> (f -.-> f'')) xs atTip where go :: SListI xs' => InPairs (Requiring g' (Extend m g f)) xs' -> Tails (Requiring f' (Retract m g f)) xs' -> NP (f' -.-> f -.-> f'') xs' -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') go :: forall (xs' :: [k]). SListI xs' => InPairs (Requiring g' (Extend m g f)) xs' -> Tails (Requiring f' (Retract m g f)) xs' -> NP (f' -.-> (f -.-> f'')) xs' -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') go InPairs (Requiring g' (Extend m g f)) xs' _ Tails (Requiring f' (Retract m g f)) xs' _ ((-.->) f' (f -.-> f'') x f :* NP (f' -.-> (f -.-> f'')) xs1 _) (TZ f' x f'x) (TZ f x fx) = Telescope g f'' xs' -> m (Telescope g f'' xs') forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Telescope g f'' xs' -> m (Telescope g f'' xs')) -> Telescope g f'' xs' -> m (Telescope g f'' xs') forall a b. (a -> b) -> a -> b $ f'' x -> Telescope g f'' (x : xs1) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ ((-.->) f' (f -.-> f'') x f (-.->) f' (f -.-> f'') x -> f' x -> (-.->) f f'' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a `apFn` f' x f' x f'x (-.->) f f'' x -> f x -> f'' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a `apFn` f x f x fx) go (PCons Requiring g' (Extend m g f) x y _ InPairs (Requiring g' (Extend m g f)) (y : zs) es) (TCons NP (Requiring f' (Retract m g f) x) xs1 _ Tails (Requiring f' (Retract m g f)) xs1 rs) ((-.->) f' (f -.-> f'') x _ :* NP (f' -.-> (f -.-> f'')) xs1 fs) (TS g' x _ Telescope g' f' xs f'x) (TS g x gx Telescope g f xs fx) = g x -> Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f'' (y : zs) -> Telescope g f'' xs') -> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> InPairs (Requiring g' (Extend m g f)) (y : zs) -> Tails (Requiring f' (Retract m g f)) (y : zs) -> NP (f' -.-> (f -.-> f'')) (y : zs) -> Telescope g' f' (y : zs) -> Telescope g f (y : zs) -> m (Telescope g f'' (y : zs)) forall (xs' :: [k]). SListI xs' => InPairs (Requiring g' (Extend m g f)) xs' -> Tails (Requiring f' (Retract m g f)) xs' -> NP (f' -.-> (f -.-> f'')) xs' -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') go InPairs (Requiring g' (Extend m g f)) (y : zs) es Tails (Requiring f' (Retract m g f)) xs1 Tails (Requiring f' (Retract m g f)) (y : zs) rs NP (f' -.-> (f -.-> f'')) xs1 NP (f' -.-> (f -.-> f'')) (y : zs) fs Telescope g' f' xs Telescope g' f' (y : zs) f'x Telescope g f xs Telescope g f (y : zs) fx go InPairs (Requiring g' (Extend m g f)) xs' _ (TCons NP (Requiring f' (Retract m g f) x) xs1 r Tails (Requiring f' (Retract m g f)) xs1 _) ((-.->) f' (f -.-> f'') x f :* NP (f' -.-> (f -.-> f'')) xs1 _) (TZ f' x f'x) (TS g x gx Telescope g f xs fx) = (NS (K (f x)) xs -> Telescope g f'' xs') -> m (NS (K (f x)) xs) -> m (Telescope g f'' xs') forall a b. (a -> b) -> m a -> m b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (f'' x -> Telescope g f'' xs' f'' x -> Telescope g f'' (x : xs1) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (f'' x -> Telescope g f'' xs') -> (NS (K (f x)) xs -> f'' x) -> NS (K (f x)) xs -> Telescope g f'' xs' forall b c a. (b -> c) -> (a -> b) -> a -> c . (\f x fx' -> (-.->) f' (f -.-> f'') x f (-.->) f' (f -.-> f'') x -> f' x -> (-.->) f f'' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a `apFn` f' x f' x f'x (-.->) f f'' x -> f x -> f'' x forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a `apFn` f x fx') (f x -> f'' x) -> (NS (K (f x)) xs -> f x) -> NS (K (f x)) xs -> f'' x forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (K (f x)) xs -> f x NS (K (f x)) xs -> CollapseTo NS (f x) forall (xs :: [k]) a. SListIN NS xs => NS (K a) xs -> CollapseTo NS a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse) (m (NS (K (f x)) xs) -> m (Telescope g f'' xs')) -> m (NS (K (f x)) xs) -> m (Telescope g f'' xs') forall a b. (a -> b) -> a -> b $ NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs) forall (xs :: [k]) (f :: * -> *) (g :: k -> *). (SListIN NS xs, Applicative f) => NS (f :.: g) xs -> f (NS g xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *) (g :: k -> *). (HSequence h, SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs) hsequence' (NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs)) -> NS (m :.: K (f x)) xs -> m (NS (K (f x)) xs) forall a b. (a -> b) -> a -> b $ (forall (a :: k). Requiring f' (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a) -> Prod NS (Requiring f' (Retract m g f) x) xs -> NS f xs -> NS (m :.: K (f x)) xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hzipWith (f' x -> g x -> Requiring f' (Retract m g f) x a -> f a -> (:.:) m (K (f x)) a forall {k} (m :: * -> *) (h :: k -> *) (x :: k) (g :: k -> *) (f :: k -> *) (z :: k). Functor m => h x -> g x -> Requiring h (Retract m g f) x z -> f z -> (:.:) m (K (f x)) z retractAux f' x f' x f'x g x g x gx) Prod NS (Requiring f' (Retract m g f) x) xs NP (Requiring f' (Retract m g f) x) xs1 r (Telescope g f xs -> NS f xs forall {k} (g :: k -> *) (f :: k -> *) (xs :: [k]). Telescope g f xs -> NS f xs tip Telescope g f xs fx) go (PCons Requiring g' (Extend m g f) x y e InPairs (Requiring g' (Extend m g f)) (y : zs) es) (TCons NP (Requiring f' (Retract m g f) x) xs1 _ Tails (Requiring f' (Retract m g f)) xs1 rs) ((-.->) f' (f -.-> f'') x _ :* NP (f' -.-> (f -.-> f'')) xs1 fs) (TS g' x g'x Telescope g' f' xs t'x) (TZ f x fx) = do (g x gx, f y fy) <- Extend m g f x y -> f x -> m (g x, f y) forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (x :: k) (y :: k). Extend m g f x y -> f x -> m (g x, f y) extendWith (Requiring g' (Extend m g f) x y -> g' x -> Extend m g f x y forall {k1} {k2} (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). Requiring h f x y -> h x -> f x y provide Requiring g' (Extend m g f) x y e g' x g' x g'x) f x f x fx g x -> Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs) forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f'' (y : zs) -> Telescope g f'' xs') -> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' xs') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> InPairs (Requiring g' (Extend m g f)) (y : zs) -> Tails (Requiring f' (Retract m g f)) (y : zs) -> NP (f' -.-> (f -.-> f'')) (y : zs) -> Telescope g' f' (y : zs) -> Telescope g f (y : zs) -> m (Telescope g f'' (y : zs)) forall (xs' :: [k]). SListI xs' => InPairs (Requiring g' (Extend m g f)) xs' -> Tails (Requiring f' (Retract m g f)) xs' -> NP (f' -.-> (f -.-> f'')) xs' -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') go InPairs (Requiring g' (Extend m g f)) (y : zs) es Tails (Requiring f' (Retract m g f)) xs1 Tails (Requiring f' (Retract m g f)) (y : zs) rs NP (f' -.-> (f -.-> f'')) xs1 NP (f' -.-> (f -.-> f'')) (y : zs) fs Telescope g' f' xs Telescope g' f' (y : zs) t'x (f y -> Telescope g f (y : zs) forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ f y fy) {------------------------------------------------------------------------------- Derived API -------------------------------------------------------------------------------} -- | Version of 'extend' where the evidence is a simple 'Bool' extendIf :: Monad m => InPairs (Extend m g f) xs -- ^ How to extend -> NP (f -.-> K Bool) xs -- ^ Where to extend /from/ -> Telescope g f xs -> m (Telescope g f xs) extendIf :: forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => InPairs (Extend m g f) xs -> NP (f -.-> K Bool) xs -> Telescope g f xs -> m (Telescope g f xs) extendIf InPairs (Extend m g f) xs es NP (f -.-> K Bool) xs ps = NP (f -.-> K Bool) xs -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (f -.-> K Bool) xs ps ((SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs)) -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall a b. (a -> b) -> a -> b $ InPairs (Requiring (K ()) (Extend m g f)) xs -> NP (f -.-> (Maybe :.: K ())) xs -> Telescope g f xs -> m (Telescope g f xs) forall {k} (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => InPairs (Requiring h (Extend m g f)) xs -> NP (f -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) extend ((forall (x :: k) (y :: k). Extend m g f x y -> Requiring (K ()) (Extend m g f) x y) -> InPairs (Extend m g f) xs -> InPairs (Requiring (K ()) (Extend m g f)) xs forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y -> g x y) -> InPairs f xs -> InPairs g xs InPairs.hmap ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y forall {k} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k) (y :: k1). (h x -> f x y) -> Requiring h f x y Require ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y) -> (Extend m g f x y -> K () x -> Extend m g f x y) -> Extend m g f x y -> Requiring (K ()) (Extend m g f) x y forall b c a. (b -> c) -> (a -> b) -> a -> c . Extend m g f x y -> K () x -> Extend m g f x y forall a b. a -> b -> a const) InPairs (Extend m g f) xs es) ((forall (a :: k). (-.->) f (K Bool) a -> (-.->) f (Maybe :.: K ()) a) -> NP (f -.-> K Bool) xs -> NP (f -.-> (Maybe :.: K ())) xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap (\(-.->) f (K Bool) a f -> (f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a) -> (f a -> (:.:) Maybe (K ()) a) -> (-.->) f (Maybe :.: K ()) a forall a b. (a -> b) -> a -> b $ K Bool a -> (:.:) Maybe (K ()) a forall {k} (x :: k). K Bool x -> (:.:) Maybe (K ()) x fromBool (K Bool a -> (:.:) Maybe (K ()) a) -> (f a -> K Bool a) -> f a -> (:.:) Maybe (K ()) a forall b c a. (b -> c) -> (a -> b) -> a -> c . (-.->) f (K Bool) a -> f a -> K Bool a forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) f (K Bool) a f) NP (f -.-> K Bool) xs ps) -- | Version of 'retract' where the evidence is a simple 'Bool' retractIf :: Monad m => Tails (Retract m g f) xs -- ^ How to retract -> NP (g -.-> K Bool) xs -- ^ Where to retract /to/ -> Telescope g f xs -> m (Telescope g f xs) retractIf :: forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => Tails (Retract m g f) xs -> NP (g -.-> K Bool) xs -> Telescope g f xs -> m (Telescope g f xs) retractIf Tails (Retract m g f) xs rs NP (g -.-> K Bool) xs ps = NP (g -.-> K Bool) xs -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (g -.-> K Bool) xs ps ((SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs)) -> (SListI xs => Telescope g f xs -> m (Telescope g f xs)) -> Telescope g f xs -> m (Telescope g f xs) forall a b. (a -> b) -> a -> b $ Tails (Requiring (K ()) (Retract m g f)) xs -> NP (g -.-> (Maybe :.: K ())) xs -> Telescope g f xs -> m (Telescope g f xs) forall {k} (m :: * -> *) (h :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]). Monad m => Tails (Requiring h (Retract m g f)) xs -> NP (g -.-> (Maybe :.: h)) xs -> Telescope g f xs -> m (Telescope g f xs) retract ((forall (x :: k) (y :: k). Retract m g f x y -> Requiring (K ()) (Retract m g f) x y) -> Tails (Retract m g f) xs -> Tails (Requiring (K ()) (Retract m g f)) xs forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y -> g x y) -> Tails f xs -> Tails g xs Tails.hmap ((K () x -> Retract m g f x y) -> Requiring (K ()) (Retract m g f) x y forall {k} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k) (y :: k1). (h x -> f x y) -> Requiring h f x y Require ((K () x -> Retract m g f x y) -> Requiring (K ()) (Retract m g f) x y) -> (Retract m g f x y -> K () x -> Retract m g f x y) -> Retract m g f x y -> Requiring (K ()) (Retract m g f) x y forall b c a. (b -> c) -> (a -> b) -> a -> c . Retract m g f x y -> K () x -> Retract m g f x y forall a b. a -> b -> a const) Tails (Retract m g f) xs rs) ((forall (a :: k). (-.->) g (K Bool) a -> (-.->) g (Maybe :.: K ()) a) -> NP (g -.-> K Bool) xs -> NP (g -.-> (Maybe :.: K ())) xs forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap (\(-.->) g (K Bool) a f -> (g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a forall {k} (f :: k -> *) (a :: k) (f' :: k -> *). (f a -> f' a) -> (-.->) f f' a fn ((g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a) -> (g a -> (:.:) Maybe (K ()) a) -> (-.->) g (Maybe :.: K ()) a forall a b. (a -> b) -> a -> b $ K Bool a -> (:.:) Maybe (K ()) a forall {k} (x :: k). K Bool x -> (:.:) Maybe (K ()) x fromBool (K Bool a -> (:.:) Maybe (K ()) a) -> (g a -> K Bool a) -> g a -> (:.:) Maybe (K ()) a forall b c a. (b -> c) -> (a -> b) -> a -> c . (-.->) g (K Bool) a -> g a -> K Bool a forall {k} (f :: k -> *) (g :: k -> *) (a :: k). (-.->) f g a -> f a -> g a apFn (-.->) g (K Bool) a f) NP (g -.-> K Bool) xs ps) -- | Version of 'align' that never retracts, only extends -- -- PRE: The telescope we are aligning with cannot be behind us. alignExtend :: (Monad m, HasCallStack) => InPairs (Requiring g' (Extend m g f)) xs -- ^ How to extend -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip -> Telescope g' f' xs -- ^ Telescope we are aligning with -> Telescope g f xs -> m (Telescope g f'' xs) alignExtend :: forall {k} (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]) (f' :: k -> *) (f'' :: k -> *). (Monad m, HasCallStack) => InPairs (Requiring g' (Extend m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) alignExtend InPairs (Requiring g' (Extend m g f)) xs es NP (f' -.-> (f -.-> f'')) xs atTip = NP (f' -.-> (f -.-> f'')) xs -> (SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (f' -.-> (f -.-> f'')) xs atTip ((SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> (SListI xs => Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall a b. (a -> b) -> a -> b $ InPairs (Requiring g' (Extend m g f)) xs -> Tails (Requiring f' (Retract m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall {k} (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f' :: k -> *) (f :: k -> *) (f'' :: k -> *) (xs :: [k]). Monad m => InPairs (Requiring g' (Extend m g f)) xs -> Tails (Requiring f' (Retract m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) align InPairs (Requiring g' (Extend m g f)) xs es ((forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y) -> Tails (Requiring f' (Retract m g f)) xs forall {k} (xs :: [k]) (f :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y) -> Tails f xs Tails.hpure ((forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y) -> Tails (Requiring f' (Retract m g f)) xs) -> (forall (x :: k) (y :: k). Requiring f' (Retract m g f) x y) -> Tails (Requiring f' (Retract m g f)) xs forall a b. (a -> b) -> a -> b $ (f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y forall {k} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k) (y :: k1). (h x -> f x y) -> Requiring h f x y Require ((f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y) -> (f' x -> Retract m g f x y) -> Requiring f' (Retract m g f) x y forall a b. (a -> b) -> a -> b $ \f' x _ -> [Char] -> Retract m g f x y forall a. HasCallStack => [Char] -> a error [Char] precondition) NP (f' -.-> (f -.-> f'')) xs atTip where precondition :: String precondition :: [Char] precondition = [Char] "alignExtend: precondition violated" -- | Version of 'alignExtend' that extends with an NS instead alignExtendNS :: (Monad m, HasCallStack) => InPairs (Extend m g f) xs -- ^ How to extend -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip -> NS f' xs -- ^ NS we are aligning with -> Telescope g f xs -> m (Telescope g f'' xs) alignExtendNS :: forall {k} (m :: * -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]) (f' :: k -> *) (f'' :: k -> *). (Monad m, HasCallStack) => InPairs (Extend m g f) xs -> NP (f' -.-> (f -.-> f'')) xs -> NS f' xs -> Telescope g f xs -> m (Telescope g f'' xs) alignExtendNS InPairs (Extend m g f) xs es NP (f' -.-> (f -.-> f'')) xs atTip NS f' xs ns = NP (f' -.-> (f -.-> f'')) xs -> (SListI xs => Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g f xs -> m (Telescope g f'' xs) forall {k} (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (f' -.-> (f -.-> f'')) xs atTip ((SListI xs => Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g f xs -> m (Telescope g f'' xs)) -> (SListI xs => Telescope g f xs -> m (Telescope g f'' xs)) -> Telescope g f xs -> m (Telescope g f'' xs) forall a b. (a -> b) -> a -> b $ InPairs (Requiring (K ()) (Extend m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope (K ()) f' xs -> Telescope g f xs -> m (Telescope g f'' xs) forall {k} (m :: * -> *) (g' :: k -> *) (g :: k -> *) (f :: k -> *) (xs :: [k]) (f' :: k -> *) (f'' :: k -> *). (Monad m, HasCallStack) => InPairs (Requiring g' (Extend m g f)) xs -> NP (f' -.-> (f -.-> f'')) xs -> Telescope g' f' xs -> Telescope g f xs -> m (Telescope g f'' xs) alignExtend ((forall (x :: k) (y :: k). Extend m g f x y -> Requiring (K ()) (Extend m g f) x y) -> InPairs (Extend m g f) xs -> InPairs (Requiring (K ()) (Extend m g f)) xs forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y -> g x y) -> InPairs f xs -> InPairs g xs InPairs.hmap ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y forall {k} {k1} (h :: k -> *) (f :: k -> k1 -> *) (x :: k) (y :: k1). (h x -> f x y) -> Requiring h f x y Require ((K () x -> Extend m g f x y) -> Requiring (K ()) (Extend m g f) x y) -> (Extend m g f x y -> K () x -> Extend m g f x y) -> Extend m g f x y -> Requiring (K ()) (Extend m g f) x y forall b c a. (b -> c) -> (a -> b) -> a -> c . Extend m g f x y -> K () x -> Extend m g f x y forall a b. a -> b -> a const) InPairs (Extend m g f) xs es) NP (f' -.-> (f -.-> f'')) xs atTip (NS f' xs -> Telescope (K ()) f' xs forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Telescope (K ()) f xs fromTip NS f' xs ns) -- | Internal auxiliary to 'extendIf' and 'retractIf' fromBool :: K Bool x -> (Maybe :.: K ()) x fromBool :: forall {k} (x :: k). K Bool x -> (:.:) Maybe (K ()) x fromBool (K Bool True) = Maybe (K () x) -> (:.:) Maybe (K ()) x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (Maybe (K () x) -> (:.:) Maybe (K ()) x) -> Maybe (K () x) -> (:.:) Maybe (K ()) x forall a b. (a -> b) -> a -> b $ K () x -> Maybe (K () x) forall a. a -> Maybe a Just (K () x -> Maybe (K () x)) -> K () x -> Maybe (K () x) forall a b. (a -> b) -> a -> b $ () -> K () x forall k a (b :: k). a -> K a b K () fromBool (K Bool False) = Maybe (K () x) -> (:.:) Maybe (K ()) x forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp Maybe (K () x) forall a. Maybe a Nothing {------------------------------------------------------------------------------- Additional API -------------------------------------------------------------------------------} newtype ScanNext h g x y = ScanNext { forall {k} (h :: k -> *) (g :: k -> *) (x :: k) (y :: k). ScanNext h g x y -> h x -> g x -> h y getNext :: h x -> g x -> h y } -- | Telescope analogue of 'scanl' on lists -- -- This function is modelled on -- -- > scanl :: (b -> a -> b) -> b -> [a] -> [b] -- -- but there are a few differences: -- -- * Since every seed has a different type, we must be given a function -- for each transition. -- * Unlike 'scanl', we preserve the length of the telescope -- ('scanl' prepends the initial seed) -- * Instead of generating a telescope containing only the seeds, we -- instead pair the seeds with the elements. scanl :: InPairs (ScanNext h g) (x ': xs) -> h x -> Telescope g f (x ': xs) -> Telescope (Product h g) (Product h f) (x ': xs) scanl :: forall {a} (h :: a -> *) (g :: a -> *) (x :: a) (xs :: [a]) (f :: a -> *). InPairs (ScanNext h g) (x : xs) -> h x -> Telescope g f (x : xs) -> Telescope (Product h g) (Product h f) (x : xs) scanl = InPairs (ScanNext h g) (x : xs) -> h x -> Telescope g f (x : xs) -> Telescope (Product h g) (Product h f) (x : xs) forall {a} (h :: a -> *) (g :: a -> *) (x :: a) (xs :: [a]) (f :: a -> *). InPairs (ScanNext h g) (x : xs) -> h x -> Telescope g f (x : xs) -> Telescope (Product h g) (Product h f) (x : xs) go where go :: InPairs (ScanNext h g) (x' ': xs') -> h x' -> Telescope g f (x' ': xs') -> Telescope (Product h g) (Product h f) (x' ': xs') go :: forall {a} (h :: a -> *) (g :: a -> *) (x :: a) (xs :: [a]) (f :: a -> *). InPairs (ScanNext h g) (x : xs) -> h x -> Telescope g f (x : xs) -> Telescope (Product h g) (Product h f) (x : xs) go InPairs (ScanNext h g) (x' : xs') _ h x' hx (TZ f x fx) = Product h f x' -> Telescope (Product h g) (Product h f) (x' : xs') forall {k} (f :: k -> *) (x :: k) (g :: k -> *) (xs :: [k]). f x -> Telescope g f (x : xs) TZ (h x' -> f x' -> Product h f x' forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair h x' hx f x' f x fx) go (PCons ScanNext h g x y f InPairs (ScanNext h g) (y : zs) fs) h x' hx (TS g x gx Telescope g f xs t) = Product h g x' -> Telescope (Product h g) (Product h f) xs' -> Telescope (Product h g) (Product h f) (x' : xs') forall {k} (g :: k -> *) (x :: k) (f :: k -> *) (xs :: [k]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (h x' -> g x' -> Product h g x' forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> g a -> Product f g a Pair h x' hx g x' g x gx) (Telescope (Product h g) (Product h f) xs' -> Telescope (Product h g) (Product h f) (x' : xs')) -> Telescope (Product h g) (Product h f) xs' -> Telescope (Product h g) (Product h f) (x' : xs') forall a b. (a -> b) -> a -> b $ InPairs (ScanNext h g) (y : zs) -> h y -> Telescope g f (y : zs) -> Telescope (Product h g) (Product h f) (y : zs) forall {a} (h :: a -> *) (g :: a -> *) (x :: a) (xs :: [a]) (f :: a -> *). InPairs (ScanNext h g) (x : xs) -> h x -> Telescope g f (x : xs) -> Telescope (Product h g) (Product h f) (x : xs) go InPairs (ScanNext h g) (y : zs) fs (ScanNext h g x y -> h x -> g x -> h y forall {k} (h :: k -> *) (g :: k -> *) (x :: k) (y :: k). ScanNext h g x y -> h x -> g x -> h y getNext ScanNext h g x y f h x' h x hx g x g x gx) Telescope g f xs Telescope g f (y : zs) t {------------------------------------------------------------------------------- Standard type class instances -------------------------------------------------------------------------------} deriving instance ( All (Compose Eq g) xs , All (Compose Eq f) xs ) => Eq (Telescope g f xs) deriving instance ( All (Compose Eq g) xs , All (Compose Ord g) xs , All (Compose Eq f) xs , All (Compose Ord f) xs ) => Ord (Telescope g f xs) deriving instance ( All (Compose Show g) xs , All (Compose Show f) xs ) => Show (Telescope g f xs) instance ( All (Compose NoThunks g) xs , All (Compose NoThunks f) xs ) => NoThunks (Telescope g f xs) where showTypeOf :: Proxy (Telescope g f xs) -> [Char] showTypeOf Proxy (Telescope g f xs) _ = [Char] "Telescope" wNoThunks :: Context -> Telescope g f xs -> IO (Maybe ThunkInfo) wNoThunks Context ctxt = \case TZ f x f -> Context -> f x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks ([Char] "TZ" [Char] -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) f x f TS g x g Telescope g f xs t -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo) allNoThunks [ Context -> g x -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks ([Char] "g" [Char] -> Context -> Context forall a. a -> [a] -> [a] : [Char] "TS" [Char] -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) g x g , Context -> Telescope g f xs -> IO (Maybe ThunkInfo) forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo) noThunks ([Char] "t" [Char] -> Context -> Context forall a. a -> [a] -> [a] : [Char] "TS" [Char] -> Context -> Context forall a. a -> [a] -> [a] : Context ctxt) Telescope g f xs t ]