在Haskell中通过多态实现递归代数数据类型

Question

在Haskell中通过多态实现递归代数数据类型

haskellalgebraic-data-typesparametric-polymorphism

3

我正在尝试理解递归代数数据类型的定义、编码和解码，以及通用多态功能。例如，我尝试通过以下方式实现二叉树的递归类型：

data BTAlg x = Empty | Leaf x x
type BT = forall z. ((BTAlg z) -> z) -> z

直觉上来说，所有具有常量e:T和二元操作m:T->T->T的类型T中，二叉树类型应该是最初的，也就是作为函子BTAlg的“初始模型”。换言之，BT的一个元素是一种为任何这样的模型T分配T元素的方式。

可以通过对BT本身进行模块结构定义来实现。

initial_module :: (BTAlg BT) -> BT
initial_module = \s -> case s of
  Empty -> (\f -> (f Empty))
  Leaf x y -> (\f -> (f (Leaf (x f) (y f))))

作为实现BT模式匹配的一步，我现在想将一个元素x:BT应用于类型BT本身，我认为这是对x进行编码和解码的某种方式。

decode_encode :: BT -> BT
decode_encode x = x initial_module

然而，这段代码导致了一种我无法处理的类型错误：

Couldn't match expected type `(BTAlg z -> z) -> z'
            with actual type `BT'
Expected type: BTAlg ((BTAlg z -> z) -> z) -> (BTAlg z -> z) -> z
  Actual type: BTAlg BT -> (BTAlg z0 -> z0) -> z0
In the first argument of `x', namely `initial_module'
In the expression: x initial_module

这里有什么问题？我不知道为什么类型检查器无法识别通用类型参数 z 必须在 x 中特化为 BT，才能将 x 应用于 initial_module；写成 (x :: ((BTAlg BT) -> BT) -> BT) initial_module 也没有帮助。

补充说明关于定义 decode_encode 的动机: 我想说服自己，BT 实际上与标准实现“同构”。

data BTStd = StdEmpty | StdLeaf BTStd BTStd

关于二叉树的实现；虽然我不知道如何在Haskell中准确地实现，但一个好的起点是构建映射BT -> BTStd和BTStd -> BT，这样可以在两个实现之间来回转换。

toStandard: BT -> BTStd的定义是将BT的通用属性应用于BTStd上的规范BTAlg模块结构：

std_module :: (BTAlg BTStd) -> BTStd
std_module s = case s of 
  Empty -> StdEmpty
  Leaf x y -> StdLeaf x y

toStandard: BT -> BTStd
toStandard x = x std_module

对于解码函数fromStandard: BTStd -> BT，我想要做以下操作：

fromStandard :: BTStd -> BT
fromStandard s = case s of 
  StdEmpty -> initial_module Empty
  StdLeaf x y -> initial_module (Leaf (fromStandard x) (fromStandard y))

然而，这会带来与上面直接定义decode_encode相同的打字问题：

Couldn't match expected type `BT'
            with actual type `(BTAlg z0 -> z0) -> z0'
In the return type of a call of `fromStandard'
Probable cause: `fromStandard' is applied to too few arguments
In the first argument of `Leaf', namely `(fromStandard x)'
In the first argument of `initial_module', namely
  `(Leaf (fromStandard x) (fromStandard y))'

谢谢你！

- Hanno

我认为你的转换没有保留 z 类型（看起来是 实际类型: BTAlg BT -> (BTAlg z0 -> z0) -> z0），但是应该要保留（看起来是 期望类型: BTAlg ((BTAlg z -> z) -> z) -> (BTAlg z -> z) -> z）。我认为你的映射没有很好地定义（你想做什么？） - josejuan

@josejuan：感谢您的评论！我在问题中添加了一些关于“decode_encode”定义的动机。您能否说一下具体哪些地方没有很好地定义？ - Hanno

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- J. Abrahamson · Accepted Answer

如果您查看decode_encode的推断类型。

:t decode_encode
> decode_encode :: ((BTAlg BT -> (BTAlg z -> z) -> z) -> t) -> t

很明显，GHC失去了相当多的多态性。我不完全确定细节——这段代码需要使用ImpredicativeTypes才能编译，这通常是我理解开始崩溃的地方。但是，有一种保留多态性的标准方法：使用newtype。

newtype BT = BT { runBT :: forall z. (BTAlg z -> z) -> z }

newtype建立了一个同构BT ~ forall z . (BTAlg z -> z) -> z，由BT和runBT证明。只要我们将这些证明放在正确的位置，我们就可以继续前进。

data    BTAlg x = Empty    | Leaf    x     x
data    BTStd   = StdEmpty | StdLeaf BTStd BTStd
newtype BT      = BT { runBT :: forall z. ((BTAlg z) -> z) -> z }

initial_module :: BTAlg BT -> BT
initial_module s = case s of
  Empty -> BT $ \f -> (f Empty)
  Leaf x y -> BT $ \f -> (f (Leaf (runBT x f) (runBT y f)))

std_module :: (BTAlg BTStd) -> BTStd
std_module s = case s of 
  Empty -> StdEmpty
  Leaf x y -> StdLeaf x y

toStandard :: BT -> BTStd
toStandard x = runBT x std_module

fromStandard :: BTStd -> BT
fromStandard s = case s of
  StdEmpty -> initial_module Empty
  StdLeaf x y -> initial_module (Leaf (fromStandard x) (fromStandard y))

特别的是，我们使用runBT来控制何时以及类型lambda在BT中被应用的次数。

decode_encode :: BT -> BT
decode_encode x = runBT x initial_module

runBT的一个用途对应于量化类型的一次合一（unification）。