dec-0.0.3: Decidable propositions.

Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Type.Dec

Contents

Types
Neg combinators
Dec combinators

Synopsis

type Neg a = a -> Void
data Dec a
- = Yes a
- | No (Neg a)
class Decidable a where
- decide :: Dec a
toNegNeg :: a -> Neg (Neg a)
tripleNeg :: Neg (Neg (Neg a)) -> Neg a
contradict :: (a -> Neg b) -> b -> Neg a
contraposition :: (a -> b) -> Neg b -> Neg a
decNeg :: Dec a -> Dec (Neg a)
decShow :: Show a => Dec a -> String
decToMaybe :: Dec a -> Maybe a
decToBool :: Dec a -> Bool

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 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 #

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.