用可变变量表示数据类型

Question

我试图用变量表示公式，例如，公式或变量和常量：

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

公式上的函数具有类约束，指定正在考虑哪种变量类型。例如，术语、变量和替换的类可能具有以下结构：

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 ...

有许多处理句法术语操作的算法，对于这些算法，在变量类型上参数化术语类型将是有益的。例如，考虑对具有不同变量类型的某些术语类型的公式的通用统一算法：

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

表示此类可变变量的最佳方法是什么？我尝试了多种方法，但尚未找到令人满意的解决方案。

Answer 1

如果您说以下简单的术语和公式表示有什么问题，也许您的问题会更清楚？有一百万种方法可以完成此类事情（{-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