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 first-order logic constructions which are expressed as Haskell types, based on those in Hout.Logic.Intuitionistic. This gives definitions for

- the universal quantifier
- the existential quantifier
- first-order equality

It also gives the natural deduction rules for these constructions, though they are not very useful to the programmer.

## Synopsis

- data Witness (a :: k) where
- Witness :: (a :: Type) -> Witness a
- ConstraintWitness :: Witness (a :: Constraint)
- DataKindWitness :: Witness (a :: (k :: Type))

- data Exists k (p :: k -> *) where
- data Forall k (p :: k -> *) = Forall (forall (a :: k). p a)
- data Equal (a :: k) (b :: k) where
- existsIntro :: Witness (a :: k) -> p a -> Exists k p
- existsElim :: (forall (a :: k). Witness a -> p a -> b) -> Exists k p -> b
- forallIntro :: (forall (a :: k). p a) -> Forall k p
- forallElim :: Forall k p -> p (a :: k)
- eqRefl :: Equal a a
- eqSym :: Equal a b -> Equal b a
- eqTrans :: Equal a b -> Equal b c -> Equal a c
- eqRewrite :: Equal a b -> p a -> p b

# Documentation

data Witness (a :: k) where Source #

A witness of a kind inhabitant. `Witness`

es can be constructed for the
`Type`

kind, `Constraint`

kind, or any data kind.

Witness :: (a :: Type) -> Witness a | Because Type is the only kind of habitats, it is the only constructor for which we can demand an inhabitant |

ConstraintWitness :: Witness (a :: Constraint) | |

DataKindWitness :: Witness (a :: (k :: Type)) |

data Forall k (p :: k -> *) Source #

The forall quantifier. As with `Exists`

, the predicate is required to
return a `Type`

. Despite `forall`

being a Haskell built-in, the lack of
support for impredicative types means that a newtype is declared for
usability.

Forall (forall (a :: k). p a) |

existsIntro :: Witness (a :: k) -> p a -> Exists k p Source #

existsElim :: (forall (a :: k). Witness a -> p a -> b) -> Exists k p -> b Source #

Exists elimination, as a continuation.

Note that this has to be expressed in this continuation style because existential types are not allowed in the return type

forallIntro :: (forall (a :: k). p a) -> Forall k p Source #

forallElim :: Forall k p -> p (a :: k) Source #