存在类型作为返回值答案

【问题标题】：Existential type as return value存在类型作为返回值
【发布时间】：2018-05-16 20:33:44
【问题描述】：

考虑以下数据结构，表示一棵树，其层级不断增加，但不一定是连续的：

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => [MyTree ('Succ z)] -> MyTree n

其中T代表类型级别的Peano数，定义为

class Plus (n :: T) (m :: T) (r :: T) | r n -> m
instance Plus 'Zero m m
instance Plus n m r => Plus ('Succ n) m ('Succ r)

像这样构造树很容易

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode [ MyLeaf, myTreeOne ]

或

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode [ myLeafTwo ]

现在我想定义以下函数：

myTreeComponents MyLeaf              = []
myTreeComponents (MyNode components) = components

它只是提取树的直接子节点列表，但我无法写出正确的类型。

这是我得到的错误

    • Couldn't match expected type ‘p’                                                                                │
                  with actual type ‘[MyTree ('Succ z)]’                                                               │
        because type variable ‘z’ would escape its scope                                                              │
      This (rigid, skolem) type variable is bound by                                                                  │
        a pattern with constructor:                                                                                   │
          MyNode :: forall (n :: T) (m :: T) (z :: T).                                                                │
                    Plus n m z =>                                                                                     │
                    [MyTree ('Succ z)] -> MyTree n,                                                                   │
        in an equation for ‘myTreeComponents’                                                                         │
        at src/Model.hs:159:19-35                                                                                     │
    • In the expression: components                                                                                   │
      In an equation for ‘myTreeComponents’:                                                                          │
          myTreeComponents (MyNode components) = components                                                           │
    • Relevant bindings include                                                                                       │
        components :: [MyTree ('Succ z)] (bound at src/Model.hs:159:26)                                               │
        myTreeComponents :: MyTree n -> p (bound at src/Model.hs:158:1)                                               │
    |                                                                                                                 │
159 | myTreeComponents (MyNode components) = components                                                               │
    |                                        ^^^^^^^^^^

对于依赖类型语言，它应该类似于

exists m. Plus n m z => MyTree n -> [ MyTree ('Succ z) ]

是否可以在 Haskell 中编写这样的类型？否则我应该如何编写我的函数？

【问题讨论】：

您需要使用自定义data GADT 定义自己的存在类型。它看起来像MyTree，但只有第二个构造函数。但是，从第一个类型中提取 m,z 以在存在主义中使用是非常棘手的：如果您可以将代理添加到 MyNode 构造函数，可能会更容易。（这很痛苦。如果 Haskell 有真正的依赖类型，或者更好的模糊类型，那就更容易了。）
感谢@chi，很抱歉，但我发现很难遵循您的建议。能否请您详细说明一下答案？
在写评论之前，我花了一些时间尝试解决方案，但花费的时间比我预期的要长，所以我中途停了下来。
@chi，添加代理应该不会太糟糕。如果它被标记为严格，它将“解包”为空。有一个 GHC 提案可以更好地绑定存在类型变量。
@chi，见the proposal。我个人有点担心所有这些类型变量的排序对未围绕这些功能设计的库 API 有何影响。

标签： haskell existential-type

【解决方案1】：

这是对您的代码的修改，添加了Proxy，因此要“记住”数字m。

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, 
    MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS -Wall #-}

import Data.Proxy

data T = Zero | Succ T

class Plus (n :: T) (m :: T) (z :: T) | n m -> z where

instance Plus n 'Zero n
instance Plus n m z => Plus n ('Succ m) ('Succ z)

data MyTree (n :: T) where
    MyLeaf :: MyTree n
    MyNode :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> MyTree n

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode (Proxy :: Proxy 'Zero) ([ MyLeaf ] :: [MyTree ('Succ ('Succ 'Zero))])

myTree :: MyTree 'Zero
myTree = MyNode (Proxy :: Proxy 'Zero) [ MyLeaf, myTreeOne ]

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode (Proxy :: Proxy ('Succ 'Zero)) [ myLeafTwo ]

为了能够编写最终函数myTreeComponents，我们需要一个自定义存在类型：

data Nodes (n :: T) where
    Nodes :: Plus n m z => ! (Proxy m) -> [MyTree ('Succ z)] -> Nodes n

这本质上是MyTree，只有第二个构造函数。最后，模式匹配现在就足够了。

myTreeComponents :: MyTree n -> Nodes n
myTreeComponents MyLeaf                = Nodes (Proxy :: Proxy 'Zero) []
myTreeComponents (MyNode p components) = Nodes p components

【讨论】：

不错！我试图消除代理（并对此有答案）；在这样做的同时，我注意到这个答案中有很多微妙的技巧。很高兴看到一个有效的例子。

【解决方案2】：

您通常可以使用 CPS 来编码存在。

exists a. f a

可以表示为

(forall a. f a -> r) -> r

但是，我不认为你的

exists m. Plus n m z => MyTree n -> [ MyTree ('Succ z) ]

是你想要的类型。首先，exists 在错误的地方——不存在单一的全局类型m，而是对于每个MyTree n，都有一个可能不同的m。

MyTree n -> exists m. Plus n m z => [ MyTree ('Succ z) ]

在这里，调用者可以选择z，并且根据n + m = z 的证据，可以提取孩子的列表。这是一致的，但这样的证据可能很难获得。我认为您实际上想要双重存在：

MyTree n -> exists m z. Plus n m z & [ MyTree ('Succ z) ]

我使用& 作为=> 的对偶，这是一种包含字典而不需要它作为参数的类型。

type a & b = (Dict a, b)

这就是说，对于n 级别的任何树，都有一些z >= n（通过与m 相加来证明），因此在'Succ z 级别有一个子级列表。是的，我认为这是正确的。所以现在让我们将其 CPS 编码为：

MyTree n -> (forall m z. Plus n m z => [ MyTree ('Succ z) ] -> r) -> r

【讨论】：

你真的试过这个吗？我不认为没有代理它可以工作。即使启用了模棱两可的类型，我也失败了。我相信，使用代理它应该可以工作。
@chi 我试图用最后一行中提出的签名编译我的函数，一切似乎都很好

【解决方案3】：

我喜欢 chi 的修复，因为使用 Proxys 存储类型是一个很好的技巧。在他的回答中，Proxy 用于消除在调用Nodes 构造函数时在Plus n m z 约束中使用的m 的歧义。（此时范围内有一个Plus n m z 约束，但没有代理，就无法告诉编译器选择它。）

除了Proxy，还有另一种修复歧义类型的方法：消除歧义类型。在这种情况下，就是m。因此，我们将拥有一个 LE n z 类，而不是 Plus n m z 类，它具有所有相同的实例，但在任何地方都没有提及 m。所以：

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, 
    MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

data T = Zero | Succ T

class LE (n :: T) (z :: T)
instance LE 'Zero n
instance LE n z => LE ('Succ n) ('Succ z)

有一个皱纹。在 chi 的回答中，他使用了 Plus 的略微修改的定义，它免费提供了 Plus n 'Zero n 实例，但在您的公式中，这是不可用的，因此 LE n n 不是免费的。所以我们得稍微装饰一下我们的叶子。

data MyTree (n :: T) where
    MyLeaf :: LE n n => MyTree n
    MyNode :: LE n z => [MyTree ('Succ z)] -> MyTree n

所有的混凝土树都和以前一样（不需要额外的Proxy）。

myTreeOne :: MyTree ('Succ 'Zero)
myTreeOne = MyNode [ MyLeaf :: MyTree ('Succ ('Succ 'Zero)) ]

myTree :: MyTree 'Zero
myTree = MyNode [ MyLeaf, myTreeOne ]

myLeafTwo :: MyTree ('Succ ('Succ 'Zero))
myLeafTwo = MyLeaf

myOtherTree :: MyTree 'Zero
myOtherTree = MyNode [ myLeafTwo ]

与 chi 的答案相比，myTreeComponents 的唯一区别（除了删除 Proxy）是我们需要将类型变量带入范围以在正文中使用。

data Nodes (n :: T) where
    Nodes :: LE n z => [MyTree ('Succ z)] -> Nodes n

myTreeComponents :: forall n. MyTree n -> Nodes n
myTreeComponents MyLeaf              = Nodes ([] :: [MyTree ('Succ n)])
myTreeComponents (MyNode components) = Nodes components

【讨论】：

【解决方案4】：

类似的东西（我不知道这种类型是否允许，现在无法检查）

MyNode n -> forall z .Plus n m z => [MyTree ('Succ z)]

z 类型未公开，因此可以是任何类型。如果z 的类型被myTreeComponents 暴露，调用者可以为它指定一个具体的类型，它一定不能这样做

【讨论】：

谢谢，但它似乎不起作用。错误信息是一样的
这里使用的是全称而不是存在量化，所以不能用。