问非monad如何使用` `bound` `？

EN

我认为你只需要在这里合并Term和Prop：

data Exp a
  = V a
  | Func String [Exp a]
  | And (Exp a) (Exp a)
  | Relation String [Exp a]
  | Forall (Scope () Prop a)

如果我没理解错的话，abstract1想要的Applicative/Monad结构应该是让pure注入一个变量，然后由>>=进行替换。这样，您的Applicative和Monad实例就可以直接遵循文档：

instance Applicative Exp where
  pure = V
  (<*>) = ap

instance Monad Exp where
  return = V
  V a           >>= f = f a
  And x y       >>= f = And (x >>= f) (y >>= f)
  Relation r xs >>= f = Relation r (fmap (>>= f) xs)  -- (I think.)
  Forall e      >>= f = Forall (e >>>= f)             -- NB: bound’s ‘>>>=’.

您可以根据您的用例以不同的方式重新安排：

• 向包装单个Term的Prop添加构造函数：

数据属性a= And (属性a) (属性a) |关系字符串项a|全部(作用域()属性a) |项(术语a)

• 使Exp成为Term或Prop的总和，并为此实现Applicative和Monad：

数据扩展a= Term (Term a) | Prop (Prop a)

• 使Exp成为一个GADT，通过它是一个原子术语还是一个通用命题来索引：

{-# LANGUAGE DataKinds，GADTs，KindSignatures #-}数据类=原子|复合数据Exp (c :：Class) a其中V :：a ->术语函数:：String ->术语->术语a和:：支持->属性->属性a关系:：String ->术语->属性Forall :：Scope ()支持->属性类型术语a= Exp‘原子类型属性a= Exp’复合

• 使用智能构造函数为Exp的“子类型”制作newtype包装器，如果您只需要区分它们的话：

新类型术语a=术语(Exp a)新类型prop a=属性(Exp a)术语:：Exp a ->可能(术语a)术语t=案例t of V{} -> yes Func{} -> yes _ -> no where yes = Just (术语t) no = Nothing属性:：Exp a ->可能(属性a)属性t=案例t of…

但是无论哪种方式，你都需要V来表达“命题可以是变量”或者“表达式可以是命题也可以是变量”。事实上，我认为你实际上可以用你的类型原样来表达，使用一个虚拟的关系：pure a = Relation "" [V a]，但是这些其他形式中的一种可能更简洁。