Safe Haskell	None
Language	Haskell2010

Data.Functor.Pow

Contents

Powers of a functor
Tag of powers of a polynomial functor

Synopsis

data Pow (n :: Natural) (f :: k -> Type) (x :: k) where
- Pow0 :: forall {k} (f :: k -> Type) (x :: k). Pow 0 f x
- PowNZ :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k). Pow' n f x -> Pow n f x
data Pow' (n :: Natural) (f :: k -> Type) (x :: k) where
- Pow1 :: forall {k} (f :: k -> Type) (x :: k). f x -> Pow' 1 f x
- PowEven :: forall {k} (n :: Natural) (m :: Natural) (f :: k -> Type) (x :: k). (KnownNat n, n ~ (m * 2)) => Pow' m f x -> Pow' m f x -> Pow' n f x
- PowOdd :: forall {k} (n :: Natural) (m :: Natural) (f :: k -> Type) (x :: k). (KnownNat n, n ~ ((m * 2) + 1)) => f x -> Pow' m f x -> Pow' m f x -> Pow' n f x
functionToPow :: forall {k} (n :: Nat) f (x :: k). SNat n -> (Finite n -> f x) -> Pow n f x
powToFunction :: forall {k} (n :: Natural) f (x :: k). Pow n f x -> Finite n -> f x
data TagPow (n :: Natural) (t :: Type -> Type) xs where
- TagPow0 :: forall (t :: Type -> Type). TagPow 0 t Void
- TagPowNZ :: forall (n :: Natural) (t :: Type -> Type) xs. TagPow' n t xs -> TagPow n t xs
data TagPow' (n :: Natural) (t :: Type -> Type) xs where
- TagPow1 :: forall (t :: Type -> Type) xs. t xs -> TagPow' 1 t xs
- TagPowEven :: forall (n :: Natural) (m :: Natural) (t :: Type -> Type) xs1 xs2. (KnownNat n, n ~ (m * 2)) => TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either xs1 xs2)
- TagPowOdd :: forall (n :: Natural) (m :: Natural) (t :: Type -> Type) x xs1 xs2. (KnownNat n, n ~ ((m * 2) + 1)) => t x -> TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either x (Either xs1 xs2))
geqPow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GEq t => TagPow n t xs -> TagPow n' t xs' -> Maybe (n :~: n', xs :~: xs')
geqPow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GEq t => TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs')
gcomparePow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GCompare t => TagPow n t xs -> TagPow n' t xs' -> GOrdering '(n, xs) '(n', xs')
gcomparePow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GCompare t => TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs')

Powers of a functor

data Pow (n :: Natural) (f :: k -> Type) (x :: k) where Source #

Pow n f = f :*: f :*: ...(n)... :*: f

Constructors

Pow0 :: forall {k} (f :: k -> Type) (x :: k). Pow 0 f x
PowNZ :: forall {k} (n :: Natural) (f :: k -> Type) (x :: k). Pow' n f x -> Pow n f x

Instances

Instances details

Functor f => Functor (Pow n f) Source #

Instance details

Defined in Data.Functor.Pow

Methods

fmap :: (a -> b) -> Pow n f a -> Pow n f b #

(<$) :: a -> Pow n f b -> Pow n f a #

Polynomial f => Polynomial (Pow n f) Source #

Instance details

Defined in Data.Functor.Polynomial.Class

Associated Types

type Tag (Pow n f)
Instance details Defined in Data.Functor.Polynomial.Class type Tag (Pow n f) = TagPow n (Tag f)

Methods

toPoly :: Pow n f x -> Poly (Tag (Pow n f)) x Source #

fromPoly :: Poly (Tag (Pow n f)) x -> Pow n f x Source #

type Tag (Pow n f) Source #

Instance details

Defined in Data.Functor.Polynomial.Class

type Tag (Pow n f) = TagPow n (Tag f)

data Pow' (n :: Natural) (f :: k -> Type) (x :: k) where Source #

Constructors

Pow1 :: forall {k} (f :: k -> Type) (x :: k). f x -> Pow' 1 f x
PowEven :: forall {k} (n :: Natural) (m :: Natural) (f :: k -> Type) (x :: k). (KnownNat n, n ~ (m * 2)) => Pow' m f x -> Pow' m f x -> Pow' n f x
PowOdd :: forall {k} (n :: Natural) (m :: Natural) (f :: k -> Type) (x :: k). (KnownNat n, n ~ ((m * 2) + 1)) => f x -> Pow' m f x -> Pow' m f x -> Pow' n f x

Instances

Instances details

Functor f => Functor (Pow' n f) Source #

Instance details

Defined in Data.Functor.Pow

Methods

fmap :: (a -> b) -> Pow' n f a -> Pow' n f b #

(<$) :: a -> Pow' n f b -> Pow' n f a #

Polynomial f => Polynomial (Pow' n f) Source #

Instance details

Defined in Data.Functor.Polynomial.Class

Associated Types

type Tag (Pow' n f)
Instance details Defined in Data.Functor.Polynomial.Class type Tag (Pow' n f) = TagPow' n (Tag f)

Methods

toPoly :: Pow' n f x -> Poly (Tag (Pow' n f)) x Source #

fromPoly :: Poly (Tag (Pow' n f)) x -> Pow' n f x Source #

type Tag (Pow' n f) Source #

Instance details

Defined in Data.Functor.Polynomial.Class

type Tag (Pow' n f) = TagPow' n (Tag f)

functionToPow :: forall {k} (n :: Nat) f (x :: k). SNat n -> (Finite n -> f x) -> Pow n f x Source #

powToFunction :: forall {k} (n :: Natural) f (x :: k). Pow n f x -> Finite n -> f x Source #

Tag of powers of a polynomial functor

data TagPow (n :: Natural) (t :: Type -> Type) xs where Source #

When t represents (U,α :: U -> Type), TagPow n t xs represents α^n below:

α^n :: U^n -> Type
α^n(u1, u2, ..., u_n) = α u1 + α u2 + ... + α u_n

This is the tag of Pow n f when t is the tag of f.

Constructors

TagPow0 :: forall (t :: Type -> Type). TagPow 0 t Void
TagPowNZ :: forall (n :: Natural) (t :: Type -> Type) xs. TagPow' n t xs -> TagPow n t xs

Instances

Instances details

GCompare t => GCompare (TagPow n t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods gcompare :: TagPow n t a -> TagPow n t b -> GOrdering a b #
GEq t => GEq (TagPow n t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods geq :: TagPow n t a -> TagPow n t b -> Maybe (a :~: b) #
(forall n. Show (t n)) => GShow (TagPow m t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods gshowsPrec :: Int -> TagPow m t a -> ShowS #
HasFinitary t => HasFinitary (TagPow n t) Source #
Instance details Defined in Data.Functor.Pow Methods withFinitary :: TagPow n t n0 -> (Finitary n0 => r) -> r Source #
(forall n. Show (t n)) => Show (TagPow m t xs) Source #
Instance details Defined in Data.Functor.Pow Methods showsPrec :: Int -> TagPow m t xs -> ShowS # show :: TagPow m t xs -> String # showList :: [TagPow m t xs] -> ShowS #
GEq t => Eq (TagPow n t xs) Source #
Instance details Defined in Data.Functor.Pow Methods (==) :: TagPow n t xs -> TagPow n t xs -> Bool # (/=) :: TagPow n t xs -> TagPow n t xs -> Bool #
GCompare t => Ord (TagPow n t xs) Source #
Instance details Defined in Data.Functor.Pow Methods compare :: TagPow n t xs -> TagPow n t xs -> Ordering # (<) :: TagPow n t xs -> TagPow n t xs -> Bool # (<=) :: TagPow n t xs -> TagPow n t xs -> Bool # (>) :: TagPow n t xs -> TagPow n t xs -> Bool # (>=) :: TagPow n t xs -> TagPow n t xs -> Bool # max :: TagPow n t xs -> TagPow n t xs -> TagPow n t xs # min :: TagPow n t xs -> TagPow n t xs -> TagPow n t xs #

data TagPow' (n :: Natural) (t :: Type -> Type) xs where Source #

Constructors

TagPow1 :: forall (t :: Type -> Type) xs. t xs -> TagPow' 1 t xs
TagPowEven :: forall (n :: Natural) (m :: Natural) (t :: Type -> Type) xs1 xs2. (KnownNat n, n ~ (m * 2)) => TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either xs1 xs2)
TagPowOdd :: forall (n :: Natural) (m :: Natural) (t :: Type -> Type) x xs1 xs2. (KnownNat n, n ~ ((m * 2) + 1)) => t x -> TagPow' m t xs1 -> TagPow' m t xs2 -> TagPow' n t (Either x (Either xs1 xs2))

Instances

Instances details

GCompare t => GCompare (TagPow' n t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods gcompare :: TagPow' n t a -> TagPow' n t b -> GOrdering a b #
GEq t => GEq (TagPow' n t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods geq :: TagPow' n t a -> TagPow' n t b -> Maybe (a :~: b) #
(forall m. Show (t m)) => GShow (TagPow' n t :: Type -> Type) Source #
Instance details Defined in Data.Functor.Pow Methods gshowsPrec :: Int -> TagPow' n t a -> ShowS #
HasFinitary t => HasFinitary (TagPow' n t) Source #
Instance details Defined in Data.Functor.Pow Methods withFinitary :: TagPow' n t n0 -> (Finitary n0 => r) -> r Source #
(forall m. Show (t m)) => Show (TagPow' n t xs) Source #
Instance details Defined in Data.Functor.Pow Methods showsPrec :: Int -> TagPow' n t xs -> ShowS # show :: TagPow' n t xs -> String # showList :: [TagPow' n t xs] -> ShowS #
GEq t => Eq (TagPow' n t xs) Source #
Instance details Defined in Data.Functor.Pow Methods (==) :: TagPow' n t xs -> TagPow' n t xs -> Bool # (/=) :: TagPow' n t xs -> TagPow' n t xs -> Bool #
GCompare t => Ord (TagPow' n t xs) Source #
Instance details Defined in Data.Functor.Pow Methods compare :: TagPow' n t xs -> TagPow' n t xs -> Ordering # (<) :: TagPow' n t xs -> TagPow' n t xs -> Bool # (<=) :: TagPow' n t xs -> TagPow' n t xs -> Bool # (>) :: TagPow' n t xs -> TagPow' n t xs -> Bool # (>=) :: TagPow' n t xs -> TagPow' n t xs -> Bool # max :: TagPow' n t xs -> TagPow' n t xs -> TagPow' n t xs # min :: TagPow' n t xs -> TagPow' n t xs -> TagPow' n t xs #

geqPow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GEq t => TagPow n t xs -> TagPow n' t xs' -> Maybe (n :~: n', xs :~: xs') Source #

geqPow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GEq t => TagPow' n t xs -> TagPow' n' t xs' -> Maybe (n :~: n', xs :~: xs') Source #

gcomparePow :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GCompare t => TagPow n t xs -> TagPow n' t xs' -> GOrdering '(n, xs) '(n', xs') Source #

gcomparePow' :: forall (t :: Type -> Type) (n :: Natural) xs (n' :: Natural) xs'. GCompare t => TagPow' n t xs -> TagPow' n' t xs' -> GOrdering '(n, xs) '(n', xs') Source #