cps :: Classical logic -> Intuitionistic logic

C.hs

{-# LANGUAGE
    BlockArguments,
    EmptyCase,
    GADTs,
    TypeOperators #-}

module C where

{- 1. Classical logic -}

{- Syntax of propositions
   a, b ::=
     | F         -- false
     | a :*: b   -- conjunction
     | a :+: b   -- disjunction
     | Not a     -- negation
     | a :->: b  -- implication
-}

-- Syntax of proofs
-- x :: K a  is a classical proof of the proposition a.
data K a where
  AndI :: K a -> K b -> K (a :*: b)
  OrIL :: K a -> K (a :+: b)
  OrIR :: K b -> K (a :+: b)
  ImplI :: (a -> K b) -> K (a :->: b)
  Assumption :: a -> K a
  Cut :: K (a :->: b) -> K a -> K b
  NotNot :: K (Not (Not a)) -> K a

{- 2. Interpretation in intuitionistic logic (embedded in Haskell). -}

-- Interpret propositions of classical logic
-- as propositions of intuitionistic logic (embedded as Haskell types)
data F
type a :*: b = (a, b)
type a :+: b = Either a b
type Not a = a -> F
type a :->: b = a -> Not (Not b)

-- Note on F: this translation doesn't use the fact that F is empty (so it could
-- technically be anything).

-- Note on (:->:): this translation inserts a double negation on the conlusion of (:->:).
-- The interpret function is technically definable without it, but in an ugly way.

-- Interpret classical proofs as intuitionistic proofs (embedded as Haskell terms)
interpret :: K a -> Not (Not a)
interpret (NotNot p) k =
  interpret p \f ->
  f k
interpret (Cut pf px) k =
  interpret pf \f ->
  interpret px \x ->
  f x k
interpret (AndI pa pb) k =
  interpret pa \a ->
  interpret pb \b ->
  k (a, b)
interpret (OrIL pa) k =
  interpret pa \a ->
  k (Left a)
interpret (OrIR pb) k =
  interpret pb \b ->
  k (Right b)
interpret (ImplI fp) k =
  k \a kb ->
  interpret (fp a) kb
interpret (Assumption a) k = k a