haskell - 我应该如何在 haskell 中表达具有约束的相互递归数据类型？

Question

我自己也不是很清楚，所以如果我的描述也不够清楚，请告诉我。

所以，我有两个类:

class Prop1 a b | a -> b
class Prop2 c d | c -> d

和数据类型:

data X y z

它们之间的关系是:

1. X是z的容器，y是辅助容器。
2. 容器 y 应包含另一组实例 X y z。

3. y 满足 Prop1，即以下成立:

   实例 Prop1 y (X y z)

4. X 本身满足 Prop2，因此:

   实例 Prop2 (X y z) z

所以当我定义X的实例时，我觉得自己一团糟，我写了这样的话:

instance Prop1 y (X y z) => Prop2 (X y z) z

但 GHC 似乎对此并不满意，并要求我添加 FlexibleContexts 和 UndecidableInstances，这让我感到不安全。

我读到对 data 施加约束是不好的，但我试过了但没有帮助:

data Prop1 y (X y z) => X y z

在Haskell中应该如何处理？

Answer 1

UndecidableInstances 可以安全使用，它只是意味着编译器不知道它将能够终止类型检查/解析约束。 UndecidableInstances 的最坏可能结果是编译器无法终止。我们可以看到编译器通过完成示例程序而终止。

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

class Prop1 a b | a -> b
class Prop2 c d | c -> d

data X y z = X

instance Prop1 y (X y z) => Prop2 (X y z) z

-- An example Y and checking Prop2
data Y = Y

instance Prop1 Y (X Y ())

main :: Prop2 (X Y ()) () => IO ()
main = print "checked"

我们必须为 Prop1 Y x 实例的 z 选择一个具体类型； y 本质上是确定 z。我为 Y 选择了 ()；可能有另一个 Y' 具有不同的 z。

类型族

如果您不想使用 UndecidableInstances，您可以使用 TypeFamilies 而不是 FunctionalDependencies。

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

class Prop1 a where
    type B a :: *

class Prop2 c where
    type D c :: *

data X y z = X

instance (Prop1 y, B y ~ (X y z)) => Prop2 (X y z) where
    type D (X y z) = z

-- An example Y and get the compiler to run all the way to requiring FlexibleContexts 
data Y = Y

instance Prop1 Y where
    type B Y = X Y ()

main :: Prop2 (X Y ()) => IO ()
main = print "checked"