Is there a way to define an existentially quantified newtype in GHC Haskell?

Question

Is it possible in (GHC) Haskell to define an existentially-quantified newtype? I understand that if type classes are involved it can't be done in a dictionary-passing implementation, but for my purposes type-classes are not needed. What I'd really like to define is this:

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

But GHC does not seem to like it. Currently I'm using data Key t where Key :: !(t a) -> Key t. 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? My understanding is that even with strict fields unboxed there will still be an extra tag word, though I could be totally wrong there.

This is not something that's causing me any noticeable performance issues. It just surprised me that the newtype was not allowed. I'm a naturally curious person, so I can't help wondering whether the version I have is being compiled to the same representation or whether any equivalent type could be defined which would be.

I'm actually somewhat surprised that there are any sensible examples of existentials without a context, but you have found one that looks somewhat useful. — augustss
Surprisingly, it's not even the only GADT I've found myself wanting which could be a newtype. At one point I tried to define one that applies a type constructor to a phantom type parameter, e.g. newtype F f t a where F :: t a -> F f t (f a). It's hard to explain why it's useful in such a short space here, but I actually did find myself wanting such a beast. — mokus

Don Stewart Don Stewart · Accepted Answer · 2011-05-04T21:42:42

No, according to GHC:

A newtype constructor cannot have an existential context

However, data is just fine:

{-# 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

E.g.

*Main> main
"foo"
7
'x'

Logically, you do need the dictionary (or tag) allocated somewhere. And that doesn't make sense if you erase the constructor.

Note: You can't unbox functions though, as you seem to be hinting at, nor polymorphic fields.

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?

Removing the -XGADTs helps me think about this:

{-# LANGUAGE ExistentialQuantification #-}

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

As in, Key (Just 'x') :: Key Maybe

enter image description here

So you want to guarantee the Key constructor is erased.

Here's the code in GHC for type checking the constraints on 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

We can see why ! won't have any effect on the representation, since it contains polymorphic components, so needs to use the universal representation. And unlifted newtype doesn't make sense, nor non-singleton constructors.

The only thing I can think of is that, like for record accessors for existentials, the opaque type variable will escape if the newtype is exposed.

Is there a way to define an existentially quantified newtype in GHC Haskell?

2 Answers