Is there a way to define an existentially quantified newtype in GHC Haskell?
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 :: !(ta) -> 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.
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
Eg
*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
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.
我看不出有什么理由不能做，但也许ghc有一些内部代表性问题。
链接地址: http://www.djcxy.com/p/7532.html上一篇: 更广泛的新型派生