Safe Haskell	None
Language	Haskell2010

Data.SOP.Telescope

Contents

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

Description

See Telescope

Intended for qualified import

import           Data.SOP.Telescope (Telescope(..))
import qualified Data.SOP.Telescope as Telescope

Synopsis

data Telescope (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]) where
- TZ ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (g ∷ k → Type) (xs1 ∷ [k]). !(f x) → Telescope g f (x ': xs1)
- TS ∷ ∀ {k} (g ∷ k → Type) (x ∷ k) (f ∷ k → Type) (xs1 ∷ [k]). !(g x) → !(Telescope g f xs1) → Telescope g f (x ': xs1)
sequence ∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Functor m ⇒ Telescope g (m :.: f) xs → m (Telescope g f xs)
fromTZ ∷ ∀ {k} (g ∷ k → Type) f (x ∷ k). Telescope g f '[x] → f x
fromTip ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NS f xs → Telescope (K () ∷ k → Type) f xs
tip ∷ ∀ {k} (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Telescope g f xs → NS f xs
toAtMost ∷ ∀ a (xs ∷ [Type]). Telescope (K a ∷ Type → Type) (K (Maybe a) ∷ Type → Type) xs → AtMost xs a
bihap ∷ ∀ {k} (g ∷ k → Type) (g' ∷ k → Type) (xs ∷ [k]) (f ∷ k → Type) (f' ∷ k → Type). NP (g -.-> g') xs → NP (f -.-> f') xs → Telescope g f xs → Telescope g' f' xs
bihczipWith ∷ ∀ {k} c (xs ∷ [k]) proxy h g g' f f'. All c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ h x → g x → g' x) → (∀ (x ∷ k). c x ⇒ h x → f x → f' x) → NP h xs → Telescope g f xs → Telescope g' f' xs
bihmap ∷ ∀ {k} (xs ∷ [k]) g g' f f'. SListI xs ⇒ (∀ (x ∷ k). g x → g' x) → (∀ (x ∷ k). f x → f' x) → Telescope g f xs → Telescope g' f' xs
bihzipWith ∷ ∀ {k} (xs ∷ [k]) h g g' f f'. SListI xs ⇒ (∀ (x ∷ k). h x → g x → g' x) → (∀ (x ∷ k). h x → f x → f' x) → NP h xs → Telescope g f xs → Telescope g' f' xs
newtype Extend (m ∷ Type → Type) (g ∷ k → Type) (f ∷ k → Type) (x ∷ k) (y ∷ k) = Extend {
- extendWith ∷ f x → m (g x, f y)
}
newtype Retract (m ∷ Type → Type) (g ∷ k → Type) (f ∷ k → Type) (x ∷ k) (y ∷ k) = Retract {
- retractWith ∷ g x → f y → m (f x)
}
align ∷ ∀ {k} m (g' ∷ k → Type) (g ∷ k → Type) (f' ∷ k → Type) (f ∷ k → Type) (f'' ∷ k → Type) (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)
extend ∷ ∀ {k} m (h ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (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)
retract ∷ ∀ {k} m (h ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (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)
alignExtend ∷ ∀ {k} m (g' ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]) (f' ∷ k → Type) (f'' ∷ k → Type). (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 ∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]) (f' ∷ k → Type) (f'' ∷ k → Type). (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 ∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Monad m ⇒ InPairs (Extend m g f) xs → NP (f -.-> (K Bool ∷ k → Type)) xs → Telescope g f xs → m (Telescope g f xs)
retractIf ∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Monad m ⇒ Tails (Retract m g f) xs → NP (g -.-> (K Bool ∷ k → Type)) xs → Telescope g f xs → m (Telescope g f xs)
newtype ScanNext (h ∷ k → Type) (g ∷ k → Type) (x ∷ k) (y ∷ k) = ScanNext {
- getNext ∷ h x → g x → h y
}
newtype SimpleTelescope (f ∷ k → Type) (xs ∷ [k]) = SimpleTelescope {
- getSimpleTelescope ∷ Telescope f f xs
}
scanl ∷ ∀ {a} h (g ∷ a → Type) (x ∷ a) (xs ∷ [a]) (f ∷ a → Type). 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.

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 ∷ ∀ {k} (f ∷ k → Type) (x ∷ k) (g ∷ k → Type) (xs1 ∷ [k]). !(f x) → Telescope g f (x ': xs1)
TS ∷ ∀ {k} (g ∷ k → Type) (x ∷ k) (f ∷ k → Type) (xs1 ∷ [k]). !(g x) → !(Telescope g f xs1) → Telescope g f (x ': xs1)

Instances

Instances details

(∀ (x ∷ k2) (y ∷ k2). LiftedCoercible g g x y) ⇒ HTrans (Telescope g ∷ (k2 → Type) → [k2] → Type) (Telescope g ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods htrans ∷ ∀ c (xs ∷ [k2]) (ys ∷ [k2]) proxy f g0. AllZipN (Prod (Telescope g)) c xs ys ⇒ proxy c → (∀ (x ∷ k2) (y ∷ k2). c x y ⇒ f x → g0 y) → Telescope g f xs → Telescope g g0 ys Source # hcoerce ∷ ∀ (f ∷ k2 → Type) (g0 ∷ k2 → Type) (xs ∷ [k2]) (ys ∷ [k2]). AllZipN (Prod (Telescope g)) (LiftedCoercible f g0) xs ys ⇒ Telescope g f xs → Telescope g g0 ys Source #
HAp (Telescope g ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hap ∷ ∀ (f ∷ k → Type) (g0 ∷ k → Type) (xs ∷ [k]). Prod (Telescope g) (f -.-> g0) xs → Telescope g f xs → Telescope g g0 xs Source #
HSequence (Telescope g ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hsequence' ∷ ∀ (xs ∷ [k]) f (g0 ∷ k → Type). (SListIN (Telescope g) xs, Applicative f) ⇒ Telescope g (f :.: g0) xs → f (Telescope g g0 xs) Source # hctraverse' ∷ ∀ c (xs ∷ [k]) g0 proxy f f'. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) Source # htraverse' ∷ ∀ (xs ∷ [k]) g0 f f'. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k). f a → g0 (f' a)) → Telescope g f xs → g0 (Telescope g f' xs) Source #
HTraverse_ (Telescope g ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hctraverse_ ∷ ∀ c (xs ∷ [k]) g0 proxy f. (AllN (Telescope g) c xs, Applicative g0) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g0 ()) → Telescope g f xs → g0 () Source # htraverse_ ∷ ∀ (xs ∷ [k]) g0 f. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k). f a → g0 ()) → Telescope g f xs → g0 () Source #
(All (Compose Show g) xs, All (Compose Show f) xs) ⇒ Show (Telescope g f xs) Source #
Instance details Defined in Data.SOP.Telescope Methods showsPrec ∷ Int → Telescope g f xs → ShowS # show ∷ Telescope g f xs → String # showList ∷ [Telescope g f xs] → ShowS #
(All (Compose Eq g) xs, All (Compose Eq f) xs) ⇒ Eq (Telescope g f xs) Source #
Instance details Defined in Data.SOP.Telescope Methods (==) ∷ Telescope g f xs → Telescope g f xs → Bool # (/=) ∷ Telescope g f xs → Telescope g f xs → Bool #
(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 Data.SOP.Telescope Methods compare ∷ Telescope g f xs → Telescope g f xs → Ordering # (<) ∷ Telescope g f xs → Telescope g f xs → Bool # (<=) ∷ Telescope g f xs → Telescope g f xs → Bool # (>) ∷ Telescope g f xs → Telescope g f xs → Bool # (>=) ∷ Telescope g f xs → Telescope g f xs → Bool # max ∷ Telescope g f xs → Telescope g f xs → Telescope g f xs # min ∷ Telescope g f xs → Telescope g f xs → Telescope g f xs #
(All (Compose NoThunks g) xs, All (Compose NoThunks f) xs) ⇒ NoThunks (Telescope g f xs) Source #
Instance details Defined in Data.SOP.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 Same (Telescope g ∷ (k2 → Type) → [k2] → Type) Source #
Instance details Defined in Data.SOP.Telescope type Same (Telescope g ∷ (k2 → Type) → [k2] → Type) = Telescope g
type Prod (Telescope g ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.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 Data.SOP.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 Data.SOP.Telescope type AllN (Telescope g ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

sequence ∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). 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 ∷ ∀ {k} (g ∷ k → Type) f (x ∷ k). Telescope g f '[x] → f x Source #

fromTip ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). NS f xs → Telescope (K () ∷ k → Type) f xs Source #

tip ∷ ∀ {k} (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Telescope g f xs → NS f xs Source #

toAtMost ∷ ∀ a (xs ∷ [Type]). Telescope (K a ∷ Type → Type) (K (Maybe a) ∷ Type → Type) xs → AtMost xs a Source #

Bifunctor analogues of SOP functions

bihap ∷ ∀ {k} (g ∷ k → Type) (g' ∷ k → Type) (xs ∷ [k]) (f ∷ k → Type) (f' ∷ k → Type). NP (g -.-> g') xs → NP (f -.-> f') xs → Telescope g f xs → Telescope g' f' xs Source #

Bifunctor analogue of hap

bihczipWith ∷ ∀ {k} c (xs ∷ [k]) proxy h g g' f f'. All c xs ⇒ proxy c → (∀ (x ∷ k). c x ⇒ h x → g x → g' x) → (∀ (x ∷ k). 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 ∷ ∀ {k} (xs ∷ [k]) g g' f f'. SListI xs ⇒ (∀ (x ∷ k). g x → g' x) → (∀ (x ∷ k). f x → f' x) → Telescope g f xs → Telescope g' f' xs Source #

Bifunctor analogue of hmap

bihzipWith ∷ ∀ {k} (xs ∷ [k]) h g g' f f'. SListI xs ⇒ (∀ (x ∷ k). h x → g x → g' x) → (∀ (x ∷ k). 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 ∷ Type → Type) (g ∷ k → Type) (f ∷ k → Type) (x ∷ k) (y ∷ k) Source #

Constructors

Extend
Fields extendWith ∷ f x → m (g x, f y)

newtype Retract (m ∷ Type → Type) (g ∷ k → Type) (f ∷ k → Type) (x ∷ k) (y ∷ k) Source #

Constructors

Retract
Fields retractWith ∷ g x → f y → m (f x)

align Source #

Arguments

∷ ∀ {k} m (g' ∷ k → Type) (g ∷ k → Type) (f' ∷ k → Type) (f ∷ k → Type) (f'' ∷ k → Type) (xs ∷ [k]). 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.

extend Source #

Arguments

∷ ∀ {k} m (h ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). 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.

retract Source #

Arguments

∷ ∀ {k} m (h ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). 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

Simplified API

alignExtend Source #

Arguments

∷ ∀ {k} m (g' ∷ k → Type) (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]) (f' ∷ k → Type) (f'' ∷ k → Type). (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

∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]) (f' ∷ k → Type) (f'' ∷ k → Type). (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

∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Monad m
⇒ InPairs (Extend m g f) xs	How to extend
→ NP (f -.-> (K Bool ∷ k → Type)) 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

∷ ∀ {k} m (g ∷ k → Type) (f ∷ k → Type) (xs ∷ [k]). Monad m
⇒ Tails (Retract m g f) xs	How to retract
→ NP (g -.-> (K Bool ∷ k → Type)) 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 ∷ k → Type) (g ∷ k → Type) (x ∷ k) (y ∷ k) Source #

Constructors

ScanNext
Fields getNext ∷ h x → g x → h y

newtype SimpleTelescope (f ∷ k → Type) (xs ∷ [k]) 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 Data.SOP.Telescope Methods hap ∷ ∀ (f ∷ k → Type) (g ∷ k → Type) (xs ∷ [k]). Prod (SimpleTelescope ∷ (k → Type) → [k] → Type) (f -.-> g) xs → SimpleTelescope f xs → SimpleTelescope g xs Source #
HCollapse (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hcollapse ∷ ∀ (xs ∷ [k]) a. SListIN (SimpleTelescope ∷ (k → Type) → [k] → Type) xs ⇒ SimpleTelescope (K a ∷ k → Type) xs → CollapseTo (SimpleTelescope ∷ (k → Type) → [k] → Type) a Source #
HSequence (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hsequence' ∷ ∀ (xs ∷ [k]) f (g ∷ k → Type). (SListIN (SimpleTelescope ∷ (k → Type) → [k] → Type) xs, Applicative f) ⇒ SimpleTelescope (f :.: g) xs → f (SimpleTelescope g xs) Source # hctraverse' ∷ ∀ c (xs ∷ [k]) g proxy f f'. (AllN (SimpleTelescope ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) Source # htraverse' ∷ ∀ (xs ∷ [k]) g f f'. (SListIN (SimpleTelescope ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g (f' a)) → SimpleTelescope f xs → g (SimpleTelescope f' xs) Source #
HTraverse_ (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hctraverse_ ∷ ∀ c (xs ∷ [k]) g proxy f. (AllN (SimpleTelescope ∷ (k → Type) → [k] → Type) c xs, Applicative g) ⇒ proxy c → (∀ (a ∷ k). c a ⇒ f a → g ()) → SimpleTelescope f xs → g () Source # htraverse_ ∷ ∀ (xs ∷ [k]) g f. (SListIN (SimpleTelescope ∷ (k → Type) → [k] → Type) xs, Applicative g) ⇒ (∀ (a ∷ k). f a → g ()) → SimpleTelescope f xs → g () Source #
type Prod (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.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 Data.SOP.Telescope type SListIN (SimpleTelescope ∷ (k → Type) → [k] → Type) = SListI ∷ [k] → Constraint
type CollapseTo (SimpleTelescope ∷ (k → Type) → [k] → Type) a Source #
Instance details Defined in Data.SOP.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 Data.SOP.Telescope type AllN (SimpleTelescope ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) = All c

scanl ∷ ∀ {a} h (g ∷ a → Type) (x ∷ a) (xs ∷ [a]) (f ∷ a → Type). 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.