haskell - 有没有办法在 GHC Haskell 中定义一个存在量化的新类型？

Question

在(GHC)Haskell 中是否可以定义一个存在量化的新类型？我知道如果涉及类型类，则无法在字典传递实现中完成，但出于我的目的，不需要类型类。我真正想定义的是:

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

但 GHC 似乎并不喜欢它。目前我正在使用 data Key t where Key :: !(t a) -> Key t .有没有办法(也许只是使用 -funbox-strict-fields ？)来定义与上面的 newtype 版本具有相同语义和开销的类型？我的理解是，即使严格的字段未装箱，仍然会有一个额外的标签词，尽管我可能完全错了。

这不会导致我出现任何明显的性能问题。让我感到惊讶的是不允许使用新类型。我是一个天生好奇的人，所以我不禁想知道我拥有的版本是否被编译为相同的表示形式，或者是否可以定义任何等效类型。

Answer 1

不，根据 GHC:

A newtype constructor cannot have an existential context

但是， 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'

从逻辑上讲，您确实需要在某处分配字典(或标签)。如果你删除构造函数，那是没有意义的。

注意:您不能像您暗示的那样拆箱函数，也不能拆箱多态字段。

Is there any way (perhaps just using -funbox-strict-fields?) to define a type with the same semantics and overhead as the newtype version above?

删除 -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没有意义，也没有非单例构造函数。

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