haskell - 存在类型包装器的必要性

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 定义并仅使用简单类型？

Answer 1

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

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

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

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

但这不是你所说的。数据类型打包方法可以让你恢复 exists来自 forall通过 curry 。你有

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

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

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

但这可能是矫枉过正。