Safe Haskell | Safe |
---|---|

Language | Haskell98 |

- type (:=) = (:~:)
- class GEq f where
- defaultEq :: GEq f => f a -> f b -> Bool
- defaultNeq :: GEq f => f a -> f b -> Bool
- data GOrdering a b where
- weakenOrdering :: GOrdering a b -> Ordering
- class GEq f => GCompare f where
- defaultCompare :: GCompare f => f a -> f b -> Ordering
- data a :~: b :: k -> k -> * where

# Documentation

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

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)

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 '(/=)'.

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.

weakenOrdering :: GOrdering a b -> Ordering Source

TODO: Think of a better name

This operation forgets the phantom types of a `GOrdering`

value.

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`

).

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

data a :~: b :: k -> k -> * where infix 4

Propositional equality. If `a :~: b`

is inhabited by some terminating
value, then the type `a`

is the same as the type `b`

. To use this equality
in practice, pattern-match on the `a :~: b`

to get out the `Refl`

constructor;
in the body of the pattern-match, the compiler knows that `a ~ b`

.

*Since: 4.7.0.0*

TestEquality k ((:~:) k a) | |

GRead k ((:=) k a) | |

GShow k ((:=) k a) | |

GCompare k ((:=) k a) | |

GEq k ((:=) k a) | |

Ord (f a) => OrdTag k ((:=) k a) f | |

Eq (f a) => EqTag k ((:=) k a) f | |

Read (f a) => ReadTag k ((:=) k a) f | In order to make a
The 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 |

Show (f a) => ShowTag k ((:=) k a) f | |

Typeable (k -> k -> *) ((:~:) k) | |

(~) k a b => Bounded ((:~:) k a b) | |

(~) k a b => Enum ((:~:) k a b) | |

Eq ((:~:) k a b) | |

Ord ((:~:) k a b) | |

(~) k a b => Read ((:~:) k a b) | |

Show ((:~:) k a b) |