Safe Haskell	Safe-Inferred
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 f xs where
- TZ ∷ !(f x) → Telescope g f (x ': xs)
- TS ∷ !(g x) → !(Telescope g f xs) → Telescope g f (x ': xs)
sequence ∷ ∀ 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 → (∀ 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
bihmap ∷ SListI xs ⇒ (∀ x. g x → g' x) → (∀ x. f x → f' x) → Telescope g f xs → Telescope g' f' xs
bihzipWith ∷ SListI 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
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 ∷ ∀ 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 ∷ ∀ 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 ∷ ∀ 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 f xs 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 ∷ !(f x) → Telescope g f (x ': xs)
TS ∷ !(g x) → !(Telescope g f xs) → Telescope g f (x ': xs)

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 ∷ l1) (ys ∷ l2) proxy f g0. AllZipN (Prod (Telescope g)) c xs ys ⇒ proxy c → (∀ (x ∷ k1) (y ∷ k20). c x y ⇒ f x → g0 y) → Telescope g f xs → Telescope g g0 ys Source # hcoerce ∷ ∀ (f ∷ k1 → Type) (g0 ∷ k20 → Type) (xs ∷ l1) (ys ∷ l2). 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 ∷ k0 → Type) (g0 ∷ k0 → Type) (xs ∷ l). 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 ∷ l) f (g0 ∷ k0 → Type). (SListIN (Telescope g) xs, Applicative f) ⇒ Telescope g (f :.: g0) xs → f (Telescope g g0 xs) Source # 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) Source # 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) Source #
HTraverse_ (Telescope g ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.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 () Source # htraverse_ ∷ ∀ (xs ∷ l) g0 f. (SListIN (Telescope g) xs, Applicative g0) ⇒ (∀ (a ∷ k0). 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 ∷ ∀ 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 → (∀ 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

bihmap ∷ SListI xs ⇒ (∀ x. g x → g' x) → (∀ x. f x → f' x) → Telescope g f xs → Telescope g' f' xs Source #

Bifunctor analogue of hmap

bihzipWith ∷ SListI 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 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

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

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.

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

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 Data.SOP.Telescope Methods hap ∷ ∀ (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 Data.SOP.Telescope Methods hcollapse ∷ ∀ (xs ∷ l) a. SListIN SimpleTelescope xs ⇒ SimpleTelescope (K a) xs → CollapseTo SimpleTelescope a Source #
HSequence (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.Telescope Methods hsequence' ∷ ∀ (xs ∷ l) f (g ∷ k0 → Type). (SListIN SimpleTelescope xs, Applicative f) ⇒ SimpleTelescope (f :.: g) xs → f (SimpleTelescope g xs) Source # 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) Source # 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) Source #
HTraverse_ (SimpleTelescope ∷ (k → Type) → [k] → Type) Source #
Instance details Defined in Data.SOP.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 () Source # htraverse_ ∷ ∀ (xs ∷ l) g f. (SListIN SimpleTelescope xs, Applicative g) ⇒ (∀ (a ∷ k0). 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 ∷ 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.