HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Moduledec-0.0.6Haskell2010

Data.Type.Dec

  • 2 types
  • 1 class
  • 10 values
  • Packagedec-0.0.6
  • Exports13
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceDec.hs

Types

3 declarations
typetype Neg a = a -> Void
#

Intuitionistic negation.

datadata Dec a
#

Decidable (nullary) relations.

Constructors

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

Instances3Decidable

Neg combinators

4 declarations
valuetoNegNeg :: a -> Neg (Neg a)
#

We can negate anything twice.

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

Dec combinators

4 declarations
valuedecShow :: Show a => Dec a -> String
#

Show Dec.

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

Boring

2 declarations

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