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

Question

我正在尝试理解给定通用多态性功能的递归代数数据类型的定义、解和编码。作为一个例子，我尝试通过

实现递归类型的二叉树

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

的直觉是二叉树的类型应该是初始的所有类型T具有常数e: T和二进制操作m: T -> T -> T，即函子BTAlg上的"初始模"。换句话说，对于T, BT的元素是为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))'

谢谢!

Answer 1

如果您查看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和runBT的见证下建立了一个同构的BT ~ forall z . (BTAlg z -> z) -> z。只要我们把那些证人安排在正确的地点，我们就可以向前推进。

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对应一次量化类型的统一。