Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Decide

Contents

The SDecide class
Supporting definitions

Description

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

Synopsis

The SDecide class

class (kparam ~ KProxy) => SDecide kparam 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 b. Sing a -> Sing b -> Decision (a :~: b) Source

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

Supporting definitions

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

Constructors

Refl :: (:~:) k b b

Instances

Category k ((:~:) k)
TestCoercion k ((:~:) k a)
TestEquality k ((:~:) k a)
(~) k a b => Bounded ((:~:) k a b)
(~) k a b => Enum ((:~:) k a b)
Eq ((:~:) k a b)
((~) * a b, Data a) => Data ((:~:) * a b)
Ord ((:~:) k a b)
(~) k a b => Read ((:~:) k a b)
Show ((:~:) k a b)

data Void :: *

Uninhabited data type

Since: 4.8.0.0

Instances

Eq Void
Data Void
Ord Void
Read Void	Reading a `Void` value is always a parse error, considering `Void` as a data type with no constructors.
Show Void
Ix Void
Generic Void
Exception Void
type Rep Void = D1 D1Void V1

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