Data.Type.Dec

Types

type Neg a = a -> Void

Intuitionistic negation.

data Dec a

Decidable (nullary) relations.

Constructors

Yes a

No (Neg a)

Instances

Eq a => Eq (Dec a)

Defined in Data.Type.Dec

Methods

(==) :: Dec a -> Dec a -> Bool

(/=) :: Dec a -> Dec a -> Bool

Ord a => Ord (Dec a)

decToBool respects this ordering.

Note: yet if you have p :: a and p :: Neg a, something is wrong.

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

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

Neg combinators

toNegNeg :: a -> Neg (Neg a)

We can negate anything twice.

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

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

Triple negation can be reduced to a single one.

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

Weak contradiction.

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

A variant of contraposition.

Dec combinators

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

Flip Dec branches.

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

Show Dec.

>>> decShow $ Yes ()
"Yes ()"

>>> decShow $ No id
"No <toVoid>"

decToMaybe :: Dec a -> Maybe a

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

decToBool :: Dec a -> Bool

Convert Dec to Bool, forgetting the evidence.