Rethinking data kinds and foreign import data

@timjs

Summary

The foreign import data declaration is sometimes awkward, difficult to explain and use correctly, and unnecessarily increases the "size" of the PureScript language. By improving support for data kinds, we may be able to deprecate and remove it.

Motivation

The objections I have to the current foreign import data syntax mostly fit into two buckets:

It diverges from data syntactically in a way that's perhaps not really necessary
The semantic difference between foreign import data and data is kind of unclear

So let's start with the syntax. It diverges awkwardly from data, as @timjs noted in https://discourse.purescript.org/t/thoughts-on-future-additions-of-type-level-features/707/9:

There is some strange separation between what you can define using a normal data declaration on one hand and using foreign data declarations:
foreign import kind Nat
foreign import data Z :: Nat  -- Ok
foreign import data S (n :: Nat) :: Nat  -- Syntax error!

data Z :: Nat  -- Syntax error!
data S (n :: Nat)  -- Ok
The usage of import foreign kind/data declarations is a bit clumsy in my view. Why not stripping the import foreign, add a kind keyword and allow empty data declarations with kind annotations?

I think at the moment, we more or less have

<foreignImportData> ::=
  'foreign' 'import' 'data' <typename> '::' <kind>

versus

<dataParam> ::=
  <identifier> | '(' <identifier> '::' <kind> ')'
<data> ::=
  [ 'data' <typename> '::' <kind> '\n' ]
  'data' <typename> <dataParam>*
  [ '=' <constructors> ]

This complicates the language syntax and by extension all tools which deal with the syntax, and (perhaps more importantly) it complicates the task of teaching people the syntax.

One concrete example where this pops up is in generated documentation. At the moment, the difference between a foreign import data and a data is mostly just an issue for the author of the module (this claim is slightly dodgy, more on this later), and should be irrelevant to any downstream consumers of the module, which suggests that they should look the same in generated documentation. However, at the moment, they look very different: in particular in that the parameters of a data type can be given names, whereas those of a foreign import data type cannot. This becomes especially awkward in cases such as #4116, where we were planning to add subscripts to type parameters in generated documentation to indicate their roles, but this is problematic for foreign import data since the syntax does not permit naming the type parameters.

As for semantics: the idea is currently that:

data is for types of kind Type (i.e. those which can have runtime representations), where the compiler knows what the type's runtime representation is, because the valid runtime representations for a data type are precisely its constructors
foreign import data is for when the type is of some kind other than Type after receiving its parameters, or when the type's runtime representation is opaque to the compiler

See also https://discourse.purescript.org/t/data-mytype-vs-foreign-import-data-mytype-type/2203. This is why data only allows declaring types of kind Type, and why foreign import data does not allow adding data constructors. The proposal in #2922, where case expressions with no branches would be permitted if a data type has no constructors, also depends on this view, because the compiler would need to be able to assume that such types are uninhabited.

I have two problems with this. Firstly, this division seems kind of arbitrary to me; it's not really clear to me why these two cases need to be separated into different declarations. Secondly, for the entire lifetime of foreign import data so far, there has been no actual difference in how the compiler treats foreign import data from data with no constructors, and the difference was not clearly documented anywhere until that Discourse thread (March last year), and even now that's a sort-of-unofficial location (compared to, say, the purescript/documentation repo). This means that it is very likely that there are cases in the wild where data is being used where it should technically be foreign import data, or vice versa, which makes it difficult to justify changing the compiler to start making stronger assumptions at this stage.

In my view, it's rare enough to want uninhabited types, and we already have Void in a library, so I don't think the compiler needs special support for uninhabited types. In particular, I think having the question of "is this type uninhabited" implicitly become part of a data type's public API kind of sucks. As I said in #2922 (comment):

adding a constructor to a previously empty data type becomes a breaking change if you can write downstream code which made use of the fact that the type previously had no constructors, even if you don’t export the new constructor.

The last awkward corner is data kinds. Just as it's useful to be able to write, eg, data Nat = Zero | Succ Nat to say that every Nat is either a Zero or the Succ of some other Nat at the term level, it's also useful to be able to express that there should be a kind Nat and types Zero :: Nat and Succ :: Nat -> Nat, and that at the type level, every Nat is either a Zero or a Succ. This isn't currently possible in PureScript; you have to write

data Nat {- or alternatively `foreign import data Nat :: Type` -}
foreign import data Zero :: Nat
foreign import data Succ :: Nat -> Nat

which is less than ideal because there's nothing stopping someone else from coming along later and writing some nonsense like this in a different module:

foreign import data Negate :: Nat -> Nat

The question of "how often do we want open vs closed data kinds" is a good one. It appears to me that GHC only has closed data kinds right now, and an issue for open data kinds has sat open for quite a long time, so it appears that they are not in a lot of demand.

Proposal

Permit data to supplant foreign import data by:

Figuring out a syntax for allowing data constructors to exist at the type level, so that I can write e.g.

data Nat = Zero | Succ Nat
type Three :: Nat
type Three = 'Succ ('Succ ('Succ 'Zero))

Saying that you can't make any assumptions about the runtime representation of a data type with no constructors, and if you want to make a type observably uninhabited then you should either make it a newtype of Void and export the constructor, or provide your own absurd-like function forall a. MyType -> a. (In this case we would close Allow case expressions without branches #2922 as "won't implement".)

If we do this, then I think we may be able to deprecate and possibly eventually remove foreign import data. The only remaining case I am aware of where it would be useful is for open data kinds, but I don't know if this is an important enough feature to justify the learning and maintenance costs.

Of course, "figuring out a syntax for data kinds" is maybe doing a bit of heavy lifting. But I think it may be worth discussing this approach first before we try to figure out a syntax for data kinds.

Examples

-- Uninhabited data types
-- note, this is currently allowed
newtype MyVoid = MyVoid Void
-- alternatively,
data MyVoid
myAbsurd :: forall a. MyVoid -> a
myAbsurd = unsafeCoerce

-- Types with opaque runtime representation
-- note, this is currently allowed
data Effect :: Type -> Type
data Effect a

-- Data kinds
data Nat = Zero | Succ Nat
type Three :: Nat
-- This is the only part that isn't currently allowed
type Three = 'Succ ('Succ ('Succ 'Zero))

One thing to consider is that foreign import data is useful as a type-level "I know what I'm doing". For example, foreign import data Any :: forall a. a.

To clarify why that might be useful, you should be able to write polykinded type-families with typelevel-eval.

I think if we can have the compiler take the view that empty data declarations for types with opaque representations are fine, and if we can add better support for data kinds so that foreign import data is only really needed as a type-level "I know what I'm doing", then I would consider these concerns addressed. If we can relegate foreign import data to just being a type-level version of unsafeCoerce, then that's much easier to explain and it's also much easier to justify ignoring until people reach an advanced level. I think it's also useful in that the presence of foreign import data would be a stronger signal of potential shenanigans.

Could the non-data-kinds issues be cleared up with a less powerful reform?

Admittedly, I'm coming at this from the other side of the argument in #2922; I think there is value in differentiating between ‘uninhabited’ and ‘mysteriously inhabited’, and while I concede that I could wrap Data.Void in newtypes and get all the same benefits (as long as the compiler has some special-case handling of Data.Void), I think that'd be about as unnatural as making everyone's proxy-like types be newtype wrappers of Unit.

But anyway, what if we presented the following unified syntax:

<dataParam> ::=
  <identifier> | '(' <identifier> '::' <kind> ')'
<dataSig> ::=
  'data' <typename> '::' <kind>
<dataBody> ::=
  ε | '=' <constructors> | '=' 'foreign'
<dataDecl> ::=
  'data' <typename> <dataParam>* <dataBody>
<data> ::=
  <dataSig> |
  <dataDecl> |
  <dataSig> '\n' <dataDecl>

With the semantics:

A dataSig with no dataDecl is uninhabited.
A dataDecl with an empty dataBody is uninhabited.
Roles may not be defined on uninhabited types (you can't coerce them if they can't exist!).
The ‘final kind’ (after filling all type parameters) of a dataDecl with a non-empty dataBody must be Type. It is an error to provide such a dataDecl with an incompatible dataSig.
The foreign keyword indicates a type that cannot be constructed or destructed from within PureScript, but which may have roles and must have final kind Type.

So, examples:

-- Uninhabited data types
-- note, this is currently allowed
data MyVoid

-- Types with opaque runtime representation
-- this syntax is not currently a thing, obviously
data Effect :: Type -> Type -- this signature is optional
data Effect a = foreign

-- Data kinds
data Nat
data Zero :: Nat
data Succ :: Nat -> Nat
-- these are all uninhabited; this is, IMO, an advantage of this scheme over
-- data kind promotion, as no unused constructors need to be generated

type Three :: Nat
type Three = Succ (Succ (Succ Zero))

This addresses the syntax divergence. The documentation issue is resolved by forbidding roles on uninhabited types; if you need roles, you already have to have a dataDecl that uses dataParams, and we can annotate those. The data kinds story remains largely the same as it is but with less foreign import noise, and hopefully it's easier to explain due to the unified syntax. This doesn't eliminate the distinction between uninhabited and foreign types, but that's how I like it! And obviously this has a much smaller scope than implementing data kind promotion, which might be a nice thing to have anyway but I don't see a need to couple that to this.

The other thing you identified as an issue is some joker defining data Negate :: Nat -> Nat, which this proposal doesn't address at all; my data kinds are as open as the existing foreign import data ones. But I might need a little bit more context to see why that's a problem we ought to solve. Our only mechanism for ‘matching’ at the type level is class instance resolution, so if that joker declares appropriate instances for Negate, they get either a working system extended to negative numbers, or what they deserve if they did it wrong; and if they don't declare instances, attempts to use Negate with any existing Nat machinery will fail. I'm not saying that open kinds are in any way superior to closed kinds, but I will say that there is alignment at the value level between our naturally-closed data types and the naturally-closed case expressions that deconstruct them, and also alignment at the type level between our naturally-open kind shenanigans and the naturally-open world of type classes and instances, and I'm a little leery of messing with that alignment without a strong reason to.

Roles may not be defined on uninhabited types (you can't coerce them if they can't exist!)

I’m not sure this works - consider:

data Void1 a

coerce (Nothing :: Maybe (Void1 a)) :: Maybe (Void1 b)

To solve this, I have to know Void1’s parameter’s role - if it is nominal, this should fail; if it is representational, then we should incur a Coercible a b subgoal; and if it is phantom, then this should work. We still have to deal with coercions, despite the fact that Void1 a is uninhabited for any choice of a.

I think distinguishing uninhabited from foreign becomes much easier to justify if the compiler is going to treat them differently, but I just can’t really see how we’d end up ever wanting to do that (other than perhaps #2922, which you can probably tell I’m not keen on anyway). I don’t find the “it would be as unnatural as having everyone’s proxy-like types being wrappers of Unit” argument that convincing, personally, because now that we have polykinds we don’t need - and preferably shouldn’t have - a litany of proxy types. Just the one should do! I think the newtype wrapper for Void approach makes sense because it makes it significantly easier to get the instances you need via newtype deriving (even if all of the implementations are eventually just absurd), and the only reason I can think of for not just using Void is because you want some additional type class instances, in which case it’s useful to not have to write out all the existing ones again.

I agree with the point about how kinds being naturally-open aligns well with type classes being naturally-open; based on experience so far it does seem like that we can probably do without closed data kinds.

data Void1 a

Is there any reason ever to give a a role other than phantom? I thought about it and tentatively concluded that there isn't one, but my justification is a little flimsy maybe. Coercible only gets involved if some value is being passed around, so since there can't be Void1 values, there must be some carrier—Maybe in your example—and that carrier should decide how valid its values are when interpreted as other types. The carrier must be a sum type (eventually; maybe the carrier itself has a carrier, but if it's products all the way down, there's still no value to coerce), and the values that can be coerced if one of the type parameters is filled with an uninhabited type must come from constructors in the sum that don't use that type parameter. If the interpretation of values thus constructed depends on the type parameter anyway, that type parameter should have a nominal role, and the role of a in Void1 is irrelevant. Otherwise, and if the carrier's type parameter doesn't have some other reason to be nominal, it is safe for the presence of Void1 not to prevent a coercion, which makes the phantom role correct for a. (Does this argument generalize to foreign carriers? I don't think so but I have a hunch that the conclusion is valid anyway.)

We may just have irreconcilable opinions about the #2922-adjacent parts of all this. I will say that, while polykinds removes the need for many of the proxies we've accumulated, there may still be times you want a Proxy (or likewise a Void1) with a more restrictive kind to aid in type inference or to make errors more comprehensible; and there is still a need for higher-order Proxy2, Proxy3, etc. (likewise Void2, Void3, etc.) for singly-inhabited (resp. uninhabited) types which accept more than one type argument. I agree that deriving newtype instances can be a compelling reason to use newtypes for those types, when needed. But newtypes or not, I still maintain that omitting vacuous cases entirely can offer a notable ergonomic benefit over using absurd, when the types get complicated.

I can’t think of a reason to give Void1 a role other than phantom off the top of my head, but I don’t find the argument that persuasive - maybe your carrier type is defined in an upstream library and you don’t get to say what you want its roles to be, so being allowed to specify the roles for your Void1 allows you to avoid having to reimplement a version of the carrier type with the roles you want?

However, I’m more coming from the point of view of not wanting to unnecessarily complicate the system by adding additional rules such as “uninhabited types can’t have roles”. I think the system is simpler and easier to understand overall if all types can have roles, and also that’s what the paper says, and if the only reason to disallow them is that it makes generating docs easier then I think the tail is wagging the dog at that point. I’d rather generate parameter names in the docs in the cases where we don’t have them than impose a rule that uninhabited types can’t have roles.

Okay, okay, we don't have to have that rule then! I don't think my proposal changes much without it. We can let people do whatever they want with roles and generate parameter names in the, I think we agree at least very rare, cases that we'll want them and they aren't provided.

I like your proposal otherwise, although I'm a bit reticent to add syntax like data Effect a = foreign when you can already express that with what we have in the language already - namely, newtype Effect a = Effect Foreign.

As a principle, do you prefer having primitive types that the compiler treats specially (which is what Foreign would have to be if we didn't have foreign import data Foreign or data Foreign = foreign syntax features, right?) over general syntactic features that can be used to implement those types? It's complexity for the compiler either way, and I don't know if I feel strongly that one is preferable to the other, but there's probably some advantage to consistently ruling in one direction. (That is to say, if we deprecate the foreign keyword in favor of a unique primitive Foreign type, I'm that much more likely to be on board with deprecating empty data declarations in favor of a unique primitive Void type.)

This also makes me think of Haskell with only one typeclass, if we want to go even further in the direction of fewer syntactic features. (I fear this is not a remotely practical thing to propose at this point, but maybe it's enlightening for other reasons?)

I also don't feel strongly that one is preferable to the other; in this case I think I'm trying to take a more pragmatic approach of considering where the language is at the moment, and how we can improve it without causing undue fuss for people who rely on existing code. For example, a large part of the reason I am leaning towards having people write newtype Effect = Effect Foreign rather than introducing a new data Effect a = foreign syntactic construct is that you can already do the former; a Foreign data type already exists in the purescript-foreign library. (I suppose that if we were going to go ahead with this approach we might want to move Foreign into a submodule of Prim, but that can be done in a non-breaking way).

I'm not concerned with complexity inside the compiler here, rather complexity for downstream tools - particuarly those which deal with the language syntax - and complexity for documentation and learning resources. I agree that the complexity inside the compiler is probably similar across all of the proposals in this thread.

I'm not concerned with complexity inside the compiler here, rather complexity for downstream tools - particuarly those which deal with the language syntax - and complexity for documentation and learning resources.

I think this is a really compelling argument, actually. To restate mostly for my own benefit, primitive types are part of the interface between users and the compiler, whereas syntax features interface with both of those and other tools in the ecosystem, which means syntax features add more coupling and slow the project down more than primitive types.

One more very minor concern about newtyping Foreign: in order to use those newtypes the same way that foreign data is used now, we have to guarantee that the runtime representation of a newtype is always the same as of the underlying type, across all backends. Either that, or all the foreign imports will have to become foreign import foo :: Foreign -> (Foreign -> Foreign) -> Foreign -> Foreign, which I don't think we want. We do already say we do that in the documentation for newtypes, but the documentation seems to assume the JavaScript backend. Are we prepared to commit to that guarantee in every backend? (I think yes, but seems like it's worth explicitly thinking about at least for a moment.)

we have to guarantee that the runtime representation of a newtype is always the same as of the underlying type

I would consider this a hard language guarantee as-is.

Yep, I think the newtype runtime representation guarantee is already present across all backends, because features like derive newtype and Coercible already rely on it.

I buy it.

In that case, my proposal seems like it boils down to just deprecating the foreign import in foreign import data declarations. 😁 Radical!

(Well, that and relocating Foreign.Foreign to Prim.Foreign.)

I'll mark this as a breaking change. When would we want to implement this change?

We should probably have a major version where we accept standalone data signatures and warn on foreign import data, like what we're currently doing with foreign import kind?

Ah... True.

@garyb

So to clarify, we currently write this:

-- This type can have values (rather than something
-- like `Void`) but the compiler has no idea what
-- its runtime representation is
foreign import data MysteriouslyInhabitedType :: Type -> Type

foreign import doStuffWithMIT :: forall a.
  a -> MysteriouslyInhabitedType -> String

data TypeOnlyNoValues :: forall k. (k -> Type) -> Type -> Type
data TypeOnlyNoValues f a

After this proposed change, we would write this?

-- This type can have values (rather than something
-- like `Void`) but the compiler has no idea what
-- its runtime representation is as represented
-- by the `Foreign` type
newtype MysteriouslyInhabitedType :: Type -> Type
newtype MysteriouslyInhabitedType a = MIT Prim.Foreign

-- While the `foreign import data` syntax would 
-- be deprecated and then later removed,
-- the syntax for FFI functions,
-- `foreign import functionName`, will be unchanged.
foreign import doStuffWithMIT :: forall a.
  a -> MysteriouslyInhabitedType -> String

data TypeOnlyNoValues :: forall k. (k -> Type) -> Type -> Type
data TypeOnlyNoValues f a -- Note: this line is optional

There's been times I've heard @garyb mention his desire to redo Foreign. I can't recall (or perhaps never fully understood) the full reasons for that, but would that need to be done first or alongside of this change?

Yes, and the data TypeOnlyNoValues f a line is optional, but not deprecated.

@JordanMartinez

@JordanMartinez It's not so much I want to redo Foreign, it's that I don't think the current library should exist, or perhaps not in core at least.

it only works for JavaScript, and I don't think a general purpose foreign library is even possible
it's not very good, it doesn't really do much aside from parsing/validating JS values

Even if it was better (could construct objects, call methods, etc.) and people did actually use it to implement functionality against the FFI, it'd make those libraries less portable. It would basically be writing JavaScript in PureScript, whereas when implementations are on the other side of the FFI barrier it leaves more room for the possibility of alternate backend compatibility.

Also, I'm not really sure it can be made better in a way that is useful - it'd either have to all be in Effect with the possibility of throwing exceptions - inconvenient if you know that something an operation doesn't need to be effectful - or it'd be unsafe, at which point you may as well write it in the FFI anyway.

edit: I'm not against having a Foreign in Prim though, I just don't think there should be a library that performs operations on Foreign.

Gotcha. Thanks for clarifying. It sounds like purescript-foreign as a library should be dropped and reappear as purescript-javascript. The library would be moved from core into the contrib libraries (as I don't know where else it would go).

I’d prefer to leave foreign as-is but possibly move it to contrib. There’s a bunch of code which depends on it and I personally don’t consider these flaws serious enough to justify breaking things. For example: I suspect a big chunk of PureScript users only care about the JS backend, which means that non-portability is a non-issue for them.

For example: I suspect a big chunk of PureScript users only care about the JS backend, which means that non-portability is a non-issue for them.

I'm sure that's true - it's pretty much true for me - but i think it's enormously impressive that PureScript can have and actually does have other backends and i think you shouldn't hide that from people who are just going to think the whole world is JavaScript, now and forever.

I mean, TBC i'm not saying you are hiding it, just that i think it's something that i personally would not like to see hidden or deprecated over time.

I completely agree; please don’t read my previous comment as an intention to deprecate other backends. :)

Sunbelt Computer Software

PL/B Language Development and Support

Navigation Menu

Repository navigation

Rethinking data kinds and `foreign import data` #4127

Summary

Motivation

Proposal

Examples

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Sunbelt Computer Software

PL/B Language Development and Support

Rethinking data kinds and foreign import data #4127

Description

Summary

Motivation

Proposal

Examples

Activity

natefaubion commented on Jun 28, 2021

natefaubion commented on Jun 28, 2021

hdgarrood commented on Jun 28, 2021

rhendric commented on Jun 29, 2021

hdgarrood commented on Jun 29, 2021

rhendric commented on Jun 29, 2021

hdgarrood commented on Jun 29, 2021

rhendric commented on Jun 29, 2021

hdgarrood commented on Jun 29, 2021

rhendric commented on Jun 29, 2021

hdgarrood commented on Jun 30, 2021

rhendric commented on Jun 30, 2021

natefaubion commented on Jun 30, 2021

hdgarrood commented on Jun 30, 2021

rhendric commented on Jun 30, 2021

JordanMartinez commented on Jul 2, 2021

rhendric commented on Jul 2, 2021

JordanMartinez commented on Jul 2, 2021

JordanMartinez commented on Jul 2, 2021

rhendric commented on Jul 2, 2021

garyb commented on Jul 3, 2021

JordanMartinez commented on Jul 3, 2021

hdgarrood commented on Jul 3, 2021

afcondon commented on Jul 4, 2021

hdgarrood commented on Jul 4, 2021

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Rethinking data kinds and `foreign import data` #4127