An encoding of N-th order logic in Haskell, where the minimal order is encoded by the term... This all fails pretty horribly (in the sense that it doesn't really achieve what I set out to do, and actually trying to write formulas using this is incredibly painful), but I thought it'd be nice to keep around.

Logic.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings, FlexibleInstances #-}
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies #-}
module Logic where

import Text.Printf (printf)
import Data.String.Utils (join)

-- | encoding of natural numbers for use with datakinds
data Nat where
  Nz :: Nat
  Ns :: Nat -> Nat

-- | computes the maximum of two natural numbers
type family Max (m :: Nat) (n :: Nat) :: Nat
type instance Max  m      Nz    = m
type instance Max  Nz     n     = n
type instance Max (Ns m) (Ns n) = Ns (Max m n)

-- | increases order if order is not zero, due to the
--   odd position of terms in this hierarchy
type family Nx (n :: Nat) :: Nat
type instance Nx  Nz    = Nz
type instance Nx (Ns n) = Ns (Ns n)


-- * datatype declarations

type Name (n :: Nat) = String

type Term = Logic Nz

type L0   = Logic (Ns Nz)
type L1   = Logic (Ns (Ns Nz))
type L2   = Logic (Ns (Ns (Ns Nz)))

type HOL  = forall n. Logic (Ns (Ns (Ns n)))

data Logic (n :: Nat) where
  Var    :: Name Nz -> Logic Nz
  Con    :: Name Nz -> Logic Nz
  Fun    :: Name Nz -> [Logic Nz] -> Logic Nz

  Pred   :: Name m -> [Logic n] -> Logic (Max m (Nx n))
  Exists :: Name m ->  Logic n  -> Logic (Max (Ns m) n)
  Forall :: Name m ->  Logic n  -> Logic (Max (Ns m) n)

  Top    :: Logic m
  Bot    :: Logic m
  Neg    :: Logic m -> Logic n
  Conj   :: Logic m -> Logic n -> Logic (Max m n)
  Disj   :: Logic m -> Logic n -> Logic (Max m n)
  Impl   :: Logic m -> Logic n -> Logic (Max m n)
  Equiv  :: Logic m -> Logic n -> Logic (Max m n)


-- * instance declarations

instance Show (Logic n) where
  show (Var x)       = x
  show (Con x)       = x
  show (Fun n xs)    = printf "%s(%s)" n (join ", " . map show $ xs)

  show (Pred n xs)   = printf "%s(%s)" n (join ", " . map show $ xs)
  show (Exists n xs) = printf "?%s.%s" n (show xs)
  show (Forall n xs) = printf "!%s.%s" n (show xs)

  show  Top          = "0"
  show  Bot          = "1"
  show (Neg x)       = printf "~(%s)" (show x)
  show (Conj x y)    = printf "%s /\\ %s" (show x) (show y)
  show (Disj x y)    = printf "%s \\/ %s" (show x) (show y)
  show (Impl x y)    = printf "%s => %s" (show x) (show y)
  show (Equiv x y)   = printf "%s == %s" (show x) (show y)