Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

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

# Types

Decidable (nullary) relations.

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.