Representing Data Types With Variable Variables

Question

I am attempting to represent formulae with variables ranging over, for instance, either formulae or variables and constants:

R(a,b) -> Q   [Q takes formulae as substitutions]
R(x,b) v P(b) [x takes constants or variables as substitutions]

Functions over formulae have class constraints specifying which variable type is being considered. For instance, classes of terms, variables and substitutions might have the following structure:

class Var b where ...
class (Var b) => Term b a | b -> a where ...
class (Term b a) => Subst s b a | b a -> s where ...

There are many algorithms dealing with syntactic term manipulation for which parameterizing term types on variable types would be beneficial. For instance, consider a generic unification algorithm over formulae of some term type having different variable types:

unify :: (Subst s b a) => a -> a -> s b a
unify (P -> F(a,b)) ((Q v R) -> F(a,b)) = {P\(Q v R)}  -- formulae
unify (P(x,f(a,b))) (P(g(c),f(y,b)))    = {x\g(c),y\a} -- variables and constants

What is the best way to represent such variable variables? I have experimented with a variety of methods, but haven't settled on a satisfactory solution.

Answer 1

Maybe your question would be clearer if you said what was wrong with the following simple minded representation of terms and formulas? There are a million ways of doing this sort of thing (the possibilities much expanded by {-LANGUAGE GADTs-})

  {-#LANGUAGE TypeOperators#-}

  data Term v c = Var v 
                | Const c deriving (Show, Eq, Ord)

  data Formula p v c = Atom p 
                     | Term v c := Term v c 
                     | Formula p v c :-> Formula p v c 
                     | Not (Formula p v c)
                     | Subst v (Term v c) (Formula p v c) 
                     | Inst p (Formula p v c) (Formula p v c) 
                     deriving (Show, Eq, Ord)


  update f v c v' = case v == v' of True -> c; False -> f v'

  one = Const (1:: Int)
  zero = Const (0 :: Int)
  x = Var 'x'
  y = Var 'y'
  p = Atom 'p'
  q = Atom 'q'
  absurd = one := zero
  brouwer p = (((p :-> absurd) :-> absurd) :-> absurd) :-> (p :-> absurd)

  ref ::  (v -> c) -> Term v c -> c
  ref i (Var v)  = i v
  ref i (Const c) = c

  eval :: (Eq c , Eq v , Eq p) => (v -> c) -> (p -> Bool) -> Formula p v c -> Bool
  eval i j (Atom p) = j p
  eval i j (p := q) = ref i p == ref i q
  eval i j (p :-> q) = not ( eval i j p) ||  eval i j q
  eval i j (Not p) = not (eval i j p)
  eval i j q@(Subst v t p) =  eval (update i v (ref i t)) j q
  eval i j q@(Inst p r s) = eval i (update j p (eval i j r)) s