为什么GHC拒绝允许这个存在类型函数？

Question

我定义了一个通用的类型（我称之为“异构”类型，但我不知道是否正确）：

data Heterotype f = forall a. f a => Heterotype a

随后，我决定创建一个函数，允许您从多态值创建异构类型：

hset :: (forall a. f a => a) -> Heterotype f
hset x = Heterotype x

然而，GHC报错如下：

████████.hs:15:10: error:
    * Could not deduce: f a0 arising from a use of `Heterotype'
    * In the expression: Heterotype x
      In an equation for `hset': hset x = Heterotype x
    * Relevant bindings include
        x :: forall a. f a => a
          (bound at ████████.hs:15:6)
        hset :: (forall a. f a => a) -> Heterotype f
          (bound at ████████.hs:15:1)
   |
15 | hset x = Heterotype x
   |          ^^^^^^^^^^^^

< p > 编辑: 以下扩展已启用：

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE NoStarIsType, ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes, RankNTypes #-}
import Data.Kind

- schuelermine

Answer 1

从逻辑角度来看，您的代码相当于一个可以读作如下（大致）的逻辑公式的证明：

- 让f成为任意类型的属性； - 假设对于任何满足f的类型a，我们都可以产生一个类型为a的值x； - 那么，存在一个满足f且具有值x的类型a。

这并不是逻辑上正确的。实际上，可能不存在任何a使得f a成立。在这种情况下，上述假设会虚假成立，因此它是真实的。然而，上述结论与f a始终为假的事实相矛盾。

因此，我们无法用该类型定义您的hset。

为了使论点正确，我们必须添加额外的假设，即存在某个类型b使得属性f成立。如果我们添加了这个假设，我们就可以证明该语句：

-- (untested, but should work)
hset :: forall b . f b => (forall a. f a => a) -> Heterotype f
hset x = Heterotype (x :: b)

- chi

---

好的，但是 Haskell 有 mempty :: forall a. Monoid a => a。 - schuelermine

@schuelermine 我没看出来这与问题有何关系？你能详细说明一下吗？你的代码使用了一个通用的 f，它可能是 Monoid，但也可能是其他东西。 - chi

是的，但如果我有一个值 p :: F a => a，那么我可以调用 newhset p :: Heterotype F。为什么我不能编写一个只接受这种多态值 x :: F a => a 并将它们放入 newhset 的函数呢？我想可以定义一个过于具体化的函数版本。 - schuelermine

如果您想在构造函数中存储您的 p，那么您需要使用普遍量化而不是存在量化，即 data Heterotype f = Heterotype (forall a. f a => a)，其中可以定义 newhset = Heterotype。您发布的版本使用了存在量化，这要求某些类型满足 F。 - chi

Answer 2

你的数据定义通过将一个值与 f 的字典打包起来，隐藏了一个单调选择的 a 。需要注意的是，这样做的整个目的是丢弃有关特定类型的信息，同时保留与该类型相关联的实例词典。

这与你在 hset 中尝试做的事情不兼容。从来没有一个具体的类型可以打包实例。这些部分无法配合使用，因为它们都缺少相同的必需内容。 Heterotype f 和 (forall a. f a => a) 都缺少具体类型来选择实例，但是 Heterotype 构造函数需要包括具体实例。信息不存在。这些部分不兼容。

- Carl

---

@schuelermine 这个问题足够大，值得在这里提出一个完整的问题。 - Carl

Answer 3

你的要求略微过于详细了 :), 下面这种写法可以正常工作：

data Heterotype f = forall a. f a => Heterotype a

hset :: forall f a. f a => a -> Heterotype f
hset x = Heterotype x

差别在于你量化了你的论点：(forall a. f a => a)，这意味着该函数接受一个表达式，该表达式必须是任意可能类型之一（调用者无法选择特定的 'a'），这不是很有意义。新版本（因此与仅使用Heterotype构造函数相同）表示调用者可以选择 a 的类型，可以是任何东西，但必须正好是一个类型（每次调用）。

有点练习才能习惯存在性; 最好的方法是反复试验 :)

- Chris Penner