| Copyright | (c) Isaac van Bakel 2020 |
|---|---|
| License | BSD-3 |
| Maintainer | ivb@vanbakel.io |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Hout.Logic.FirstOrder
Description
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. Witnesses can be constructed for the
Type kind, Constraint kind, or any data kind.
Constructors
| 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.
Constructors
| 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 #