Haskell类型类的基础和"could not deduce (~) from the context (~)"错误

Question

我对Haskell还比较陌生，我相信我误解了类型类的一些基本知识。假设我想创建一个类型类"T"，实现由四个代数类型"a、B、C和d"支持的n元树，它们的结构要求最大深度为四。这似乎是一个愚蠢的例子，但我认为它最能说明我的观点。

module Test where
class T t0 where
parent :: T t1 => t0 -> Maybe t1
children :: T t1 => t0 -> [t1]
data A = A [B]
instance T A where
parent (A _) = Nothing
children (A bs) = bs
data B = B A [C]
instance T B where
parent (B a _) = Just a
children (B _ cs) = cs
data C = C B [D]
instance T C where
parent (C b _) = Just b
children (C _ ds) = ds
data D = D C
instance T D where
parent (D c) = Just c
children (D _) = []

我想编写通用的父函数和子函数，但GHC没有

Test.hs:10:27:
Could not deduce (t1 ~ B)
from the context (T t1)
bound by the type signature for children :: T t1 => A -> [t1]
at Test.hs:10:9-28
`t1' is a rigid type variable bound by
the type signature for children :: T t1 => A -> [t1]
at Test.hs:10:9
Expected type: [t1]
Actual type: [B]
In the expression: bs
In an equation for `children': children (A bs) = bs
In the instance declaration for `T A'
Test.hs:14:31:
Could not deduce (t1 ~ A)
from the context (T t1)
bound by the type signature for parent :: T t1 => B -> Maybe t1
at Test.hs:14:9-31
`t1' is a rigid type variable bound by
the type signature for parent :: T t1 => B -> Maybe t1
at Test.hs:14:9
In the first argument of `Just', namely `a'
In the expression: Just a
In an equation for `parent': parent (B a _) = Just a
Test.hs:15:29:
Could not deduce (t1 ~ C)
from the context (T t1)
bound by the type signature for children :: T t1 => B -> [t1]
at Test.hs:15:9-30
`t1' is a rigid type variable bound by
the type signature for children :: T t1 => B -> [t1]
at Test.hs:15:9
Expected type: [t1]
Actual type: [C]
In the expression: cs
In an equation for `children': children (B _ cs) = cs
In the instance declaration for `T B'
Test.hs:19:31:
Could not deduce (t1 ~ B)
from the context (T t1)
bound by the type signature for parent :: T t1 => C -> Maybe t1
at Test.hs:19:9-31
`t1' is a rigid type variable bound by
the type signature for parent :: T t1 => C -> Maybe t1
at Test.hs:19:9
In the first argument of `Just', namely `b'
In the expression: Just b
In an equation for `parent': parent (C b _) = Just bv

我(认为我)理解类型类根本不像Java接口，因为类级函数必须为所提供的类型变量的任何可能值工作；调用者没有"决定"类型。我不明白为什么GHC不能推导(t1~_)，因为t1的类型总是"t"的一个实例。我看到实例声明之间存在某种循环依赖关系，例如，a的实例声明取决于B的有效性，这取决于a和C的有效性等等，但我觉得GHC足够聪明，能够解决这个问题，我只是缺少了一些东西。每当我希望类型类中的函数接受该类中的一个类型但返回另一个类型时，我似乎总是会遇到这个错误。。。有没有一种方法可以用类型类来实现这一点？

我看到这里有很多措辞相似的问题，但我还没有找到一个与我的问题相匹配的问题(据我所知)。

提前谢谢。

Answer 1

您已经正确理解了这个问题：这些签名实际上意味着

parent :: forall t1 . T t1 => t0 -> Maybe t1

而不是在协变OO语言中

parent :: exists t1 . T t1 => t0 -> Maybe t1

这类东西的两种常见解决方案是使用类似的语法扩展

• TypeFamilies

  class T t0 where
  type Child t0 :: *
  parent :: Child t0 -> Maybe t0
  children :: t0 -> [Child t 0]
  instance T A where
  type Child A = B
  parent (A _) = Nothing
  ...
  

• 或MultiparamTypeClasses

  class T child t0 where
  parent :: child -> Maybe t0
  children :: t0 -> [child]
  instance T A B where
  ...
  

请注意，在这两种情况下，D都不会有实例。

至于这些扩展中哪一个"更好"，你真的无法回答。MultiparamTypeClasses本身往往过于"弱"，因为您需要手动修复所有涉及的类型，但可以通过添加FunctionalDependency来解决。在class T child t0 | t0 -> child的特殊情况下，这在很大程度上等同于TypeFamilies的解。但在您的情况下，class T child t0 | t0 -> child, child -> t0也是可能的。

有关详细信息，请考虑Haskell Wiki。

Answer 2

这确实不是你特定问题的答案，但它是你问题的解决方案：创建一个k元树结构，其最大深度受其类型的限制。如果您不关心使用大量GHC扩展，那么此解决方案非常简单且可扩展。

我不想谈太多细节——某些扩展的确切工作规则非常复杂，如果你想要详细的细节，你应该阅读文档。

{-# LANGUAGE 
MultiParamTypeClasses
, DataKinds
, GADTs
, FunctionalDependencies
, KindSignatures
, FlexibleInstances
, UndecidableInstances
, PolyKinds
, TypeOperators
, FlexibleContexts
, TypeFamilies
#-} 
-- Not all of these are needed; most are used to make the code cleaner
data Nat = Z | P Nat

Nat类型用于在类型级别上对深度进行编码。使用-XDataKinds，GHC可以采用类似Nat的简单数据类型并"提升"它；也就是说，数据构造函数变为类型，类型Nat变为"种类"(类型的类型)。CCD_ 13==零；P==加一。

type family LTEQ (a :: Nat) (b :: Nat) :: Bool
type instance LTEQ Z Z = True
type instance LTEQ Z (P x) = True
type instance LTEQ (P x) Z = False
type instance LTEQ (P a) (P b) = LTEQ a b

接下来我们在CCD_ 15上定义了一个偏序。注意显式类型签名(即a :: Nat)-PolyKinds不需要这些签名，但可以更清楚地了解发生了什么。如果这看起来很困惑，可以将其视为一组规则：

0 <= 0 == True
0 <= (1 + x) == True
(1 + x) <= 0 == False
(1 + x) <= (1 + y) == x <= y

如果你想向自己证明这是有效的：

-- This would only be used for testing
data Pr p = Pr
lteq :: f ~ (a `LTEQ` b) => Pr a -> Pr b -> Pr f
lteq _ _ = Pr
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr Z)
lteq (Pr :: Pr (P Z)) (Pr :: Pr Z) :: Pr Bool 'False
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr (P Z))
lteq (Pr :: Pr (P Z)) (Pr :: Pr (P Z)) :: Pr Bool 'True
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr (P (P Z)))
lteq (Pr :: Pr (P Z)) (Pr :: Pr (P (P Z))) :: Pr Bool 'True
>:t lteq (Pr :: Pr Z) (Pr :: Pr (P (P Z)))
lteq (Pr :: Pr Z) (Pr :: Pr (P (P Z))) :: Pr Bool 'True
>:t lteq (Pr :: Pr Z) (Pr :: Pr Z)
lteq (Pr :: Pr Z) (Pr :: Pr Z) :: Pr Bool 'True

我们必须使用Pr而不是仅使用a -> b -> (LTEQ a b)，因为a和b是提升类型(特别是Nat类型)，而(->)只采用未提升类型。如果这没有意义，不要太担心，因为这其实并不重要。只要说这里需要它就足够了。

定义最大深度是什么，非常非常简单：

type MAXDEPTH = P (P (P (P Z)))

请注意，更改最大深度是多么简单。现在是Tree数据类型。它使用GADT(广义代数数据类型)语法；基本上，所有这些意味着我们可以更好地控制如何创建Tree类型的东西。d类型变量是深度，a是存储在树中的元素。

data Tree d a where
D0    :: a -> Tree Z a     
DPlus :: ((P d) `LTEQ` MAXDEPTH) ~ True => a -> [Tree d a] -> Tree (P d) a 

让我们按构造函数将其分解。第一个是D0，它取一个类型为a的值，并创建一个深度为零的树，只存储该值：只有一个没有子节点的节点。

CCD_ 30获取一个节点和子树列表。添加一个节点显然会将深度增加一个——您可以看到结果类型反映了这一点。然后，为了强制执行最大深度4，我们只说d + 1 <= MAXDEPTH。

因为0深度树非常无聊，您可能需要深度1:的辅助函数

depth1 a xs = DPlus a (map D0 xs)

然后是一个有趣的例子：

instance Show a => Show (Tree d a) where
show (D0 a)     = "D0 " ++ show a
show (DPlus a xs) = "DPlus " ++ show a ++ " " ++ show xs

还有一个快速测试：

>depth1 'c' "hello"
DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']
>DPlus 'a' [depth1 'c' "hello"]
DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]
>DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]
DPlus 'b' [DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]]
>DPlus 'c' [DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]]
DPlus 'c' [DPlus 'b' [DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]]]
>DPlus 'd' [DPlus 'c' [DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]]]
<interactive>:130:1:
Couldn't match type 'False with 'True
Expected type: 'True ...

正如您所看到的，试图构建深度大于4的树将导致类型错误。

简要说明：您的示例代码适用于允许您引用备份其结构的树。由于我回答的主要目的是演示使用DataKinds在类型级别上强制树深度，所以我只实现了一个非常简单的树。您有正确的想法来引用"向上"树，但由于现在所有内容都是单一类型，您可能甚至不需要类型类！