Safe Haskell	None
Language	Haskell2010

Data.SOP.Tails

Contents

Description

Intended for qualified import

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

Synopsis

data Tails (f ∷ k → k → Type) (xs ∷ [k]) where
- TNil ∷ ∀ {k} (f ∷ k → k → Type). Tails f ('[] ∷ [k])
- TCons ∷ ∀ {k} (f ∷ k → k → Type) (x ∷ k) (xs1 ∷ [k]). NP (f x) xs1 → Tails f xs1 → Tails f (x ': xs1)
mk1 ∷ ∀ {k} (f ∷ k → k → Type) (x ∷ k). Tails f '[x]
mk2 ∷ ∀ {k} f (x ∷ k) (y ∷ k). f x y → Tails f '[x, y]
mk3 ∷ ∀ {k} f (x ∷ k) (y ∷ k) (z ∷ k). f x y → f x z → f y z → Tails f '[x, y, z]
extendWithTails ∷ ∀ {k} (xs ∷ [k]) (x ∷ k) (y ∷ k) f. SListI xs ⇒ Index xs x → Index xs y → Tails (Fn2 f) xs → f x → Maybe (f y)
hcmap ∷ ∀ {k} proxy c f g (xs ∷ [k]). All c xs ⇒ proxy c → (∀ (x ∷ k) (y ∷ k). (c x, c y) ⇒ f x y → g x y) → Tails f xs → Tails g xs
hcpure ∷ ∀ {k} proxy f c (xs ∷ [k]). All c xs ⇒ proxy c → (∀ (x ∷ k) (y ∷ k). (c x, c y) ⇒ f x y) → Tails f xs
hmap ∷ ∀ {k} (xs ∷ [k]) f g. SListI xs ⇒ (∀ (x ∷ k) (y ∷ k). f x y → g x y) → Tails f xs → Tails g xs
hpure ∷ ∀ {k} (xs ∷ [k]) f. SListI xs ⇒ (∀ (x ∷ k) (y ∷ k). f x y) → Tails f xs
inPairsToTails ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). All (Top ∷ k → Constraint) xs ⇒ InPairs (Fn2 f) xs → Tails (Fn2 f) xs

Documentation

data Tails (f ∷ k → k → Type) (xs ∷ [k]) where Source #

For every tail (x ': xs) of the list, an f x y for every y in xs

Constructors

TNil ∷ ∀ {k} (f ∷ k → k → Type). Tails f ('[] ∷ [k])
TCons ∷ ∀ {k} (f ∷ k → k → Type) (x ∷ k) (xs1 ∷ [k]). NP (f x) xs1 → Tails f xs1 → Tails f (x ': xs1)

Convenience constructors

mk1 ∷ ∀ {k} (f ∷ k → k → Type) (x ∷ k). Tails f '[x] Source #

mk2 ∷ ∀ {k} f (x ∷ k) (y ∷ k). f x y → Tails f '[x, y] Source #

mk3 ∷ ∀ {k} f (x ∷ k) (y ∷ k) (z ∷ k). f x y → f x z → f y z → Tails f '[x, y, z] Source #

extendWithTails ∷ ∀ {k} (xs ∷ [k]) (x ∷ k) (y ∷ k) f. SListI xs ⇒ Index xs x → Index xs y → Tails (Fn2 f) xs → f x → Maybe (f y) Source #

hcmap ∷ ∀ {k} proxy c f g (xs ∷ [k]). All c xs ⇒ proxy c → (∀ (x ∷ k) (y ∷ k). (c x, c y) ⇒ f x y → g x y) → Tails f xs → Tails g xs Source #

hcpure ∷ ∀ {k} proxy f c (xs ∷ [k]). All c xs ⇒ proxy c → (∀ (x ∷ k) (y ∷ k). (c x, c y) ⇒ f x y) → Tails f xs Source #

hmap ∷ ∀ {k} (xs ∷ [k]) f g. SListI xs ⇒ (∀ (x ∷ k) (y ∷ k). f x y → g x y) → Tails f xs → Tails g xs Source #

hpure ∷ ∀ {k} (xs ∷ [k]) f. SListI xs ⇒ (∀ (x ∷ k) (y ∷ k). f x y) → Tails f xs Source #

inPairsToTails ∷ ∀ {k} (f ∷ k → Type) (xs ∷ [k]). All (Top ∷ k → Constraint) xs ⇒ InPairs (Fn2 f) xs → Tails (Fn2 f) xs Source #