存在类型包装器的必要性

Question

事实证明，虽然存在/秩为n的类型背后的思想非常简单，但正确使用它们却令人惊讶地困难。

为什么将存在类型包装成data类型是必要的？

我有以下简单示例：

{-# LANGUAGE RankNTypes, ImpredicativeTypes, ExistentialQuantification #-}
module Main where

c :: Double
c = 3

-- Moving `forall` clause from here to the front of the type tuple does not help,
-- error is the same
lists :: [(Int, forall a. Show a => Int -> a)]
lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

data HRF = forall a. Show a => HRF (Int -> a)

lists' :: [(Int, HRF)]
lists' = [ (1, HRF $ \x -> x)
         , (2, HRF $ \x -> show x)
         , (3, HRF $ \x -> c^x)
         ]

如果我注释掉lists的定义，代码将成功编译。如果我不注释它，我会得到以下错误：

test.hs:8:21:
    Could not deduce (a ~ Int)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:8:11-22
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:8:11
    In the expression: x
    In the expression: \ x -> x
    In the expression: (1, \ x -> x)

test.hs:9:21:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:9:11-27
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:9:11
    In the return type of a call of `show'
    In the expression: show x
    In the expression: \ x -> show x

test.hs:10:21:
    Could not deduce (a ~ Double)
    from the context (Show a)
      bound by a type expected by the context: Show a => Int -> a
      at test.hs:10:11-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => Int -> a at test.hs:10:11
    In the first argument of `(^)', namely `c'
    In the expression: c ^ x
    In the expression: \ x -> c ^ x
Failed, modules loaded: none.

为什么会发生这种情况？第二个例子不应该与第一个等效吗？n级别类型的这些用法有什么区别？在我需要这种多态性时，是否可能省略额外的ADT定义并仅使用简单类型？

- Vladimir Matveev

Answer 1

你的第一次尝试不是使用存在类型。相反，你

lists :: [(Int, forall a. Show a => Int -> a)]

要求第二个组件能够提供我选择的任何可显示类型的元素，而不仅仅是你选择的某些可显示类型。您正在寻找

lists :: [(Int, exists a. Show a * (Int -> a))]  -- not real Haskell

但这并不是你所说的。数据类型打包方法允许您通过柯里化从forall中恢复exists。您已经

HRF :: forall a. Show a => (Int -> a) -> HRF

这意味着要构建一个HRF值，您必须提供一个三元组，其中包含类型a、a的Show字典以及一个Int -> a的函数。也就是说，HRF构造函数的类型有效地对这个非类型进行了柯里化。

HRF :: (exists a. Show a * (Int -> a)) -> HRF   -- not real Haskell

您可以通过使用rank-n类型来编码存在性，从而避免使用datatype方法。

type HRF = forall x. (forall a. Show a => (Int -> a) -> x) -> x

但这可能有些过头了。

- pigworker

Answer 2

在处理存在类型的时候，你需要考虑两个问题：

• 如果你存储“任何可以进行显示的内容”，那么你必须同时存储可以显示的内容和如何显示它。
• 实际变量只能有一个单一的类型。

第一个问题是为什么你必须拥有存在类型包装器的原因，因为当你写下这个代码时：

data Showable = Show a => Showable a

实际发生的情况是声明类似于以下内容：

data Showable a = Showable (instance of Show a) a

即，Show a类实例的引用与值a一起存储。如果没有这个过程，就无法拥有一个函数来解开Showable，因为该函数不知道如何显示a。

第二点是您有时会遇到一些类型怪异现象的原因，以及为什么您不能在例如let绑定中绑定存在类型。

---

您的代码推理也存在问题。如果您有一个函数，例如forall a . Show a => (Int -> a) ，则您将获得一个函数，只要调用者选择，它就可以产生任何类型的可显示值。您可能的意思是exists a . Show a => (Int -> a)，这意味着如果该函数获取一个整数，它将返回某个类型，该类型存在Show实例。

- dflemstr

---

非常感谢您的解释。所有的答案都非常有帮助，但我认为从您的答案中找到了“少缺的拼图块”，因此我将其标记为被采纳。 - Vladimir Matveev

Answer 3

这些例子并不相等。第一个例子，

lists :: [(Int, forall a. Show a => Int -> a)]

这段文字表明每个秒组件都可以生成任何所需类型，只要它是来自一个Int的Show实例。

第二个例子相当于类型包装器的模数。

lists :: [(Int, exists a. Show a => Int -> a)]

即，每个第二组件可以从一个Int产生一些属于Show类型的值，但是你不知道这个函数返回哪种类型。

此外，你放入元组中的函数不满足第一个约定：

lists = [ (1, \x -> x)
        , (2, \x -> show x)
        , (3, \x -> c^x)
        ]

\x -> x 产生与输入相同类型的结果，因此在这里是 Int。 show 总是生成一个 String，因此它是一个固定的类型。最后，\x -> c^x 产生与 c 相同的类型，即 Double。

- Daniel Fischer