如何将“ bound”用于非单子？

如何解决如何将“ bound”用于非单子？

我正在尝试使用bound package用一种简单的逻辑语言来表示术语和命题。这是我到目前为止的内容：

import Bound

data Term a = V a
            | Func String [Term a]
  deriving (Eq,Ord,Read,Show,Functor,Foldable,Traversable)

data Prop a = And (Prop a) (Prop a)
            | Relation String [Term a]
            | Forall (Scope () Prop a)
            deriving (Functor,Traversable)

特别是，有些术语要么是变量，要么是应用于某些术语的函数，还有一些命题是：两个命题的结合，应用于某些术语的关系以及对另一个命题中变量的量化。 但是，当我尝试创建一个函数来构造“ Forall”时，按照软件包文档中的示例，我被告知Prop不是monad：

forall' :: Eq a => a -> Prop a -> Prop a
forall' v b = Forall (abstract1 v b)

这是预料之中的，因为我没有定义Monad Prop。但是pure中没有明智的return（或Prop），那么如何使用bound包支持这种语言？

解决方法

我认为您只需要在此处合并Term和Prop：

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

如果我理解正确，那么Applicative想要的Monad / abstract1结构应该有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 ‘>>>=’.

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

• 在Prop中添加一个构造函数，以包装单个Term：

  data Prop a
    = And (Prop a) (Prop a)
    | Relation String [Term a]
    | Forall (Scope () Prop a)
    | Term (Term a)

• 使Exp等于Term或Prop，并为此实现Applicative和Monad：

  data Exp a
    = Term (Term a)
    | Prop (Prop a)
  

• 使Exp的GADT通过原子或通用命题编制索引：

  {-# LANGUAGE DataKinds,GADTs,KindSignatures #-}
  
  data Class = Atomic | Compound
  
  data Exp (c :: Class) a where
    V        :: a                  -> Term a
    Func     :: String -> [Term a] -> Term a
    And      :: Prop a -> Prop a   -> Prop a
    Relation :: String -> [Term a] -> Prop a
    Forall   :: Scope () Prop a    -> Prop a
  
  type Term a = Exp 'Atomic a
  type Prop a = Exp 'Compound a
  

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

  newtype Term a = Term (Exp a)
  newtype Prop a = Prop (Exp a)
  
  term :: Exp a -> Maybe (Term a)
  term t = case t of
    V{}    -> yes
    Func{} -> yes
    _      -> no
    where
      yes = Just (Term t)
      no  = Nothing
  
  prop :: Exp a -> Maybe (Prop a)
  prop t = case t of
    …
  

但是无论哪种方式，您都需要在其中V来表达“命题可以成为变量”或“表达式可以是命题或变量”。实际上，我认为您可以可以使用伪关系pure a = Relation "" [V a]原样表达您的类型，但其他形式之一可能更简洁。