5

事实证明，尽管它们背后的想法非常简单，但要正确使用存在/秩-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 定义并仅使用简单类型？

4

3 回答 3

6

您的第一次尝试是不使用存在类型。而是你的

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

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

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

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

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

这意味着要构建一个HRF值，您必须提供一个三元组，其中包含一个 type a、一个Show字典 fora和一个 in 函数Int -> a。也就是说，HRF构造函数的类型有效地将这个非类型

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

您可以通过使用 rank-n 类型对存在性进行 Church-encode 来避免使用数据类型方法

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

但这可能是矫枉过正。

于 2012-06-03T14:12:13.007 回答
3

示例不等价。首先，

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

表示每个第二个组件都可以产生任何所需的 type，只要它是Showfrom an的一个实例Int。

第二个例子是模数类型包装器等价于

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

即，每个第二个组件都可以生成属于from 的某种类型，但是您不知道该函数返回哪种类型。ShowInt

此外，您放入元组的函数不满足第一个合同：

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

\x -> x产生与作为输入给出的结果相同的类型，所以在这里，就是Int. show总是产生 a String，所以它是一种固定类型。最后，\x -> c^x产生与 has 相同的类型c，即Double.

于 2012-06-03T14:06:31.960 回答
3

关于存在类型的处理，您必须考虑两个问题：

  • 如果你存储“任何可以是shown 的东西”，你必须存储可以显示的东西以及如何显示它。
  • 一个实际变量只能有一种类型。

第一点是为什么你必须有存在类型包装器，因为当你写这个时：

data Showable = Show a => Showable a

实际发生的是这样的事情被宣布：

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

即对类实例的引用Show a与值一起存储a。如果不发生这种情况，您将无法拥有解包 a 的函数Showable，因为该函数不知道如何显示a.

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

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

于 2012-06-03T14:06:41.130 回答