{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Intended for qualified import -- -- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope module Ouroboros.Consensus.HardFork.Combinator.Util.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 Prelude hiding (scanl, sequence, zipWith) import Data.Functor.Product import Data.Kind import Data.SOP.Strict import GHC.Stack import NoThunks.Class (NoThunks (..), allNoThunks) import Ouroboros.Consensus.Util.Counting import Ouroboros.Consensus.Util.SOP import Ouroboros.Consensus.HardFork.Combinator.Util.InPairs (InPairs (..), Requiring (..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs import Ouroboros.Consensus.HardFork.Combinator.Util.Tails (Tails (..)) import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Tails as Tails {------------------------------------------------------------------------------- Telescope -------------------------------------------------------------------------------} -- | Telescope -- -- A telescope is an extension of an 'NS', where every time we "go right" in the -- sum we have an additional value. -- -- Blockchain intuition: think of @g@ as representing some kind of past state, -- and @f@ some kind of current state. Then depending on how many hard fork -- transitions we have had, we might either have, say -- -- > TZ currentByronState -- > TS pastByronState $ TZ currentShelleyState -- > TS pastByronState $ TS pastShelleyState $ TZ currentGoguenState -- -- 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. data Telescope (g :: k -> Type) (f :: k -> Type) (xs :: [k]) 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 :: 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 :: Telescope g f xs -> NP (f -.-> f') xs -> Telescope g f' xs go (TZ f x fx) ((-.->) f f' x f :* NP (f -.-> f') xs _) = f' x -> Telescope g f' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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') xs fs) = g x -> Telescope g f' xs -> Telescope g f' (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). 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') xs fs) instance HTraverse_ (Telescope g) where hctraverse_ :: 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 (f :: * -> *) a. Applicative f => a -> f a pure ()) htraverse_ :: (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 (f :: * -> *) a. Applicative f => a -> f a pure ()) instance HSequence (Telescope g) where hsequence' :: 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 (f :: * -> *) a. Applicative f => a -> f a pure) forall (x :: k). (:.:) f g x -> (:.:) f g x forall a. a -> a id hctraverse' :: 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 forall (x :: k). c x => g x -> g (g x) forall (f :: * -> *) a. Applicative f => a -> f a pure htraverse' :: (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' forall (x :: k). g x -> g (g x) 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 :: 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 :: Telescope g (m :.: f) xs' -> m (Telescope g f xs') go (TZ (Comp m (f x) fx)) = f x -> Telescope g f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (f x -> Telescope g f (x : xs)) -> m (f x) -> m (Telescope g f (x : 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 a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f xs -> Telescope g f (x : xs)) -> m (Telescope g f xs) -> m (Telescope g f (x : 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 {------------------------------------------------------------------------------- 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 :: 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 :: 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') xs _) = f' x -> Telescope g' f' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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') xs gs) ((-.->) f f' x _ :* NP (f -.-> f') xs fs) = g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). 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') xs gs NP (f -.-> f') xs NP (f -.-> f') xs 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' :: 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 :: Telescope g f xs' -> m (Telescope g' f' xs') go (TZ f x fx) = f' x -> Telescope g' f' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (f' x -> Telescope g' f' (x : xs)) -> m (f' x) -> m (Telescope g' f' (x : 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' (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS (g' x -> Telescope g' f' xs -> Telescope g' f' (x : xs)) -> m (g' x) -> m (Telescope g' f' xs -> Telescope g' f' (x : 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' (x : xs)) -> m (Telescope g' f' xs) -> m (Telescope g' f' (x : xs)) 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 (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' (Proxy Top forall k (t :: k). 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' :: 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' 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 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_ :: 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 :: 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 (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 (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_ (Proxy Top forall k (t :: k). 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 (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 (Proxy Top forall k (t :: k). 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 :: 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 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 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 (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 :: 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 { 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 :: 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_ :: 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 forall (a :: k). c a => f a -> g () f 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 (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_ forall (a :: k). f a -> g () f 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' :: 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 (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' :: 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 (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 forall (a :: k). c a => f a -> g (f' a) f 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 (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 (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' forall (a :: k). f a -> g (f' a) f 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 :: 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 :: 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 :: Telescope g f xs -> NS f xs tip (TZ f x l) = f x -> NS f (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs) Z f x l tip (TS g x _ Telescope g f xs r) = NS f xs -> NS f (x : xs) forall a (f :: a -> *) (xs :: [a]) (x :: a). NS f xs -> NS f (x : xs) 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 :: NS f xs -> Telescope (K ()) f xs fromTip (Z f x l) = f x -> Telescope (K ()) f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ f x l fromTip (S NS f xs r) = K () x -> Telescope (K ()) f xs -> Telescope (K ()) f (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). 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 xs -> Telescope (K ()) f xs forall k (f :: k -> *) (xs :: [k]). NS f xs -> Telescope (K ()) f xs fromTip NS f xs r) toAtMost :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a toAtMost :: 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 :: Telescope (K a) (K (Maybe a)) xs -> AtMost xs a go (TZ (K Maybe a ma)) = AtMost (x : xs) a -> (a -> AtMost (x : xs) a) -> Maybe a -> AtMost (x : xs) a forall b a. b -> (a -> b) -> Maybe a -> b maybe AtMost (x : xs) a forall (xs :: [*]) a. AtMost xs a AtMostNil 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 (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) 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 :: 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 { 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. -- -- Blockchain intuition: suppose we have a telescope containing the ledger -- state. The "how to extend" argument would take, say, the final Byron -- state to the initial Shelley state; and "where to extend from" argument -- would indicate when we want to extend: when the current slot number has -- gone past the end of the Byron era. 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 :: 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 :: 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 '[x] -> m (Telescope g f '[x]) forall (m :: * -> *) a. Monad m => a -> m a return (f x -> Telescope g f '[x] forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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)) xs 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 (x : y : zs) -> m (Telescope g f (x : y : zs)) forall (m :: * -> *) a. Monad m => a -> m a return (f x -> Telescope g f (x : y : zs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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 (m :: * -> *) k (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 (h :: k1 -> *) k2 (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 a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f (y : zs) -> Telescope g f (x : y : zs)) -> m (Telescope g f (y : zs)) -> m (Telescope g f (x : y : zs)) 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)) xs NP (f -.-> (Maybe :.: h)) (y : zs) ps (f y -> Telescope g f (y : zs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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)) xs ps) (TS g x gx Telescope g f xs fx) = g x -> Telescope g f (y : zs) -> Telescope g f (x : y : zs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f (y : zs) -> Telescope g f (x : y : zs)) -> m (Telescope g f (y : zs)) -> m (Telescope g f (x : y : zs)) 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)) xs 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 { Retract m g f x y -> g x -> f y -> m (f x) retractWith :: g x -> f y -> m (f x) } -- | Retract a telescope -- -- Blockchain intuition: suppose we have a telescope containing the consensus -- state. When we rewind the consensus state, we might cross a hard fork -- transition point. So we first /retract/ the telescope /to/ the era containing -- the slot number that we want to rewind to, and only then call -- 'rewindChainDepState' on that era. Of course, retraction may fail (we -- might not /have/ past consensus state to rewind to anymore); this failure -- would require a choice for a particular monad @m@. 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 :: 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 :: 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 (x : xs) -> m (Telescope g f (x : xs)) forall (m :: * -> *) a. Monad m => a -> m a return (Telescope g f (x : xs) -> m (Telescope g f (x : xs))) -> Telescope g f (x : xs) -> m (Telescope g f (x : xs)) forall a b. (a -> b) -> a -> b $ f x -> Telescope g f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ f x fx go (TCons NP (Requiring h (Retract m g f) x) xs r Tails (Requiring h (Retract m g f)) xs rs) ((-.->) g (Maybe :.: h) x p :* NP (g -.-> (Maybe :.: h)) xs 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 (x : xs)) -> m (NS (K (f x)) xs) -> m (Telescope g f (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (f x -> Telescope g f (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (f x -> Telescope g f (x : xs)) -> (NS (K (f x)) xs -> f x) -> NS (K (f x)) xs -> Telescope g f (x : xs) forall b c a. (b -> c) -> (a -> b) -> a -> c . NS (K (f x)) xs -> f x 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 (x : xs))) -> m (NS (K (f x)) xs) -> m (Telescope g f (x : xs)) forall a b. (a -> b) -> a -> b $ NS (m :.: K (f x)) xs -> m (NS (K (f x)) 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 hx g x g x gx) Prod NS (Requiring h (Retract m g f) x) xs NP (Requiring h (Retract m g f) x) xs 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 xs -> Telescope g f (x : xs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f xs -> Telescope g f (x : xs)) -> m (Telescope g f xs) -> m (Telescope g f (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 rs NP (g -.-> (Maybe :.: h)) xs NP (g -.-> (Maybe :.: h)) xs ps Telescope g f xs 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 :: 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 (m :: * -> *) k (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 (h :: k1 -> *) k2 (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. -- -- Blockchain intuition: suppose we have one telescope containing the -- already-ticked ledger state, and another telescope containing the consensus -- state. Since the ledger state has already been ticked, it might have been -- advanced to the next era. If this happens, we should then align the -- consensus state with the ledger state, moving /it/ also to the next era, -- before we can do the consensus header validation check. Note that in this -- particular example, the ledger state will always be ahead of the consensus -- state, never behind; 'alignExtend' can be used in this case. 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 :: 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 :: 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'')) xs _) (TZ f' x f'x) (TZ f x fx) = Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs)) forall (m :: * -> *) a. Monad m => a -> m a return (Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs))) -> Telescope g f'' (x : xs) -> m (Telescope g f'' (x : xs)) forall a b. (a -> b) -> a -> b $ f'' x -> Telescope g f'' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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) xs _ Tails (Requiring f' (Retract m g f)) xs rs) ((-.->) f' (f -.-> f'') x _ :* NP (f' -.-> (f -.-> f'')) xs 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 a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs)) -> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' (x : y : zs)) 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)) xs Tails (Requiring f' (Retract m g f)) (y : zs) rs NP (f' -.-> (f -.-> f'')) xs 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) xs r Tails (Requiring f' (Retract m g f)) xs _) ((-.->) f' (f -.-> f'') x f :* NP (f' -.-> (f -.-> f'')) xs _) (TZ f' x f'x) (TS g x gx Telescope g f xs fx) = (NS (K (f x)) xs -> Telescope g f'' (x : xs)) -> m (NS (K (f x)) xs) -> m (Telescope g f'' (x : xs)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (f'' x -> Telescope g f'' (x : xs) forall a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). f x -> Telescope g f (x : xs) TZ (f'' x -> Telescope g f'' (x : xs)) -> (NS (K (f x)) xs -> f'' x) -> NS (K (f x)) xs -> Telescope g f'' (x : 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 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'' (x : xs))) -> m (NS (K (f x)) xs) -> m (Telescope g f'' (x : xs)) forall a b. (a -> b) -> a -> b $ NS (m :.: K (f x)) xs -> m (NS (K (f x)) 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 g x g x gx) Prod NS (Requiring f' (Retract m g f) x) xs NP (Requiring f' (Retract m g f) x) xs 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) xs _ Tails (Requiring f' (Retract m g f)) xs rs) ((-.->) f' (f -.-> f'') x _ :* NP (f' -.-> (f -.-> f'')) xs 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 (m :: * -> *) k (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 (h :: k1 -> *) k2 (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 a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). g x -> Telescope g f xs -> Telescope g f (x : xs) TS g x gx (Telescope g f'' (y : zs) -> Telescope g f'' (x : y : zs)) -> m (Telescope g f'' (y : zs)) -> m (Telescope g f'' (x : y : zs)) 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)) xs Tails (Requiring f' (Retract m g f)) (y : zs) rs NP (f' -.-> (f -.-> f'')) xs 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 a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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 :: 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 k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). (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 :: 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 k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). (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 :: 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 k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). (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 :: 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 k1 k2 (h :: k1 -> *) (f :: k1 -> k2 -> *) (x :: k1) (y :: k2). (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 :: 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) -> (:.:) Maybe (K ()) x) -> Maybe (K () x) -> (:.:) Maybe (K ()) x forall a b. (a -> b) -> a -> b $ Maybe (K () x) forall a. Maybe a Nothing {------------------------------------------------------------------------------- Additional API -------------------------------------------------------------------------------} newtype ScanNext h g x y = ScanNext { 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 :: 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 :: 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 a (f :: a -> *) (x :: a) (g :: a -> *) (xs :: [a]). 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) (y : zs) -> Telescope (Product h g) (Product h f) (x' : y : zs) forall a (g :: a -> *) (x :: a) (f :: a -> *) (xs :: [a]). 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) (y : zs) -> Telescope (Product h g) (Product h f) (x' : y : zs)) -> Telescope (Product h g) (Product h f) (y : zs) -> Telescope (Product h g) (Product h f) (x' : y : zs) 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 ]