Difference between "foreign import data Foo :: Type" and just "data Foo"

Question

Is there any functional difference between the titular approaches in defining a foreign type? The foreign import data Foo :: Type approach makes the intention clearer, but is that it?

Answer 1

Although they look similar on the surface, they are very different in terms of their representation in the meta language, as each will yield different constructs after parsing (ExternDataDeclaration for the former, DataDeclaration for the latter).

For example, you can derive instances of a data declaration but doing so for a foreign data declaration will throw an error.

-- This works
data Empty
derive instance eqEmpty :: Eq Empty
derive instance ordEmpty :: Ord Empty

-- This breaks
foreign import data Empty :: Type
derive instance eqEmpty :: Eq Empty

Error found:

  Cannot derive a type class instance, because the type declaration for Empty could not be found.

In the foreign case, you'll have to write these instances yourself.

I'm new to PureScript, so I'm unaware if there are other limitations that affect one and not the other. I'd say for all practical purposes they are identical.

Answer 2

In theory the two declarations have different meaning: data X has no inhabitants (so equivalent to Void) but import foreign data X :: Type has unknown inhabitants.

At the moment it doesn't matter much either way, but in the future it will as writing an empty case expression for an empty data type will be possible.