Copyright | (c) Isaac van Bakel 2020 |
---|---|

License | BSD-3 |

Maintainer | ivb@vanbakel.io |

Stability | experimental |

Portability | POSIX |

Safe Haskell | Safe |

Language | Haskell2010 |

This module contains type aliases for intuitionistic logic constructions which are expressed as Haskell types.

It also gives the natural deduction rules for those aliases, except when they are aliases of arrow types. For example, implies-introduction and elimination are both Haskell arrow constructions (function abstraction and application, respectively) so no rule is given.

## Synopsis

- type True = ()
- type False = Void
- type (/\) a b = (a, b)
- type (\/) a b = Either a b
- type Not a = a -> False
- type (<->) a b = (a -> b) /\ (b -> a)
- andIntro :: a -> b -> a /\ b
- andElimLeft :: (a /\ b) -> a
- andElimRight :: (a /\ b) -> b
- orIntroLeft :: a -> a \/ b
- orIntroRight :: b -> a \/ b
- orElim :: (a -> c) -> (b -> c) -> (a \/ b) -> c
- trueIntro :: True
- exFalso :: False -> a
- iffIntro :: (a -> b) -> (b -> a) -> a <-> b
- iffElimLeft :: (a <-> b) -> a -> b
- iffElimRight :: (a <-> b) -> b -> a

# Documentation

type Not a = a -> False Source #

Negation of a type. Because this is an arrow type alias, not-introduction and elimination are not part of this module.

type (<->) a b = (a -> b) /\ (b -> a) Source #

Iff. Some derived rules are defined for iff for the sake of completeness.

andElimLeft :: (a /\ b) -> a Source #

andElimRight :: (a /\ b) -> b Source #

orIntroLeft :: a -> a \/ b Source #

orIntroRight :: b -> a \/ b Source #

exFalso :: False -> a Source #

Ex Falso Quod Libet - it is recommended when writing functions of this
form to use the `EmptyCase`

extension, to make the compiler check that
the type is uninhabited.

iffElimLeft :: (a <-> b) -> a -> b Source #

iffElimRight :: (a <-> b) -> b -> a Source #