Safe Haskell  SafeInferred 

Language  Haskell2010 
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
 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 sopcore
conventions, supporting
functor (hmap
, hcmap
), applicative (hap
, hpure
), foldable
(hcollapse
) and traversable (hsequence'
). However, since Telescope
is a bifunctor, it cannot reuse the sopcore
classes. The naming scheme
of the functions is adopted from sopcore
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.
Instances
(∀ (x ∷ k2) (y ∷ k2). LiftedCoercible g g x y) ⇒ HTrans (Telescope g ∷ (k2 → Type) → [k2] → Type) (Telescope g ∷ (k2 → Type) → [k2] → Type) Source #  
Defined in Data.SOP.Telescope 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 #  
HSequence (Telescope g ∷ (k → Type) → [k] → Type) Source #  
Defined in Data.SOP.Telescope 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 #  
Defined in Data.SOP.Telescope 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 #  
(All (Compose Eq g) xs, All (Compose Eq f) xs) ⇒ Eq (Telescope g f xs) 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 #  
Defined in Data.SOP.Telescope 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 #  
type Same (Telescope g ∷ (k2 → Type) → [k2] → Type) Source #  
type Prod (Telescope g ∷ (k → Type) → [k] → Type) Source #  
type SListIN (Telescope g ∷ (k → Type) → [k] → Type) Source #  
Defined in Data.SOP.Telescope  
type AllN (Telescope g ∷ (k → Type) → [k] → Type) (c ∷ k → Constraint) Source #  
Defined in Data.SOP.Telescope 
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
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 #
Extend  

newtype Retract m g f x y Source #
Retract  

∷ ∀ 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.
∷ ∀ 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.
∷ ∀ 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
∷ (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.
∷ (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
Additional API
newtype SimpleTelescope f xs Source #
Telescope
with both functors set to the same f
SimpleTelescope  
