haskell - 通过 Haskell 中的多态性递归代数数据类型

鉴于通用多态性的功能，我试图理解递归代数数据类型的定义、解译和编码。作为一个例子，我试图通过实现递归类型的二叉树

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

直觉是，二叉树的类型应该是所有类型 T 中的初始值，它配备了一个常数 e: T 和一个二元运算 m: 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 必须专门用于 BT 中的 x 才能使 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 的通用属性应用于 BTAlg 上的规范 BTStd 模块结构:

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))'

谢谢!

最佳答案

如果您查看 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 来控制 BT 中的类型 lambda 被应用的时间和次数

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

runBT 的一种使用对应于量化类型的一种统一。

关于haskell - 通过 Haskell 中的多态性递归代数数据类型，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/24361736/

bt

haskell - 通过 Haskell 中的多态性递归代数数据类型