ouroboros-consensus-0.1.0.0: Consensus layer for the Ouroboros blockchain protocol
Safe HaskellNone
LanguageHaskell2010

Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Description

Intended for qualified import

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

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 ∷ ∀ (f ∷ k0 → Type) (g0 ∷ k0 → Type) (xs ∷ l). Prod (Telescope g) (f -.-> g0) xs → Telescope g f xs → Telescope g g0 xs #

HSequence (Telescope g ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hsequence' ∷ ∀ (xs ∷ l) f (g0 ∷ k0 → Type). (SListIN (Telescope g) xs, Applicative f) ⇒ Telescope g (f :.: g0) xs → f (Telescope g g0 xs) #

hctraverse' ∷ ∀ c (xs ∷ l) g0 proxy f f'. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) #

htraverse' ∷ ∀ (xs ∷ l) g0 f f'. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k0). f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) #

HTraverse_ (Telescope g ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hctraverse_ ∷ ∀ c (xs ∷ l) g0 proxy f. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g0 ()) → Telescope g f xs → g0 () #

htraverse_ ∷ ∀ (xs ∷ l) g0 f. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k0). f a → g0 ()) → Telescope g f xs → g0 () #

(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

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

maxTelescope g f xs → Telescope g f xs → Telescope g f xs Source #

minTelescope 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

showsPrecIntTelescope g f xs → ShowS Source #

showTelescope 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) #

wNoThunks ∷ Context → Telescope g f xs → IO (Maybe ThunkInfo) #

showTypeOfProxy (Telescope g f xs) → String #

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 ∷ ∀ 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

fromTZTelescope g f '[x] → f x Source #

fromTipNS f xs → Telescope (K ()) f xs Source #

tipTelescope g f xs → NS f xs Source #

toAtMostTelescope (K a) (K (Maybe a)) xs → AtMost xs a Source #

Bifunctor analogues of SOP functions

bihapNP (g -.-> g') xs → NP (f -.-> f') xs → Telescope g f xs → Telescope g' f' xs Source #

Bifunctor analogue of hap

bihczipWithAll c xs ⇒ proxy c → (∀ x. c x ⇒ h x → g x → g' x) → (∀ 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

bihmapSListI xs ⇒ (∀ x. g x → g' x) → (∀ x. f x → f' x) → Telescope g f xs → Telescope g' f' xs Source #

Bifunctor analogue of hmap

bihzipWithSListI xs ⇒ (∀ x. h x → g x → g' x) → (∀ 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

newtype Retract m g f x y Source #

Constructors

Retract 

Fields

align Source #

Arguments

∷ ∀ 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

∷ ∀ 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

∷ ∀ 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

newtype SimpleTelescope f xs Source #

Telescope with both functors set to the same f

Constructors

SimpleTelescope 

Fields

Instances

Instances details
HAp (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hap ∷ ∀ (f ∷ k0 → Type) (g ∷ k0 → Type) (xs ∷ l). Prod SimpleTelescope (f -.-> g) xs → SimpleTelescope f xs → SimpleTelescope g xs #

HCollapse (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hcollapse ∷ ∀ (xs ∷ l) a. SListIN SimpleTelescope xs ⇒ SimpleTelescope (K a) xs → CollapseTo SimpleTelescope a #

HSequence (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN SimpleTelescope xs, Applicative f) ⇒ SimpleTelescope (f :.: g) xs → f (SimpleTelescope g xs) #

hctraverse' ∷ ∀ c (xs ∷ l) g proxy f f'. (AllN SimpleTelescope c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) #

htraverse' ∷ ∀ (xs ∷ l) g f f'. (SListIN SimpleTelescope xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) #

HTraverse_ (SimpleTelescope ∷ (k → Type) → [k] → Type) Source # 
Instance details

Defined in Ouroboros.Consensus.HardFork.Combinator.Util.Telescope

Methods

hctraverse_ ∷ ∀ c (xs ∷ l) g proxy f. (AllN SimpleTelescope c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k0). c a ⇒ f a → g ()) → SimpleTelescope f xs → g () #

htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN SimpleTelescope xs, Applicative g) ⇒ (∀ (a ∷ k0). f a → g ()) → SimpleTelescope f xs → g () #

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

scanlInPairs (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.