hout- Non-interactive proof assistant monad for first-order logic.

Copyright(c) Isaac van Bakel 2020
Safe HaskellSafe



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.



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.


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 Exists k (p :: k -> *) where Source #

The existential quantifier, parameterised by a kind. The predicate itself is required to return a Type, since Exists carries the proof term. If k is Type, then Exists also carries the witness term in a Witness.


Exists :: Witness (a :: k) -> p a -> Exists k p 

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) 

data Equal (a :: k) (b :: k) where Source #

Type level equality, parameterised by a kind.


Refl :: Equal a a

The unique equality constructor - pattern matching on Refl allows the compiler to deduce that a and b must unify.

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 #

eqSym :: Equal a b -> Equal b a Source #

eqTrans :: Equal a b -> Equal b c -> Equal a c Source #

eqRewrite :: Equal a b -> p a -> p b Source #

Rewrite by equality.

This could be expressed as an -, but -> is easier to use. The power of the rule is not affected.