有没有一种方法在GHC Haskell中定义一个存在量化的newtype？

Question

在Haskell的(GHC)中是否有可能定义一个存在量化的新类型？我知道如果涉及到类型类，那么在字典传递实现中是无法做到的，但对于我的目的来说不需要类型类。我真正想定义的是这个：

newtype Key t where Key :: t a -> Key t

但 GHC 似乎不喜欢它。 我目前正在使用 data Key t where Key :: !(t a) -> Key t。 有没有办法（也许只是使用 -funbox-strict-fields？）定义一个与上面新类型版本相同语义和开销的类型？我的理解是，即使强制字段未装箱，仍将存在额外的标记字，尽管我可能完全错误。这些不会对我的性能造成任何明显问题。只是新类型不被允许让我感到惊讶。我是一个天生好奇的人，所以我不禁想知道我拥有的版本是否被编译为相同的表示形式，或者是否可以定义任何等效类型。

- mokus

---

我其实有点惊讶于存在量词没有上下文的合理示例，但你找到了一个看起来有些有用的例子。 - augustss

令人惊讶的是，这甚至不是我发现自己想要的唯一GADT，它本可以是一个新类型。曾经我尝试定义一个将类型构造器应用于虚拟类型参数的GADT，例如newtype F f t a where F :: t a -> F f t (f a)。在这么短的空间里很难解释它为什么有用，但我确实发现自己需要这样一个东西。 - mokus

Answer 1

不可以，根据GHC的规定：

一个新类型构造器不能有存在上下文

然而，data就没问题：

{-# LANGUAGE ExistentialQuantification #-}

data E = forall a. Show a => E a

test = [ E "foo"
       , E (7 :: Int)
       , E 'x'
       ]

main = mapM_ (\(E e) -> print e) test

例如

*Main> main
"foo"
7
'x'

从逻辑上讲，你确实需要在某个地方分配字典（或标签）。如果你删除构造函数，这是没有意义的。

注意：你不能取消函数的拆箱，就像你所暗示的那样，也不能取消多态字段。

---

有没有办法（可能只使用 -funbox-strict-fields？）定义一个与上面新类型版本具有相同语义和开销的类型？

删除 -XGADTs 可以帮助我思考这个问题：

{-# LANGUAGE ExistentialQuantification #-}

data Key t = forall a. Key !(t a)

就像这样，Key (Just 'x') :: Key Maybe

所以您希望确保Key构造函数被擦除。

以下是GHC中用于检查newtype约束的代码：

-- Checks for the data constructor of a newtype
checkNewDataCon con
  = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
        -- One argument
    ; checkTc (null eq_spec) (newtypePredError con)
        -- Return type is (T a b c)
    ; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
        -- No existentials
    ; checkTc (not (any isBanged (dataConStrictMarks con)))
          (newtypeStrictError con)
        -- No strictness

我们可以看出为什么 ! 不会对表示产生任何影响，因为它包含多态组件，所以需要使用通用表示。而非举例构造函数也没有意义。

我唯一能想到的是，就像存在类型的记录访问器一样，如果暴露了newtype，不透明类型变量将被释放。

- Don Stewart

---

我知道这是不允许的，我的意思是为什么在我给出的具体示例中不能允许，或者是否存在任何解决方案以获得类似的高效运行时表示。我的示例需要哪个字典？这里没有类型类。此类型的唯一功能是“忘记”幻影类型参数。 - mokus

更新以更多地讨论“newtype”将遇到的表示问题。 - Don Stewart

这个论点同样适用于 newtype Identity a = Identity a 吗？还是说适用于 newtype Key f a = Key (f a)？ - mokus

嗯。是的，这是一个很好的观点！这就是为什么你不能有未提升的 newtype 的原因。我认为问题与存在类型记录的访问器的类似问题有关，这会导致不透明上下文逃逸。解包 newtype 会产生类似的效果（虽然你可以想象这样工作，只要构造函数没有被过早抹掉）。 - Don Stewart

嗯，从实际角度来看，如果在编译器内部处理新类型的匹配与data类型不同，这将是有意义的。在某种程度上，我知道它确实是这样的，因为新类型不会得到包装函数。在这种情况下，对我来说更像是“我们不这样做，因为这是额外的工作，除了mokus之外没有人想要它”;)。 - mokus

我也想要...更详细地说，单例模式下依赖编程的日益普及使你想要它，因为这使得将Int值映射到类似于Nat的类型变得更加经济实惠。 - NioBium

Answer 2

我看不出它不能工作的理由，但也许ghc在内部表示方面存在一些问题。

- augustss

---

是的，我认为这是唯一有意义的事情。newtype 不能太早被擦除，因为存在类型会在 GHC 的类型转换中变得可见。否则，这似乎是一个合法的做法。 - Don Stewart

我怀疑这可能归结于这样的事情。如果没有其他的，GHC在Core中传递类型相等证明之类的东西吗？我假设它们会出现在记录中携带的字典中，并通过模式匹配进行解包。即使它们在运行时不存在，它们存在于Core中的事实意味着新类型必须具有“除了~字典之外没有额外字段”的规则，这似乎是相当特别的。 - mokus

现在 GHC 做的事情和它应该做的事情是两回事。对 newtype 的当前处理方式是不可靠的。也许你应该在 trac 上提出一个增强请求，也许 Simon 会让它工作。 - augustss

有趣。你是在指 http://hackage.haskell.org/trac/ghc/ticket/1496 还是其他的不安全性问题？我知道现有的 GeneralizedNewtypeDeriving 实现可以用来破坏隐藏的不变量，但我没有意识到它实际上可以用来实现 unsafeCoerce！ - mokus

此外，一个有趣的事实是，Core中显然包含了对newtypes的类型相等断言，这可能是newtypes不能具有存在类型的主要原因。据我所知，System F没有存在类型，因此它没有可以相等的对象。 - mokus