ANN: H98 FFI Addendum 1.0, Release Candidate 10

[Manuel M T Chakravarty]

"Simon Marlow" <simonmar at microsoft.com> wrote,

> > We routinely use code like this:
> > 
> >   data Point
> >   foreign import getMousePos :: Ptr Point ->  IO ()
> >   foreign import getX :: Ptr Point -> IO Int
> >   foreign import getY :: Ptr Point -> IO Int
> > 
> > The idea being that:
> > 
> > 1) there is a foreign type (which might be called Point, 
> > MousePos, point_t, struct point or whatever)
> > 
> > 2) that we have a pointer to it
> > 
> > 3) that the thing we have a pointer to can take on a number 
> > of different 
> > values.  We don't know what the values are but this doesn't 
> > mean they don't exist.
> 
> Let's be clear about the role of Point here:  it is a dummy type
> argument to Ptr, used to disambiguate the type 'Ptr Point' from any
> other kind of Ptr.  It is for type-safety in the Haskell code.
> 
> Additionally, the type argument to Ptr is used to resolve overloading
> when doing marshalling using the Storable class, but we're not using
> that facility here because no marshalling is going on.
> 
> There definitely aren't any values of type Point, so I don't see why it
> needs a semantics.  The semantics of empty data declarations seems like
> an entirely orthogonal issue, and I don't see any problem with the
> current semantics for empty data declarations, which is a completely
> natural degenerate case of ordinary data declarations.
> 
> > > And what do you mean by a trick?
> > 
> > It is possible that, since we cannot directly observe values 
> > of foreign types, 
> > we can safely model the type as having just one value 
> > (bottom) or, perhaps 
> > even no values at all.  By this I mean that exactly the same 
> > properties can 
> > be proved whether we use an accurate model or a simplified model.
> > 
> > But, it is a trick because we know that there is not just one 
> > (or zero) values in that type (at least, for most types).
> 
> I don't agree with that last sentence: there's no trickery going on; it
> doesn't matter how many values of the type Point there are.  I could use
> any Haskell type with the same results.
> 
> Let me say this another way:  the type argument to Ptr in no way
> represents the type of the foreign data.  It is used to resolve
> overloading and to disciminate pointer types in Haskell marshalling
> code, that's all.  There is no link between the semantics of the Haskell
> type and the semantics of the foreign type (whatever that might be), and
> we shouldn't confuse the issue by pretending that there is.

Exactly what I think, too.  Empty data types are used as
Skolem constants in the type checker.

Alastair wrote earlier that `data T' is not inhibited
(except by bottom as we have a lazy language).  That's
semantically exactly what we want.  Hence, if the compiler
wants to regard two values of type `T' to be the same, it is
perfectly reasonable to do that.  That's the point where
IMHO Alastair's earlier argument was flawed (and what has
led to the misunderstanding).

My main problem with this extension is the following:

* As we have learnt, nhc98 and Hugs use `data T' for an
  entirely different purpose than the one proposed by John
  (namely to represent primitive external types).  It may be
  possible to abuse nhc98 and Hugs `data T' also in the way
  John wants it (and GHC provides it), but this sounds less
  straight forward than initially where the impression was
  given that the three systems already implement the same
  extension.

* So far, the FFI addendum has managed to stay away from
  changing anything at H98's syntax other than adding
  `foreign'.  I am reluctant to change that, but then it is
  really a very small change that won't break anything.

BTW, I tend to use the following (which - suprise, suprise -
is what c2hs generates in that situation):

  data Point = Point (Ptr Point)

  foreign import getMousePos :: Point ->  IO ()

No need for an extension here and I hide from the
application programmer the fact that the argument to
`getMousePos' is a pointer.

Cheers,
Manuel