如何对非单子使用`bound`？

Posted 2023-03-28

【中文标题】如何对非单子使用`bound`？

【英文标题】：How can I use `bound` for non-monads?

【发布时间】：2020-09-01 17:22:06

【问题描述】：

我正在尝试使用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, Foldable, Traversable)

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

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

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

【参考方案1】：

我认为您只需在此处合并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 ‘>>>=’.

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

将构造函数添加到 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

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

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]，但这些其他形式之一可能更干净。

【讨论】：

啊，是的，我可以看到使用按类型索引的 GADT 会起作用——不过我希望避免这种情况——似乎我做不到！

@B.Mehta：我编辑添加了一个基本示例。还不错，虽然我认为你不能直接创建Monad 实例，因为类型不会对齐；您可能需要将其包装在一个存在性隐藏该类型参数中，并在隐藏类型上分派，此时您不妨只使用 sum 类型。 （GADT 在您确实需要时非常有用，但在您并非绝对需要时通常有更简单的解决方案。）