First-Order Logic formulated using TypeInTypes of GHC 8.0.1

Logic.hs

{-# LANGUAGE DataKinds, ExistentialQuantification, FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances, GADTs, IncoherentInstances, InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses, PolyKinds, RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell    #-}
{-# LANGUAGE TypeApplications, TypeFamilies, TypeInType, TypeOperators   #-}
{-# LANGUAGE UndecidableInstances, UnicodeSyntax                         #-}
module Main where
import GHC.TypeLits
import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude.List
import Data.Constraint.Forall
import qualified Data.Constraint as C

import Lib

main :: IO ()
main = someFunc

class Language lang where
  data Function lang (arity :: Peano)
  data Predicate lang (arity :: Peano)

data Peano = Z | S Peano deriving (Read, Show, Eq, Ord)

data instance Sing (v :: Vec a n) where
  SVNil  :: Sing 'VNil
  (::<|) :: Sing a -> Sing as -> Sing (a ':<| as)

type SVec (v :: Vec a n) = Sing v

data Vec a n where
  VNil  :: Vec a 'Z
  (:<|) :: a -> Vec a n -> Vec a ('S n)
deriving instance Show a => Show (Vec a n)

-- We cannot use builtin @'GHC.TypeLits.Nat'@s,
-- because the lack of their "constructor"
-- prevents the following "flatting" function
-- from compiling.
type family Flat (vs :: Vec [a] n) :: [a] where
  Flat 'VNil = '[] 
  Flat (v ':<| vs) = Union v (Flat vs)

data MapVec (f :: a -> Type) (as :: Vec a n) where
  Empty  :: MapVec f 'VNil
  MVCons :: f x -> MapVec f as -> MapVec f (x ':<| as)

infixr 9 :<|, ::<|

data Expr lang (vs :: [Symbol]) where
  Apply :: Function lang n -> MapVec (Expr lang) (vs :: Vec [Symbol] n) -> Expr lang (Flat vs)
  Var   :: SSymbol v -> Expr lang '[v]

instance ForallF Show (Function lang) => Show (Expr lang vs) where
  showsPrec _ (Var v) = withKnownSymbol  v $ showString (symbolVal v)
  showsPrec d (Apply v Empty) =
    showsPrec d v C.\\ (instF @Show @(Function lang) @'Z)
  showsPrec d (Apply v (vs :: MapVec (Expr lang) (as :: Vec [Symbol] m))) =
    (showsPrec d v C.\\ (instF @Show @(Function lang) @m))
    . showChar '(' . foldr1 (\a b -> a . showString ", " . b) (showArgs vs) . showChar ')'

showArgs :: forall f vs. ForallF Show f => MapVec f vs -> [ShowS]
showArgs Empty = []
showArgs (MVCons (fx :: f x) rest) =
  shows fx : showArgs rest C.\\ (instF  @Show @f @x)

type Constant lang = Function lang 'Z

(>-) :: f x -> MapVec f as -> MapVec f (x ':<| as)
(>-) = MVCons

mkConst :: Constant lang -> Expr lang '[]
mkConst f = Apply f Empty

(<@>) :: Function lang n -> MapVec (Expr lang) vs -> Expr lang (Flat (vs :: Vec [Symbol] n))
(<@>) = Apply
infixr 9 >-
infixl 4 <@>

(<?>) :: Predicate lang n -> MapVec (Expr lang) vs -> Formula lang (Flat (vs :: Vec [Symbol] n))
(<?>) = AtomicF
infixl 7 <?>

data Formula lang (vs ∷ [Symbol]) where
  AtomicF :: Predicate lang n -> MapVec (Expr lang) (vs :: Vec [Symbol] n) -> Formula lang (Flat vs)
  (:==:) ∷ Expr lang vs -> Expr lang us -> Formula lang (Union vs us)
  (:/\:) ∷ Formula lang  vs -> Formula lang  us -> Formula lang  (Union vs us)
  (:\/:) ∷ Formula lang  vs -> Formula lang  us -> Formula lang  (Union vs us)
  Neg    ∷ Formula lang  vs -> Formula lang  vs
  (:=>:) ∷ Formula lang  vs -> Formula lang  us -> Formula lang  (Union vs us)
  Forall ∷ Sing v -> Formula lang  vs -> Formula lang  (Delete v vs)
  Exists ∷ Sing v -> Formula lang  vs -> Formula lang  (Delete v vs)

infixr 8  :==:
infixr 3  :/\:
infixr 2  :\/:
infixr 1  :=>:

instShowF :: forall f a. ForallF Show f C.:- Show (f a)
instShowF = instF

instance (ForallF Show (Expr lang), ForallF Show (Predicate lang)) => Show (Formula lang vs) where
  showsPrec _ ((a :: Expr lang us) :==: (b :: Expr lang ts)) =
      (showsPrec 10 a C.\\ instShowF @(Expr lang) @us)
    . showString " = "
    . (showsPrec 10 b C.\\ instShowF @(Expr lang) @ts)
  showsPrec d ((a :: Formula lang us) :\/: (b :: Formula lang ts)) = showParen (d > 2) $
      (showsPrec 2 a C.\\ instShowF @(Formula lang) @us)
    . showString " \\/ "
    . (showsPrec 2 b C.\\ instShowF @(Formula lang) @ts)
  showsPrec d ((a :: Formula lang us) :/\: (b :: Formula lang ts)) = showParen (d > 3) $
      (showsPrec 3 a C.\\ instShowF @(Formula lang) @us)
    . showString " /\\ "
    . (showsPrec 3 b C.\\ instShowF @(Formula lang) @ts)
  showsPrec d ((a :: Formula lang us) :=>: (b :: Formula lang ts)) = showParen (d > 1) $
      (showsPrec 3 a C.\\ instShowF @(Formula lang) @us)
    . showString " => "
    . (showsPrec 3 b C.\\ instShowF @(Formula lang) @ts)
  showsPrec d (Neg (a :: Formula lang us)) = showParen (d > 4) $
    showString "~ "
    . (showsPrec 4 a C.\\ instShowF @(Formula lang) @us)
  showsPrec d (Forall v (a :: Formula lang us)) = showParen (d > 5) $
    showString "∀ " . showString (withKnownSymbol v $ symbolVal v) .
    showString ". "
    . (showsPrec 5 a C.\\ instShowF @(Formula lang) @us)
  showsPrec d (Exists v (a :: Formula lang us)) = showParen (d > 5) $
    showString "∃ " . showString (withKnownSymbol v $ symbolVal v) .
    showString ". "
    . (showsPrec 5 a C.\\ instShowF @(Formula lang) @us)
  showsPrec d (AtomicF v (vs :: MapVec (Expr lang) (as :: Vec [Symbol] m))) =
    showParen (d > 9) $
    (showsPrec d v C.\\ (instShowF @(Predicate lang) @m))
    . showChar '(' . foldr1 (\a b -> a . showString ", " . b) (showArgs vs) . showChar ')'


type Sentence = Formula []

data ZF
data PA

instance Language ZF where
  data Function ZF n
  data Predicate ZF n where
    (:<-:) :: Predicate ZF ('S ('S 'Z))

deriving instance Show (Function ZF n)
deriving instance Show (Predicate ZF n)

instance Language PA where
  data Function PA n where
    Plus :: Function PA ('S ('S 'Z))
    Mult :: Function PA ('S ('S 'Z))
    Succ  :: Function PA ('S 'Z)
    Zero  :: Function PA 'Z
  data Predicate PA n where
    Leq :: Predicate PA ('S ('S 'Z))

deriving instance Show (Function PA n)
deriving instance Show (Predicate PA n)

x = sing :: Sing "x"
y = sing :: Sing "y"