Ptr type

[Austin Seipp]

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/