{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

{-|
Module      : Hout.Logic.FirstOrder
Description : Constructs of first-order intuitionistic logic in Haskell types
Copyright   : (c) Isaac van Bakel, 2020
License     : BSD-3
Maintainer  : ivb@vanbakel.io
Stability   : experimental
Portability : POSIX

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.
-}
module Hout.Logic.FirstOrder where

import Data.Kind

-- Types

-- | A witness of a kind inhabitant. 'Witness'es can be constructed for the
-- 'Type' kind, 'Constraint' kind, or any data kind.
data Witness (a :: k) where
  -- | Because Type is the only kind of habitats, it is the only constructor for
  -- which we can demand an inhabitant
  Witness :: (a :: Type) -> Witness a
  ConstraintWitness :: Witness (a :: Constraint)
  DataKindWitness :: Witness (a :: (k :: Type))

-- | 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'.
data Exists k (p :: k -> *) where
  Exists :: Witness (a :: k) -> p a -> Exists k p

-- | 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. 
data Forall k (p :: k -> *) = Forall (forall (a :: k). p a)

-- | Type level equality, parameterised by a kind.
data Equal (a :: k) (b :: k) where
  -- | The unique equality constructor - pattern matching on 'Refl' allows the
  -- compiler to deduce that @a@ and @b@ must unify.
  Refl :: Equal a a

-- Natural deduction (FO)

existsIntro :: Witness (a :: k) -> p a -> Exists k p
existsIntro witness proof = Exists witness proof

-- | 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
existsElim :: (forall (a :: k). Witness a -> p a -> b) -> Exists k p -> b
existsElim f (Exists witness proof) = f witness proof

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

forallElim :: Forall k p -> p (a :: k)
forallElim (Forall forall) = forall

eqRefl :: Equal a a
eqRefl = Refl

eqSym :: Equal a b -> Equal b a
eqSym Refl = Refl

eqTrans :: Equal a b -> Equal b c -> Equal a c
eqTrans Refl Refl = Refl

-- | Rewrite by equality.
--
-- This could be expressed as an @<->@, but @->@ is easier to use. The power
-- of the rule is not affected.
eqRewrite :: Equal a b -> p a -> p b
eqRewrite Refl proof = proof