Safe Haskell	None
Language	Haskell2010

Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Contents

Telescope
- Utilities
- Bifunctor analogues of SOP functions
Extension, retraction, alignment
- Simplified API
Additional API

Description

Intended for qualified import

import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Telescope as Telescope

Synopsis

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)
sequence :: forall m g f xs. Functor m => Telescope g (m :.: f) xs -> m ( Telescope g f xs)
fromTZ :: Telescope g f '[x] -> f x
fromTip :: NS f xs -> Telescope ( K ()) f xs
tip :: Telescope g f xs -> NS f xs
toAtMost :: Telescope ( K a) ( K ( Maybe a)) xs -> AtMost xs a
bihap :: NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs
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
bihmap :: SListI xs => ( forall x. g x -> g' x) -> ( forall x. f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs
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
newtype Extend m g f x y = Extend {
- extendWith :: f x -> m (g x, f y)
}
newtype Retract m g f x y = Retract {
- retractWith :: g x -> f y -> m (f x)
}
align :: forall m g' g f' f f'' xs. 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)
extend :: forall m h g f xs. Monad m => InPairs ( Requiring h ( Extend m g f)) xs -> NP (f -.-> ( Maybe :.: h)) xs -> Telescope g f xs -> m ( Telescope g f xs)
retract :: forall m h g f xs. Monad m => Tails ( Requiring h ( Retract m g f)) xs -> NP (g -.-> ( Maybe :.: h)) xs -> Telescope g f xs -> m ( Telescope g f xs)
alignExtend :: ( 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)
alignExtendNS :: ( 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)
extendIf :: Monad m => InPairs ( Extend m g f) xs -> NP (f -.-> K Bool ) xs -> Telescope g f xs -> m ( Telescope g f xs)
retractIf :: Monad m => Tails ( Retract m g f) xs -> NP (g -.-> K Bool ) xs -> Telescope g f xs -> m ( Telescope g f xs)
newtype ScanNext h g x y = ScanNext {
- getNext :: h x -> g x -> h y
}
newtype SimpleTelescope f xs = SimpleTelescope {
- getSimpleTelescope :: Telescope f f xs
}
scanl :: InPairs ( ScanNext h g) (x ': xs) -> h x -> Telescope g f (x ': xs) -> Telescope ( Product h g) ( Product h f) (x ': xs)

Telescope

data Telescope (g :: k -> Type ) (f :: k -> Type ) (xs :: [k]) where Source #

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.

Constructors

TZ :: !(f x) -> Telescope g f (x ': xs)
TS :: !(g x) -> !( Telescope g f xs) -> Telescope g f (x ': xs)

Instances

Instances details

HAp ( Telescope g :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hap :: forall (f :: k0 -> Type ) (g0 :: k0 -> Type ) (xs :: l). Prod ( Telescope g) (f -.-> g0) xs -> Telescope g f xs -> Telescope g g0 xs Source #
HTraverse_ ( Telescope g :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hctraverse_ :: forall c (xs :: l) g0 proxy f. ( AllN ( Telescope g) c xs, Applicative g0) => proxy c -> ( forall (a :: k0). c a => f a -> g0 ()) -> Telescope g f xs -> g0 () Source # htraverse_ :: forall (xs :: l) g0 f. ( SListIN ( Telescope g) xs, Applicative g0) => ( forall (a :: k0). f a -> g0 ()) -> Telescope g f xs -> g0 () Source #
HSequence ( Telescope g :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hsequence' :: forall (xs :: l) f (g0 :: k0 -> Type ). ( SListIN ( Telescope g) xs, Applicative f) => Telescope g (f :.: g0) xs -> f ( Telescope g g0 xs) Source # hctraverse' :: forall c (xs :: l) g0 proxy f f'. ( AllN ( Telescope g) c xs, Applicative g0) => proxy c -> ( forall (a :: k0). c a => f a -> g0 (f' a)) -> Telescope g f xs -> g0 ( Telescope g f' xs) Source # htraverse' :: forall (xs :: l) g0 f f'. ( SListIN ( Telescope g) xs, Applicative g0) => ( forall (a :: k0). f a -> g0 (f' a)) -> Telescope g f xs -> g0 ( Telescope g f' xs) Source #
( All ( Compose Eq g) xs, All ( Compose Eq f) xs) => Eq ( Telescope g f xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods (==) :: Telescope g f xs -> Telescope g f xs -> Bool Source # (/=) :: Telescope g f xs -> Telescope g f xs -> Bool Source #
( 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) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods compare :: Telescope g f xs -> Telescope g f xs -> Ordering Source # (<) :: Telescope g f xs -> Telescope g f xs -> Bool Source # (<=) :: Telescope g f xs -> Telescope g f xs -> Bool Source # (>) :: Telescope g f xs -> Telescope g f xs -> Bool Source # (>=) :: Telescope g f xs -> Telescope g f xs -> Bool Source # max :: Telescope g f xs -> Telescope g f xs -> Telescope g f xs Source # min :: Telescope g f xs -> Telescope g f xs -> Telescope g f xs Source #
( All ( Compose Show g) xs, All ( Compose Show f) xs) => Show ( Telescope g f xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods showsPrec :: Int -> Telescope g f xs -> ShowS Source # show :: Telescope g f xs -> String Source # showList :: [ Telescope g f xs] -> ShowS Source #
( All ( Compose NoThunks g) xs, All ( Compose NoThunks f) xs) => NoThunks ( Telescope g f xs) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods noThunks :: Context -> Telescope g f xs -> IO ( Maybe ThunkInfo ) Source # wNoThunks :: Context -> Telescope g f xs -> IO ( Maybe ThunkInfo ) Source # showTypeOf :: Proxy ( Telescope g f xs) -> String Source #
type Prod ( Telescope g :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type Prod ( Telescope g :: (k -> Type ) -> [k] -> Type ) = NP :: (k -> Type ) -> [k] -> Type
type SListIN ( Telescope g :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type SListIN ( Telescope g :: (k -> Type ) -> [k] -> Type ) = SListI :: [k] -> Constraint
type AllN ( Telescope g :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type AllN ( Telescope g :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) = All c

sequence :: forall m g f xs. Functor m => Telescope g (m :.: f) xs -> m ( Telescope g f xs) Source #

Specialization of hsequence' with weaker constraints ( Functor rather than Applicative )

Utilities

fromTZ :: Telescope g f '[x] -> f x Source #

fromTip :: NS f xs -> Telescope ( K ()) f xs Source #

tip :: Telescope g f xs -> NS f xs Source #

toAtMost :: Telescope ( K a) ( K ( Maybe a)) xs -> AtMost xs a Source #

Bifunctor analogues of SOP functions

bihap :: NP (g -.-> g') xs -> NP (f -.-> f') xs -> Telescope g f xs -> Telescope g' f' xs Source #

Bifunctor analogue of hap

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

Bifunctor equivalent of hczipWith

bihmap :: SListI xs => ( forall x. g x -> g' x) -> ( forall x. f x -> f' x) -> Telescope g f xs -> Telescope g' f' xs Source #

Bifunctor analogue of hmap

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

Bifunctor equivalent of hzipWith

Extension, retraction, alignment

newtype Extend m g f x y Source #

Constructors

Extend
Fields extendWith :: f x -> m (g x, f y)

newtype Retract m g f x y Source #

Constructors

Retract
Fields retractWith :: g x -> f y -> m (f x)

align Source #

Arguments

:: 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 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.

extend Source #

Arguments

:: 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 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.

retract Source #

Arguments

:: 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 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 .

Simplified API

alignExtend Source #

Arguments

:: ( 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)

Version of align that never retracts, only extends

PRE: The telescope we are aligning with cannot be behind us.

alignExtendNS Source #

Arguments

:: ( 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)

Version of alignExtend that extends with an NS instead

extendIf Source #

Arguments

:: 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)

Version of extend where the evidence is a simple Bool

retractIf Source #

Arguments

:: 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)

Version of retract where the evidence is a simple Bool

Additional API

newtype ScanNext h g x y Source #

Constructors

ScanNext
Fields getNext :: h x -> g x -> h y

newtype SimpleTelescope f xs Source #

Telescope with both functors set to the same f

Constructors

SimpleTelescope
Fields getSimpleTelescope :: Telescope f f xs

Instances

Instances details

HAp ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hap :: forall (f :: k0 -> Type ) (g :: k0 -> Type ) (xs :: l). Prod SimpleTelescope (f -.-> g) xs -> SimpleTelescope f xs -> SimpleTelescope g xs Source #
HCollapse ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hcollapse :: forall (xs :: l) a. SListIN SimpleTelescope xs => SimpleTelescope ( K a) xs -> CollapseTo SimpleTelescope a Source #
HTraverse_ ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hctraverse_ :: forall c (xs :: l) g proxy f. ( AllN SimpleTelescope c xs, Applicative g) => proxy c -> ( forall (a :: k0). c a => f a -> g ()) -> SimpleTelescope f xs -> g () Source # htraverse_ :: forall (xs :: l) g f. ( SListIN SimpleTelescope xs, Applicative g) => ( forall (a :: k0). f a -> g ()) -> SimpleTelescope f xs -> g () Source #
HSequence ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope Methods hsequence' :: forall (xs :: l) f (g :: k0 -> Type ). ( SListIN SimpleTelescope xs, Applicative f) => SimpleTelescope (f :.: g) xs -> f ( SimpleTelescope g xs) Source # hctraverse' :: forall c (xs :: l) g proxy f f'. ( AllN SimpleTelescope c xs, Applicative g) => proxy c -> ( forall (a :: k0). c a => f a -> g (f' a)) -> SimpleTelescope f xs -> g ( SimpleTelescope f' xs) Source # htraverse' :: forall (xs :: l) g f f'. ( SListIN SimpleTelescope xs, Applicative g) => ( forall (a :: k0). f a -> g (f' a)) -> SimpleTelescope f xs -> g ( SimpleTelescope f' xs) Source #
type Prod ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type Prod ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) = NP :: (k -> Type ) -> [k] -> Type
type SListIN ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type SListIN ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) = SListI :: [k] -> Constraint
type CollapseTo ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) a Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type CollapseTo ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) a = [a]
type AllN ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) Source #
Instance details Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope type AllN ( SimpleTelescope :: (k -> Type ) -> [k] -> Type ) (c :: k -> Constraint ) = All c

scanl :: InPairs ( ScanNext h g) (x ': xs) -> h x -> Telescope g f (x ': xs) -> Telescope ( Product h g) ( Product h f) (x ': xs) Source #

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.