Ptr type

[Simon Peyton Jones]

I've moved this thread to https://ghc.haskell.org/trac/ghc/ticket/9163



| -----Original Message-----
| From: mad.one at gmail.com [mailto:mad.one at gmail.com] On Behalf Of Austin
| Seipp
| Sent: 03 June 2014 14:22
| To: Richard Eisenberg
| Cc: Simon Peyton Jones; ghc-devs at haskell.org
| Subject: Re: Ptr type
| 
| I think Ptr should almost certainly be representational, as it is a case
| where the actual underlying value is the same, but what it points to is
| not (I'll ignore castPtr here for a second).
| 
| This makes me think of something I talked about before with Andres - in
| general, phantom roles seem somewhat dangerous, and I kind of wonder if
| they should be inferred by default. Often you see some code along the
| lines of:
| 
| ----------------------------------
| 
| module A ( Bar, newBarInt ) where
| 
| data Bar a = Bar Int
| 
| newBarInt :: Int -> Bar Int
| 
| ---------------------------------
| 
| where A is exported to the client and the module boundary enforces some
| restrictions on 'Bar', like what types we can instantiate 'Bar a'
| to (the example is dumb but bear with me).
| 
| In the above example, I believe the `a` in `Bar a` would be inferred at
| phantom role.
| 
| The question I have is: what legitimate case would there be for phantom
| roles like this? Such usage of phantom type parameters seems very
| common, but in almost *all* cases I can't think of a reason why I would
| ever want a user to be allowed to `coerce` away the type information, if
| the `a` parameter was phantom. It seems like in the above example, I
| would almost certainly want `a` to be representational instead.
| 
| What other cases exist for legitimate phantom roles such as this where
| we want this inference? I wonder if instead we should require an
| explicit role annotation for phantoms in this case - not the other way
| around.
| 
| Ptr is a similar story - by default it would maybe seem reasonable to be
| phantom, but that seems like an especially grievous error, given we
| don't want people to `poke` incorrect values in or something (again,
| ignoring castPtr for a second, but I think the general idea holds.)
| 
| 
| On Tue, Jun 3, 2014 at 7:24 AM, Richard Eisenberg <eir at cis.upenn.edu>
| wrote:
| > It seemed clear to me that Ptr *should* be representational, thinking
| > that we don't want to coerce a `Ptr Int` to a `Ptr Bool`. I don't see
| > any reason why this couldn't be changed.
| >
| > Why is Ptr a `data` not a `newtype`? If it were a newtype, we could
| > keep the role annotation and use `coerce` internally, according to the
| > updated Coercible solver.
| >
| > However, it is crucial that FunPtr have a representational argument,
| > as normaliseFfiType' depends on this fact. There is a brief comment in
| > TcForeign, but clearly more comments are necessary. Will do shortly.
| > If we want to change FunPtr's role, normaliseFfiType' would have to be
| > updated, too, but it shouldn't be hard.
| >
| > More comments in the code later today.
| >
| > Richard
| >
| > On Jun 3, 2014, at 7:13 AM, Simon Peyton Jones <simonpj at microsoft.com>
| > wrote:
| >
| > Richard
| >
| > In GHC.Ptr we see
| >
| > type role Ptr representational
| > data Ptr a = Ptr Addr# deriving (Eq, Ord)
| >
| > with no comments.  Why is Ptr representational?
| >
| > In the same module we have castPtr, which unpacks and repacks a Ptr.
| > If Ptr was phantom, we could use coerce.  And that in turn would
| > actually make a lot of code more efficient – there are lots of calls
| to castPtr.
| >
| > Simon
| >
| >
| >
| >
| >
| > _______________________________________________
| > ghc-devs mailing list
| > ghc-devs at haskell.org
| > http://www.haskell.org/mailman/listinfo/ghc-devs
| >
| 
| 
| 
| --
| Regards,
| 
| Austin Seipp, Haskell Consultant
| Well-Typed LLP, http://www.well-typed.com/