dependent-sum-0.4: Dependent sum type
Safe HaskellSafe
LanguageHaskell98

Data.GADT.Compare

Synopsis

Documentation

class GEq f => GCompare f where Source #

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 :: f a -> f b -> GOrdering a b Source #

Instances

Instances details
GCompare ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a := a0) -> (a := b) -> GOrdering a0 b Source #

data GOrdering a b where Source #

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 :: GOrdering a b 
GEQ :: GOrdering t t 
GGT :: GOrdering a b 

Instances

Instances details
GRead (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

greadsPrec :: Int -> GReadS (GOrdering a) Source #

GShow (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS Source #

Show (f a) => ShowTag (GOrdering a :: k -> Type) (f :: k -> Type) Source # 
Instance details

Defined in Data.Dependent.Sum

Methods

showTaggedPrec :: forall (a0 :: k0). GOrdering a a0 -> Int -> f a0 -> ShowS Source #

Eq (GOrdering a b) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

(==) :: GOrdering a b -> GOrdering a b -> Bool

(/=) :: GOrdering a b -> GOrdering a b -> Bool

Ord (GOrdering a b) Source # 
Instance details

Defined in Data.GADT.Compare

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

Show (GOrdering a b) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

showsPrec :: Int -> GOrdering a b -> ShowS

show :: GOrdering a b -> String

showList :: [GOrdering a b] -> ShowS

class GEq f where Source #

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

Methods

geq :: f a -> f b -> Maybe (a := b) Source #

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 ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

geq :: forall (a0 :: k0) (b :: k0). (a := a0) -> (a := b) -> Maybe (a0 := b) Source #

type (:=) = (:~:) Source #

Backwards compatibility alias; as of GHC 7.8, this is the same as (:~:).

defaultEq :: GEq f => f a -> f b -> Bool Source #

If f has a GEq instance, this function makes a suitable default implementation of (==).

defaultNeq :: GEq f => f a -> f b -> Bool Source #

If f has a GEq instance, this function makes a suitable default implementation of (/=).

weakenOrdering :: GOrdering a b -> Ordering Source #

TODO: Think of a better name

This operation forgets the phantom types of a GOrdering value.

defaultCompare :: GCompare f => f a -> f b -> Ordering Source #

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

Constructors

Refl :: forall k (a :: k). a :~: a 

Instances

Instances details
GRead ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

greadsPrec :: Int -> GReadS ((:=) a) Source #

GShow ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

gshowsPrec :: forall (a0 :: k0). Int -> (a := a0) -> ShowS Source #

GCompare ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a := a0) -> (a := b) -> GOrdering a0 b Source #

GEq ((:=) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

geq :: forall (a0 :: k0) (b :: k0). (a := a0) -> (a := b) -> Maybe (a0 := b) Source #

TestEquality ((:~:) a :: k -> Type) 
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

Ord (f a) => OrdTag ((:=) a :: k -> Type) (f :: k -> Type) Source # 
Instance details

Defined in Data.Dependent.Sum

Methods

compareTagged :: forall (a0 :: k0). (a := a0) -> (a := a0) -> f a0 -> f a0 -> Ordering Source #

Eq (f a) => EqTag ((:=) a :: k -> Type) (f :: k -> Type) Source # 
Instance details

Defined in Data.Dependent.Sum

Methods

eqTagged :: forall (a0 :: k0). (a := a0) -> (a := a0) -> f a0 -> f a0 -> Bool Source #

Read (f a) => ReadTag ((:=) a :: k -> Type) (f :: k -> Type) Source #

In order to make a Read instance for DSum tag f, tag must be able to parse itself as well as any value of the tagged type. GRead together with this class provides the interface by which it can do so.

ReadTag tag f => t is conceptually equivalent to something like this imaginary syntax: (forall a. Inhabited (tag a) => Read (f a)) => t, where Inhabited is an imaginary predicate that characterizes non-empty types, and f and a do not occur free in t.

The Tag example type introduced in the DSum section could be given the following instances, among others:

instance GRead Tag where
    greadsPrec _p str = case tag of
       "AString"   -> [(\k -> k AString, rest)]
       "AnInt"     -> [(\k -> k AnInt,   rest)]
       _           -> []
       where (tag, rest) = break isSpace str
instance ReadTag Tag [] where
    readTaggedPrec AString = readsPrec
    readTaggedPrec AnInt   = readsPrec
Instance details

Defined in Data.Dependent.Sum

Methods

readTaggedPrec :: forall (a0 :: k0). (a := a0) -> Int -> ReadS (f a0) Source #

Show (f a) => ShowTag ((:=) a :: k -> Type) (f :: k -> Type) Source # 
Instance details

Defined in Data.Dependent.Sum

Methods

showTaggedPrec :: forall (a0 :: k0). (a := a0) -> Int -> f a0 -> ShowS Source #

a ~ b => Bounded (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b) 
Instance details

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

Orphan instances

GRead ((:=) a :: k -> Type) Source # 
Instance details

Methods

greadsPrec :: Int -> GReadS ((:=) a) Source #

GShow ((:=) a :: k -> Type) Source # 
Instance details

Methods

gshowsPrec :: forall (a0 :: k0). Int -> (a := a0) -> ShowS Source #