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

编程问答 2022-08-13

问题描述

我正在尝试使用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]原样表达您的类型，但其他形式之一可能更简洁。

dslhaskellhaskelllogicmonadspackagepackagepackage