存在型包装必需品

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通过钻营.你有

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

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

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

您可以通过使用rank-n类型对教会编码存在主义来避免数据类型方法

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

但这可能是矫枉过正的.

Answer 2

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

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

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

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实例的类型。