Representation of data types with variable variables

Question

I am trying to imagine formulas with the variables above, for example, either formulas 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 formulas have class restrictions that determine what type of variable is considered. For example, classes of terms, variables, and permutations can have the following structure:

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

There are many algorithms associated with syntactic terms for which it would be useful to use types of parameter types for variable types. For example, consider a general unification algorithm over formulas of a certain type of terms having different types of variables:

 unify :: (Subst sba) => a -> a -> sba 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 experimented with various methods, but did not find a satisfactory solution.

Answer 1

Perhaps your question will be clearer if you say what was wrong with the following simple mental presentation of terms and formulas? There are a million ways to do these things (capabilities greatly expanded by {-LANGUAGE GADTs-} )

  {-#LANGUAGE TypeOperators#-} data Term vc = Var v | Const c deriving (Show, Eq, Ord) data Formula pvc = Atom p | Term vc := Term vc | Formula pvc :-> Formula pvc | Not (Formula pvc) | Subst v (Term vc) (Formula pvc) | Inst p (Formula pvc) (Formula pvc) deriving (Show, Eq, Ord) update fvcv' = case v == v' of True -> c; False -> fv' 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 vc -> c ref i (Var v) = iv ref i (Const c) = c eval :: (Eq c , Eq v , Eq p) => (v -> c) -> (p -> Bool) -> Formula pvc -> Bool eval ij (Atom p) = jp eval ij (p := q) = ref ip == ref iq eval ij (p :-> q) = not ( eval ijp) || eval ijq eval ij (Not p) = not (eval ijp) eval ij q@ (Subst vtp) = eval (update iv (ref it)) jq eval ij q@ (Inst prs) = eval i (update jp (eval ijr)) s