singletons-1.0: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Decide

Contents

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.

Instances

SDecide Bool (KProxy Bool) 
SDecide Ordering (KProxy Ordering) 
SDecide * (KProxy *) 
SDecide Nat (KProxy Nat) 
SDecide Symbol (KProxy Symbol) 
SDecide () (KProxy ()) 
SDecide a0 (KProxy a0) => SDecide [a] (KProxy [a]) 
SDecide a0 (KProxy a0) => SDecide (Maybe a) (KProxy (Maybe a)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0)) => SDecide (Either a b) (KProxy (Either a b)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0)) => SDecide ((,) a b) (KProxy ((,) a b)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0)) => SDecide ((,,) a b c) (KProxy ((,,) a b c)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0)) => SDecide ((,,,) a b c d) (KProxy ((,,,) a b c d)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0)) => SDecide ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0), SDecide f0 (KProxy f0)) => SDecide ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) 
(SDecide a0 (KProxy a0), SDecide b0 (KProxy b0), SDecide c0 (KProxy c0), SDecide d0 (KProxy d0), SDecide e0 (KProxy e0), SDecide f0 (KProxy f0), SDecide g0 (KProxy g0)) => SDecide ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) 

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 a1 a1 

Instances

TestCoercion k ((:~:) k a) 
TestEquality k ((:~:) k a) 
Typeable (k -> k -> *) ((:~:) k) 
(~) 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 Source

A logically uninhabited data type.

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 
Typeable * Void 
type Rep 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