`data MyType` vs `foreign import data MyType :: Type`

Chatroom Cross-posts
#1

artemisSystem
Is there a difference in how these work? Are there times where one of them fits better than the other?

data MyType
foreign import data MyType :: Type

natefaubion
Empty data is semantically a type that has no runtime representation (only type information). foreign import data is for things that have a representation (if any) that is opaque to the compiler.

natefaubion
This distinction is often blurred because it’s easy to just use unsafeCoerce

artemisSystem
Thanks!

natefaubion
foreign import data is really just unsafeCoerce for the type language.

natefaubion
My recommendation though is to use foreign import if you are dealing with foreign libraries.

wclr
I see that compile time both have no representation, but how the usage is different?

natefaubion
data Foo semantically says “this type cannot be represented by a runtime value” since it has no way to construct it, which is different than “this may or may not be represented by a runtime value which has a representation that is opaque to the compiler.” The compiler doesn’t do anything with this information currently, which is why people often treat it as the same thing.

natefaubion
One is saying “this can’t be used at runtime”, the other is saying “assume nothing”

wclr
But in terms of usage in the language currently they are the same?

natefaubion
The language does not currently treat them differently.

natefaubion
Well, that’s not entirely true, but for practical purposes they don’t do anything differently.

wclr
Ok, and what is the (practical) correct case for using just data MyType?

natefaubion
I really recommend foreign import however if you are representing opaque data, as it makes your intention much more clear.

natefaubion
Empty data is useful for type-level computation, since it essentially becomes a term constructor at the type level.

natefaubion
For example, you can use it to tag data types with extra type information, and enforce invariants that way.

natefaubion
It is not common, and I would consider it a very advanced feature.

5 Likes
#2

natefaubion
Empty data is useful for type-level computation, since it essentially becomes a term constructor at the type level.

natefaubion
For example, you can use it to tag data types with extra type information, and enforce invariants that way.

@natefaubion are TypeExpr construtors used across the typelevel-eval (like here or here) good examples of this approach?

1 Like