Safe Haskell	None
Language	Haskell2010

Data.Functor.Polynomial.Tag

Contents

The type class for tags
Tags
Reexports

Description

This module provides a way to represent "tag" of various polynomial data types. For example, a GADT TagMaybe represents a functor of the same shape of Maybe.

data TagMaybe n where
   TagNothing :: TagMaybe Void -- ^ Nothing takes 0 parameter
   TagJust    :: TagMaybe ()   -- ^ Just takes 1 paramerer

Synopsis

class HasFinitary (tag :: Type -> Type) where
- withFinitary :: tag n -> (Finitary n => r) -> r
data TagMaybe n where
- TagNothing :: TagMaybe Void
- TagJust :: TagMaybe ()
data TagList a where
- TagList :: forall (n :: Nat). KnownNat n => TagList (Finite Integer n)
type TagFn = (:~:) :: k -> k -> Type
data TagV n
data TagK c n where
- TagK :: forall c. c -> TagK c Void
type TagSum = (:+:) :: (k -> Type) -> (k -> Type) -> k -> Type
data TagMul (f :: Type -> Type) (g :: Type -> Type) x where
- TagMul :: forall (f :: Type -> Type) x1 (g :: Type -> Type) y. !(f x1) -> !(g y) -> TagMul f g (Either x1 y)
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
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')
data TagComp (t :: Type -> Type) (u :: Type -> Type) n where
- TagComp :: forall (t :: Type -> Type) a (u :: Type -> Type) n. t a -> TagPow (Cardinality a) u n -> TagComp t u n
data TagDay (t :: Type -> Type) (u :: Type -> Type) n where
- TagDay :: forall (t :: Type -> Type) n1 (u :: Type -> Type) m. t n1 -> u m -> TagDay t u (n1, m)
class GShow (t :: k -> Type) where
- gshowsPrec :: forall (a :: k). Int -> t a -> ShowS
class GEq (f :: k -> Type) where
- geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
class GEq f => GCompare (f :: k -> Type) where
- gcompare :: forall (a :: k) (b :: k). f a -> f b -> GOrdering a b
data GOrdering (a :: k) (b :: k) where
- GLT :: forall {k} (a :: k) (b :: k). GOrdering a b
- GEQ :: forall {k} (a :: k). GOrdering a a
- GGT :: forall {k} (a :: k) (b :: k). GOrdering a b

The type class for tags

class HasFinitary (tag :: Type -> Type) where Source #

Methods

withFinitary :: tag n -> (Finitary n => r) -> r Source #

Instances

Instances details

HasFinitary TagList Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagList n -> (Finitary n => r) -> r Source #
HasFinitary TagMaybe Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagMaybe n -> (Finitary n => r) -> r Source #
HasFinitary TagV Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagV n -> (Finitary n => r) -> r Source #
HasFinitary (TagK c) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagK c n -> (Finitary n => r) -> r Source #
Finitary n => HasFinitary ((:~:) n) Source #
Instance details Defined in Data.GADT.HasFinitary Methods withFinitary :: (n :~: n0) -> (Finitary n0 => r) -> r Source #
HasFinitary u => HasFinitary (TagComp t u) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagComp t u n -> (Finitary n => r) -> r Source #
(HasFinitary t, HasFinitary u) => HasFinitary (TagDay t u) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagDay t u n -> (Finitary n => r) -> r Source #
(HasFinitary t1, HasFinitary t2) => HasFinitary (TagMul t1 t2) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods withFinitary :: TagMul t1 t2 n -> (Finitary n => r) -> r Source #
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 #
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 #
(HasFinitary t1, HasFinitary t2) => HasFinitary (t1 :+: t2) Source #
Instance details Defined in Data.GADT.HasFinitary Methods withFinitary :: (t1 :+: t2) n -> (Finitary n => r) -> r Source #

Tags

data TagMaybe n where Source #

Tag of Maybe.

Constructors

TagNothing :: TagMaybe Void
TagJust :: TagMaybe ()

Instances

Instances details

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

data TagList a where Source #

Constructors

:: forall (n :: Nat). KnownNat n => TagList (Finite Integer n)

Instances

type TagFn = (:~:) :: k -> k -> Type Source #

TagFn n represents ((), const n :: () -> Type).

This is the tag of (->) r functor.

It's also the tag of Proxy and Identity, by being isomorphic to (->) Void and (->) () respectively.

TagFn Void   -- Tag of Proxy
TagFn ()     -- Tag of Identity

data TagV n Source #

TagV n is an empty type for any n. It represents (∅, α = absurd :: ∅ -> Nat).

This is the tag of V1.

Instances

Instances details

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

data TagK c n where Source #

TagK c n represents (c, α), where α is a constant function to Void:

α = const Void :: c -> Type

This is the tag of Const.

Constructors

TagK :: forall c. c -> TagK c Void

Instances

Instances details

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

type TagSum = (:+:) :: (k -> Type) -> (k -> Type) -> k -> Type Source #

When t1, t2 represents (U, α1) and (V,α2) respectively,

α1 :: U -> Nat
α2 :: V -> Nat

TagSum t1 t2 represents (Either U V, β = either α1 α2).

β :: Either U V -> Nat
β (Left u)  = α1(u)
β (Right v) = α2(v)

This is the tag of f :+: g, when t1, t2 is the tag of f, g respectively.

data TagMul (f :: Type -> Type) (g :: Type -> Type) x where Source #

When t1, t2 represents (U, α1) and (V,α2) respectively,

α1 :: U -> Nat
α2 :: V -> Nat

TagMul t1 t2 represents the direct product (U,V) and the function β on it:

β :: (U,V) -> Nat
β(u,v) = α1 u + α2 v

This is the tag of f :*: g when t1, t2 is the tag of f, g respectively.

Constructors

TagMul :: forall (f :: Type -> Type) x1 (g :: Type -> Type) y. !(f x1) -> !(g y) -> TagMul f g (Either x1 y)

Instances

Instances details

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

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 #

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 #

data TagComp (t :: Type -> Type) (u :: Type -> Type) n where Source #

When t, u is the tag of f, g respectively, TagComp t u is the tag of f :.: g.

Constructors

TagComp :: forall (t :: Type -> Type) a (u :: Type -> Type) n. t a -> TagPow (Cardinality a) u n -> TagComp t u n

Instances

Instances details

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

data TagDay (t :: Type -> Type) (u :: Type -> Type) n where Source #

Constructors

TagDay :: forall (t :: Type -> Type) n1 (u :: Type -> Type) m. t n1 -> u m -> TagDay t u (n1, m)

Instances

Instances details

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

Reexports

class GShow (t :: k -> Type) where #

Show-like class for 1-type-parameter GADTs. GShow t => ... is equivalent to something like (forall a. Show (t a)) => .... The easiest way to create instances would probably be to write (or derive) an instance Show (T a), and then simply say:

instance GShow t where gshowsPrec = defaultGshowsPrec

Methods

gshowsPrec :: forall (a :: k). Int -> t a -> ShowS #

Instances

Instances details

GShow SNat
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: Nat). Int -> SNat a -> ShowS #
GShow SChar
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: Char). Int -> SChar a -> ShowS #
GShow SSymbol
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: Symbol). Int -> SSymbol a -> ShowS #
GShow TagList Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagList a -> ShowS #
GShow TagMaybe Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagMaybe a -> ShowS #
GShow TagV Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagV a -> ShowS #
Show c => GShow (TagK c :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagK c a -> ShowS #
GShow (TypeRep :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a :: k). Int -> TypeRep a -> ShowS #
(forall n. Show (t n), forall n. Show (u n)) => GShow (TagComp t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagComp t u a -> ShowS #
(forall n. Show (t n), forall n. Show (u n)) => GShow (TagDay t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagDay t u a -> ShowS #
(forall n. Show (t1 n), forall n. Show (t2 n)) => GShow (TagMul t1 t2 :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gshowsPrec :: Int -> TagMul t1 t2 a -> ShowS #
(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 #
(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 #
GShow ((:~:) a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> (a :~: a0) -> ShowS #
GShow (GOrdering a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> GOrdering a a0 -> ShowS #
(GShow a, GShow b) => GShow (Product a b :: k -> Type)	`>>>` `gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)`"Pair Refl Refl"
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> Product a b a0 -> ShowS #
(GShow a, GShow b) => GShow (Sum a b :: k -> Type)	`>>>` `gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)`"InL Refl"
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> Sum a b a0 -> ShowS #
GShow ((:~~:) a :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> (a :~~: a0) -> ShowS #
(GShow a, GShow b) => GShow (a :*: b :: k -> Type)	`>>>` `gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)`"Refl :: Refl" Since: some-1.0.4*
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> (a :*: b) a0 -> ShowS #
(GShow a, GShow b) => GShow (a :+: b :: k -> Type)	`>>>` `gshow (L1 Refl :: ((:~:) Int :+: (:~:) Bool) Int)`"L1 Refl" Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> (a :+: b) a0 -> ShowS #

class GEq (f :: k -> Type) where #

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

This class is sometimes confused with TestEquality from base. TestEquality only checks type equality.

Consider

>>> data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int

The correct TestEquality Tag instance is

>>> :{
instance TestEquality Tag where
    testEquality TagInt1 TagInt1 = Just Refl
    testEquality TagInt1 TagInt2 = Just Refl
    testEquality TagInt2 TagInt1 = Just Refl
    testEquality TagInt2 TagInt2 = Just Refl
:}

While we can define

instance GEq Tag where
   geq = testEquality

this will mean we probably want to have

instance Eq Tag where
   _ == _ = True

Note: In the future version of some package (to be released around GHC-9.6 / 9.8) the forall a. Eq (f a) constraint will be added as a constraint to GEq, with a law relating GEq and Eq:

geq x y = Just Refl   ⇒  x == y = True        ∀ (x :: f a) (y :: f b)
x == y                ≡  isJust (geq x y)     ∀ (x, y :: f a)

So, the more useful GEq Tag instance would differentiate between different constructors:

>>> :{
instance GEq Tag where
    geq TagInt1 TagInt1 = Just Refl
    geq TagInt1 TagInt2 = Nothing
    geq TagInt2 TagInt1 = Nothing
    geq TagInt2 TagInt2 = Just Refl
:}

which is consistent with a derived Eq instance for Tag

>>> deriving instance Eq (Tag a)

Note that even if a ~ b, the geq (x :: f a) (y :: f b) may be Nothing (when value terms are inequal).

The consistency of GEq and Eq is easy to check by exhaustion:

>>> let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True
>>> (checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)
(True,True,True,True)

>>> let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)
>>> (checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)
(True,True,True,True)

Methods

geq :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

Produce a witness of type-equality, if one exists.

A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
    Refl <- geq t1 t2
    return x

Or in a list comprehension:

extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

(Making use of the DSum type from Data.Dependent.Sum in both examples)

Instances

Instances details

GEq SNat
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #
GEq SChar
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) #
GEq SSymbol
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) #
GEq TagList Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagList a -> TagList b -> Maybe (a :~: b) #
GEq TagMaybe Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagMaybe a -> TagMaybe b -> Maybe (a :~: b) #
GEq TagV Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagV a -> TagV b -> Maybe (a :~: b) #
Eq c => GEq (TagK c :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagK c a -> TagK c b -> Maybe (a :~: b) #
GEq (TypeRep :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) #
(GEq t, GEq u) => GEq (TagComp t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagComp t u a -> TagComp t u b -> Maybe (a :~: b) #
(GEq t, GEq u) => GEq (TagDay t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagDay t u a -> TagDay t u b -> Maybe (a :~: b) #
(GEq t1, GEq t2) => GEq (TagMul t1 t2 :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods geq :: TagMul t1 t2 a -> TagMul t1 t2 b -> Maybe (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) #
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) #
GEq ((:~:) a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
(GEq a, GEq b) => GEq (Product a b :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0) #
(GEq a, GEq b) => GEq (Sum a b :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0) #
GEq ((:~~:) a :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
(GEq a, GEq b) => GEq (a :*: b :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k) (b0 :: k). (a :: b) a0 -> (a :: b) b0 -> Maybe (a0 :~: b0) #
(GEq f, GEq g) => GEq (f :+: g :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: k) (b :: k). (f :+: g) a -> (f :+: g) b -> Maybe (a :~: b) #

class GEq f => GCompare (f :: k -> Type) where #

Type class for comparable GADT-like structures. When 2 things are equal, must return a witness that their parameter types are equal as well (GEQ).

Methods

gcompare :: forall (a :: k) (b :: k). f a -> f b -> GOrdering a b #

Instances

Instances details

GCompare SNat
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b #
GCompare SChar
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> GOrdering a b #
GCompare SSymbol
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> GOrdering a b #
GCompare TagList Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagList a -> TagList b -> GOrdering a b #
GCompare TagMaybe Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagMaybe a -> TagMaybe b -> GOrdering a b #
GCompare TagV Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagV a -> TagV b -> GOrdering a b #
Ord c => GCompare (TagK c :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagK c a -> TagK c b -> GOrdering a b #
GCompare (TypeRep :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> GOrdering a b #
(GCompare t, GCompare u) => GCompare (TagComp t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagComp t u a -> TagComp t u b -> GOrdering a b #
(GCompare t, GCompare u) => GCompare (TagDay t u :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagDay t u a -> TagDay t u b -> GOrdering a b #
(GCompare t1, GCompare t2) => GCompare (TagMul t1 t2 :: Type -> Type) Source #
Instance details Defined in Data.Functor.Polynomial.Tag Methods gcompare :: TagMul t1 t2 a -> TagMul t1 t2 b -> GOrdering a b #
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 #
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 #
GCompare ((:~:) a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> GOrdering a0 b #
(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). Product a b a0 -> Product a b b0 -> GOrdering a0 b0 #
(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0 #
GCompare ((:~~:) a :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> GOrdering a0 b #
(GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k) (b0 :: k). (a :: b) a0 -> (a :: b) b0 -> GOrdering a0 b0 #
(GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type)	Since: some-1.0.4
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: k) (b :: k). (f :+: g) a -> (f :+: g) b -> GOrdering a b #

data GOrdering (a :: k) (b :: k) where #

A type for the result of comparing GADT constructors; the type parameters of the GADT values being compared are included so that in the case where they are equal their parameter types can be unified.

Constructors

GLT :: forall {k} (a :: k) (b :: k). GOrdering a b
GEQ :: forall {k} (a :: k). GOrdering a a
GGT :: forall {k} (a :: k) (b :: k). GOrdering a b

Instances

Instances details

GRead (GOrdering a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS (GOrdering a) #
GShow (GOrdering a :: k -> Type)
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k). Int -> GOrdering a a0 -> ShowS #
Show (GOrdering a b)
Instance details Defined in Data.GADT.Internal Methods showsPrec :: Int -> GOrdering a b -> ShowS # show :: GOrdering a b -> String # showList :: [GOrdering a b] -> ShowS #
Eq (GOrdering a b)
Instance details Defined in Data.GADT.Internal Methods (==) :: GOrdering a b -> GOrdering a b -> Bool # (/=) :: GOrdering a b -> GOrdering a b -> Bool #
Ord (GOrdering a b)
Instance details Defined in Data.GADT.Internal Methods compare :: GOrdering a b -> GOrdering a b -> Ordering # (<) :: GOrdering a b -> GOrdering a b -> Bool # (<=) :: GOrdering a b -> GOrdering a b -> Bool # (>) :: GOrdering a b -> GOrdering a b -> Bool # (>=) :: GOrdering a b -> GOrdering a b -> Bool # max :: GOrdering a b -> GOrdering a b -> GOrdering a b # min :: GOrdering a b -> GOrdering a b -> GOrdering a b #