RE: ANN: H98 FFI Addendum 1.0, Release Candidate 10
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. Cheers, Simon
"Simon Marlow" <simonmar@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
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.
It doesn't matter how many values of the type Point there are. I could use any Haskell type with the same results.
There definitely aren't any values of type Point, so I don't see why it needs a semantics.
OK, I think I agree with all of this.
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.
Actually, I think both Hugs and nhc98 straightforwardly allow John's use. All three systems do implement the same extension. In fact it is the current usage of 'data T' for primitive types that is tricky. At the moment, basically they must be *internal* types, i.e. types already known to the Haskell runtime system. The idea of using them for external, previously unknown, types is entirely speculative. It would require somehow specifying storage sizes, and routines to marshal values into the heap, and perhaps more. None of these mechanisms yet exist. The question was raised as to whether we might one day want those facilities, because the natural place to specify them is in the FFI. But no-one even has a proposal for how it might work, so I think we can safely dismiss it at this stage.
data Point foreign import getMousePos :: Ptr Point -> IO () foreign import getX :: Ptr Point -> IO Int foreign import getY :: Ptr Point -> IO Int
vs
data Point = Point (Ptr Point) foreign import getMousePos :: Point -> IO ()
I like the second idiom. You are right that there is no need for the application programmer to know whether pointers are involved, because even in the first style, it is not possible to 'peek' inside a Ptr Point to get the `actual' Point value. So why not hide the pointer altogether? Yes. Regards, Malcolm
ok, I'm convinced. The semantics of empty datatypes can be a type inhabited only by bottom. Hugs implements exactly that. [Except in the special case of a few magical names (Int, Float, etc) when they occur in the Prelude (and only then). Since it is only usable in the Prelude, they can be treated as an internal detail and ignored.] -- Alastair
Malcolm Wallace <Malcolm.Wallace@cs.york.ac.uk> wrote,
data Point foreign import getMousePos :: Ptr Point -> IO () foreign import getX :: Ptr Point -> IO Int foreign import getY :: Ptr Point -> IO Int
vs
data Point = Point (Ptr Point) foreign import getMousePos :: Point -> IO ()
I like the second idiom. You are right that there is no need for the application programmer to know whether pointers are involved, because even in the first style, it is not possible to 'peek' inside a Ptr Point to get the `actual' Point value. So why not hide the pointer altogether? Yes.
From this, I infer that there is no dire need for empty data types in conjunction with the FFI. Consequently, I suggest that we do not include empty data types into the FFI spec (especially because the spec otherwise refrains from extending the base language in any way other than by foreign declarations).
Cheers, Manuel
participants (4)
-
Alastair Reid -
Malcolm Wallace -
Manuel M T Chakravarty -
Simon Marlow