Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K

Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

Moduledec-0.0.6Haskell2010

Data.Type.Dec

Contents

Types
Neg combinators
Dec combinators
Boring

Synopsis

type Neg
data Dec
class Decidable
value toNegNeg
value tripleNeg
value contradict
value contraposition
value decNeg
value decShow
value decToMaybe
value decToBool
value boringYes
value absurdNo

Packagedec-0.0.6
Exports13
LanguageHaskell2010
LicenceBSD-3-Clause
SourceDec.hs

Types

typetype Neg a = a -> Void

Intuitionistic negation.

datadata Dec a

Decidable (nullary) relations.

Constructors

Yes a
No (Neg a)

Instances3Eq, Ord, Boring

Eq a => Eq (Dec a)Defined in dec-0.0.6 · Data.Type.Dec
Ord a => Ord (Dec a)Defined in dec-0.0.6 · Data.Type.Dec
decToBool respects this ordering.
Note: yet if you have p :: a and p :: Neg a, something is wrong.
Decidable a => Boring (Dec a)Defined in dec-0.0.6 · Data.Type.Dec
This relies on the fact that a is proposition in h-Prop sense.

classclass 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

Instances3Decidable

Decidable VoidDefined in dec-0.0.6 · Data.Type.Dec
Void is falsehood.
Decidable ()Defined in dec-0.0.6 · Data.Type.Dec
() is truth.
(Decidable a, Decidable b) => Decidable (a, b)Defined in dec-0.0.6 · Data.Type.Dec
Products of decidable propositions are decidable

Neg combinators

valuetoNegNeg :: a -> Neg (Neg a)

We can negate anything twice.

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

valuetripleNeg :: Neg (Neg (Neg a)) -> Neg a

Triple negation can be reduced to a single one.

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

Weak contradiction.

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

A variant of contraposition.

Dec combinators

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

Flip Dec branches.

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

Show Dec.

Example1 expression

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

Example1 expression

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

valuedecToMaybe :: Dec a -> Maybe a

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

valuedecToBool :: Dec a -> Bool

Convert Dec to Bool, forgetting the evidence.

Boring

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

valueboringYes :: Boring a => Dec a

Yes, it's boring.

valueabsurdNo :: Absurd a => Dec a

No, it's absurd.