| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Type.Dec
Contents
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
| Eq a => Eq ( Dec a) Source # | |
| Ord a => Ord ( Dec a) Source # |
Note:
yet if you have
|
|
Defined in Data.Type.Dec |
|
| Decidable a => Boring ( Dec a) Source # |
This relies on the fact that
Since: 0.0.5 |
|
Defined in Data.Type.Dec |
|
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.