haskell - 为什么 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
   |          ^^^^^^^^^^^^

编辑:启用以下扩展:

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

Answer 1

从逻辑的角度来看，您的代码将对应于逻辑公式的证明，可以按如下方式阅读(大致):

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

这在逻辑上不合理。事实上，无论 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)