Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Decide

Contents

The SDecide class
Supporting definitions
Orphan instances

Description

Defines the class SDecide, allowing for decidable equality over singletons.

Synopsis

class SDecide k where
- (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
data (a :: k) :~: (b :: k) where
- Refl :: forall {k} (a :: k). a :~: a
data Void
type Refuted a = a -> Void
data Decision a
- = Proved a
- | Disproved (Refuted a)
decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b)
decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b)

The SDecide class

class SDecide k where Source #

Members of the SDecide "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an Eq instance.

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4 Source #

Compute a proof or disproof of equality, given two singletons.

Supporting definitions

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

Constructors

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

Instances

Instances details

TestCoercion ((:~:) a :: k -> Type)
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)
TestEquality ((:~:) a :: k -> Type)
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)
a ~ b => Bounded (a :~: b)
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b maxBound :: a :~: b
a ~ b => Enum (a :~: b)
Instance details Defined in GHC.Internal.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]
a ~ b => Read (a :~: b)
Instance details Defined in GHC.Internal.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 GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS show :: (a :~: b) -> String showList :: [a :~: b] -> ShowS
Eq (a :~: b)
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool (/=) :: (a :~: b) -> (a :~: b) -> Bool
Ord (a :~: b)
Instance details Defined in GHC.Internal.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

data Void #

Instances

Instances details

Semigroup Void
Instance details Defined in GHC.Internal.Base Methods (<>) :: Void -> Void -> Void sconcat :: NonEmpty Void -> Void stimes :: Integral b => b -> Void -> Void
Show Void
Instance details Defined in GHC.Internal.Show Methods showsPrec :: Int -> Void -> ShowS show :: Void -> String showList :: [Void] -> ShowS
Eq Void
Instance details Defined in GHC.Internal.Base Methods (==) :: Void -> Void -> Bool (/=) :: Void -> Void -> Bool
Ord Void
Instance details Defined in GHC.Internal.Base Methods compare :: Void -> Void -> Ordering (<) :: Void -> Void -> Bool (<=) :: Void -> Void -> Bool (>) :: Void -> Void -> Bool (>=) :: Void -> Void -> Bool max :: Void -> Void -> Void min :: Void -> Void -> Void

type Refuted a = a -> Void Source #

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a Source #

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a	Witness for `a`
Disproved (Refuted a)	Proof that no `a` exists

decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b) Source #

A suitable default implementation for testEquality that leverages SDecide.

decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b) Source #

A suitable default implementation for testCoercion that leverages SDecide.

Orphan instances

SDecide k => TestCoercion (WrappedSing :: k -> Type) Source #
Instance details Methods testCoercion :: forall (a :: k) (b :: k). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)
SDecide k => TestEquality (WrappedSing :: k -> Type) Source #
Instance details Methods testEquality :: forall (a :: k) (b :: k). WrappedSing a -> WrappedSing b -> Maybe (a :~: b)