haskell - Haskell中有诸如 "type extensions"之类的东西吗？

Question

我实际上并不认为术语“类型扩展”正式意味着我想要的，但这是我能想到的唯一术语。

我有一个多态 Haskell 类型来表示命题逻辑中的术语:

 data PropLogic a = Prop a | Tautology | Contradiction | And (PropLogic a) (PropLogic a)
                | Or (PropLogic a) (PropLogic a) | Implies (PropLogic a) (PropLogic a)
                | Not (PropLogic a)
     deriving (Eq,Show)

问题是，我也想要一个类似的带有量化运算符的命题逻辑多态类型:

data PropQuantifiedLogic a = Prop a | Tautology | Contradiction | And (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Or (PropQuantifiedLogic a) (PropQuantifiedLogic a) | Implies (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Not (PropQuantifiedLogic a) | Forall (PropQuantifiedLogic a)
                | Exists (PropQuantifiedLogic a)
     deriving (Eq,Show)

现在，我可以在每个值构造函数的名称中添加一个前缀，其中 PropLogic 和 PropQuantifiedLogic 都有冲突的名称，但重点是我想创建像这样的许多类型都会有很多相互冲突的值构造器:模态逻辑类型、时序逻辑类型等等......并且为每个类型创建新的前缀很快就会变得丑陋。

我真正想做的是:

extendtype PropQuantifiedLogic a = PropLogic a | Exists (PropQuantifiedLogic a)
                                 | Forall (PropQuantifiedLogic a)

这相当于 PropQuantifiedLogic 的第一个定义，并且会进行类型检查。

在 Haskell 中可以做这样的事情吗？如果不是，我该如何处理这种情况？这种“扩展类型”概念会带来一些歧义，但我相信这只是意味着在使用这样的类型时类型推断不起作用，我可以处理这个问题。

Answer 1

您始终可以将其实现为

 data PropFrame a b = OrF b b | AndF b b ... | Prop a | Top

然后

type Prop a = Fix (PropFrame a)

然后你可以添加一个新的原语

data QualifiedF a b = All (b -> b) | Exists (b -> b) | LiftProp (PropFrame a b)
type Qualified a = Fix (QualifiedF a)

这有点难看，但可以用 -XPatternSynonyms 来修饰。这里的主要思想是将有问题的递归情况分解为显式参数，并使用 Fix 重新获得递归。

使用示例

qand :: Qualified a -> Qualified a -> Qualified a
qand l r = Fix (LiftProp (AndF l r))

orOrAll :: (Qualified a -> Qualified a) -> Qualified a
orOrAll f = Fix (All f) `qand` Fix (Exists f)