| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Type.Dec
Synopsis
- type Neg a = a -> Void
- data Dec a
- class Decidable a where
- 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
- boringYes :: Boring a => Dec a
- absurdNo :: Absurd a => Dec a
Types
Decidable (nullary) relations.
Instances
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.
Neg combinators
toNegNeg :: a -> Neg (Neg a) Source #
We can negate anything twice.
Double-negation elimination is inverse of toNegNeg and generally
impossible.
contradict :: (a -> Neg b) -> b -> Neg a Source #
Weak contradiction.
contraposition :: (a -> b) -> Neg b -> Neg a Source #
A variant of contraposition.