haskell - 最接近于 Haskell 中的 Prolog atom 或 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)

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

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

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

bound是一个基于这个想法(和一些其他技巧)建模表达式语言的优秀包。