singletons-0.10.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.Eq

Description

Defines the SEq singleton version of the Eq type class.

Synopsis

Documentation

class (kparam ~ KProxy) => SEq kparam where Source

The singleton analogue of Eq. Unlike the definition for Eq, it is required that instances define a body for '(%:==)'. You may also supply a body for '(%:/=)'.

Methods

(%:==) :: forall a b. Sing a -> Sing b -> Sing (a :== b) Source

Boolean equality on singletons

(%:/=) :: forall a b. Sing a -> Sing b -> Sing (a :/= b) Source

Boolean disequality on singletons

Instances

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

type family a == b :: Bool

A type family to compute Boolean equality. Instances are provided only for open kinds, such as * and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

Instances

type (==) Bool a b = EqBool a b 
type (==) Ordering a b = EqOrdering a b 
type (==) * a b = EqStar a b 
type (==) Nat a b = EqNat a b 
type (==) Symbol a b = EqSymbol a b 
type (==) () a b = EqUnit a b 
type (==) [k] a b = EqList k a b 
type (==) (Maybe k) a b = EqMaybe k a b 
type (==) (k -> k1) a b = EqArrow k k1 a b 
type (==) (Either k k1) a b = EqEither k k1 a b 
type (==) ((,) k k1) a b = Eq2 k k1 a b 
type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b 
type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b 
type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b 
type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b 
type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b 
type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b 
type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b 
type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 k k1 k2 k3 k4 k5 k6 k7 k8 k9 a b 
type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b = Eq11 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 a b 
type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b = Eq12 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 a b 
type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b = Eq13 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 a b 
type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b = Eq14 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 a b 
type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b 

type (:==) a b = a == b Source

A re-export of the type-level (==) that conforms to the singletons naming convention.

type (:/=) a b = Not (a :== b) Source

A type synonym conforming to singletons naming conventions