最近等价于Haskell中的Prolog原子或Lisp符号

Question

我试图编写一个简单的程序来操作命题微积分中的表达式，并希望为命题变量(例如'P或其他什么)提供一个很好的语法。

字符串完成了任务，但是语法在这种上下文中是误导的，并且允许像++这样的不适当的操作。

从语法上讲，我希望能够写下一些在视觉上不被引用的东西(不过，类似于'P的东西是可以的)。在支持的操作方面，我希望能够确定两个符号是否相等，并通过show将它们转换为与其名称匹配的字符串。我也希望这些东西是开放的(只有髓质构造函数的ADT在原则上类似于符号，但要求所有变体都提前声明)。

下面是一个使用字符串的玩具示例，其中一些符号更合适。

type Var = String

data Proposition =
    Primitive Var |
    Negated Proposition |
    Implication Proposition Proposition

instance Show Proposition where
    show (Primitive p) = p
    show (Negated n) = "!" ++ show n
    show (Implication ant cons) = 
        "(" ++ show ant ++ "->" ++ show cons ++ ")"

main = putStrLn $ show $ Implication (Primitive "A") (Primitive "B")

Answer 1

通常，在Haskell中这样做的方法是对符号类型进行参数化。所以你的榜样会变成：

data Proposition a = 
    Primitive a |
    Negated (Proposition a) |
    Implication (Proposition a) (Proposition a)

这就让用户来决定他们的符号的最佳表达方式。与LISP一样的符号相比，这具有优势:用于不同目的的符号不会混淆，涉及符号的数据结构现在允许对所有符号进行转换，这些转换比您所意识到的更有用。例如，Functor在符号表示和Monad模型替换之间的变化。

(=<<) :: (a        ->      Proposition b)      -> Proposition a -> Proposition b
          ^                ^^^^^^^^^^^^^          ^^^^^^^^^^^^^        
substitute each free var   with an expression   in this expression

你也可以获得一种类型安全的开放性：

implyOpen :: Proposition a -> Proposition b -> Proposition (Either a b)
implyOpen p q = Implication (Left <$> p) (Right <$> q)

另一个有趣的技巧是使用非常规递归类型以类型安全的方式建模变量绑定。

data Proposition a = 
    ... |
    ForAll (Proposition (Maybe a))

在这里，我们在内部命题中增加了一个“自由变量”-- Primitive Nothing是被量化的变量。一开始它可能看起来很尴尬，但是当你开始编写它的代码时，它是炸弹，因为它的类型使得它很难搞错。

定界是一个很好的包，可以根据这个想法(和其他一些技巧)来建模表达式语言。