dec-0.0.6: Decidable propositions.
Safe HaskellSafe
LanguageHaskell2010

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
Decidable a => Boring (Dec a) Source #

This relies on the fact that a is proposition in h-Prop sense.

Since: 0.0.5

Instance details

Defined in Data.Type.Dec

Methods

boring :: Dec a #

Eq a => Eq (Dec a) Source # 
Instance details

Defined 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 details

Defined in Data.Type.Dec

Methods

compare :: 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

decide :: Dec a Source #

Instances

Instances details
Decidable Void Source #

Void is falsehood.

Since: 0.0.5

Instance details

Defined in Data.Type.Dec

Methods

decide :: Dec Void Source #

Decidable () Source #

() is truth.

Since: 0.0.5

Instance details

Defined in Data.Type.Dec

Methods

decide :: Dec () Source #

(Decidable a, Decidable b) => Decidable (a, b) Source #

Products of decidable propositions are decidable

Since: 0.0.5

Instance details

Defined in Data.Type.Dec

Methods

decide :: Dec (a, b) Source #

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 #

Weak contradiction.

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.

Boring

Dec a can be Boring in two ways: When a is Boring or Absurd.

boringYes :: Boring a => Dec a Source #

Yes, it's boring.

Since: 0.0.5

absurdNo :: Absurd a => Dec a Source #

No, it's absurd.

Since: 0.0.5