dec-0.0.4: Decidable propositions.

Data.Type.Dec

Synopsis

# Types

type Neg a = a -> Void Source #

Intuitionistic negation.

data Dec a Source #

Decidable (nullary) relations.

Constructors

 Yes a No (Neg a)

#### Instances

Instances details
 Eq a => Eq (Dec a) Source # Instance detailsDefined in Data.Type.Dec Methods(==) :: Dec a -> Dec a -> Bool #(/=) :: Dec a -> Dec a -> Bool # Ord a => Ord (Dec a) Source # decToBool respects this ordering.Note: yet if you have p :: a and p :: Neg a, something is wrong. Instance detailsDefined in Data.Type.Dec Methodscompare :: Dec a -> Dec a -> Ordering #(<) :: Dec a -> Dec a -> Bool #(<=) :: Dec a -> Dec a -> Bool #(>) :: Dec a -> Dec a -> Bool #(>=) :: Dec a -> Dec a -> Bool #max :: Dec a -> Dec a -> Dec a #min :: Dec a -> Dec a -> Dec a #

class Decidable a where Source #

Class of decidable types.

## Law

a should be a Proposition, i.e. the Yes answers should be unique.

Note: We'd want to have decidable equality :~: here too, but that seems to be a deep dive into singletons.

Methods

# Neg combinators

toNegNeg :: a -> Neg (Neg a) Source #

We can negate anything twice.

Double-negation elimination is inverse of toNegNeg and generally impossible.

tripleNeg :: Neg (Neg (Neg a)) -> Neg a Source #

Triple negation can be reduced to a single one.

contradict :: (a -> Neg b) -> b -> Neg a Source #

contraposition :: (a -> b) -> Neg b -> Neg a Source #

A variant of contraposition.

# Dec combinators

decNeg :: Dec a -> Dec (Neg a) Source #

Flip Dec branches.

decShow :: Show a => Dec a -> String Source #

Show Dec.

>>> decShow $Yes () "Yes ()"  >>> decShow$ No id
"No <toVoid>"


decToMaybe :: Dec a -> Maybe a Source #

Convert Dec a to Maybe a, forgetting the No evidence.

decToBool :: Dec a -> Bool Source #

Convert Dec to Bool, forgetting the evidence.