singletons-3.0.4: Basic singleton types and definitions

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 infix 4 Source #

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: base-4.7.0.0

Constructors

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

#### Instances

Instances details

TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b Source #

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

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

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

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

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

a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

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

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

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

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

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

data Void Source #

Uninhabited data type

Since: base-4.8.0.0

#### Instances

Instances details

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

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) Source #
SDecide k => TestEquality (WrappedSing :: k -> Type) Source # |
Instance details Methods testEquality :: forall (a :: k) (b :: k). WrappedSing a -> WrappedSing b -> Maybe (a :~: b) Source #