singletons-2.1: A framework for generating singleton types

Copyright (C) 2013 Richard Eisenberg BSD-style (see LICENSE) Richard Eisenberg (eir@cis.upenn.edu) experimental non-portable None Haskell2010

Data.Singletons.Decide

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

 Reading a `Void` value is always a parse error, considering `Void` as a data type with no constructors. 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