Skip to content
This repository has been archived by the owner on Jan 27, 2024. It is now read-only.

Make a plan for how to handle product types #2

Open
seagreen opened this issue May 18, 2017 · 3 comments
Open

Make a plan for how to handle product types #2

seagreen opened this issue May 18, 2017 · 3 comments

Comments

@seagreen
Copy link
Owner

seagreen commented May 18, 2017

Currently product types act like PureScript row types where as long as the required fields exist it doesn't matter if there are other fields as well. See the implementation here. Is this actually what we want?

This issue is made additionally tricky by the goals of a schema system as opposed to a type system. As a schema system we'd like to be able to add additional, optional fields to a product type and still maintain backwards compatibility with old data. Is there a principled way to do this that won't cause us trouble in the future?

@no-longer-on-githu-b
Copy link

no-longer-on-githu-b commented May 20, 2017

If field names appear in the serialized data, you can tag schemas and serialized data with version numbers using semver. You can check statically that versions are backwards-compatible, and if they aren't, require a major verison bump. All the versions would remain in the schema.

foo#1.0 = {x :: Int}
foo#1.1 = {x :: Int, y :: Int}
foo#2.0 = {a :: Int}

If you have constrained types, such as Int where * >= 0, you can use an SMT solver like Z3 to check compatibility. For example, A where P(*) is backwards-compatible with B where Q(*) if A is backwards compatible with B and forall x. P(x) implies Q(x). But I don't know if Plate has this or if this is planned.


I have never actually implemented the compatibility checks but I don't see why it shouldn't work. It's analogous to subtyping where upcasts are coercions.

@seagreen seagreen changed the title Clarify the role of product types Make a plan for how we're going to handle product types May 20, 2017
@seagreen seagreen changed the title Make a plan for how we're going to handle product types Make a plan for how to handle product types May 20, 2017
@seagreen
Copy link
Owner Author

@rightfold: Field names will definitely appear in serialized data. My plan is to make Plate useful for describing meaningful-on-their-own formats like https://en.wikipedia.org/wiki/ICalendar, not to compete with Protocol Buffers-style formats that do very efficient serialization by dropping field names.

If field names appear in the serialized data, you can tag schemas and serialized data with version numbers using semver. You can check statically that versions are backwards-compatible, and if they aren't, require a major verison bump.

I think the simplest thing to do is to leave versioning out of the core of Plate. I really like the idea of doing static analysis on version compatibility though, once we get the core of Plate finished this would be a great tool to build.

@seagreen
Copy link
Owner Author

Also @rightfold your twitter comments are super relevant:

In PureScript, additional fields are only allowed if you explicitly allow them. You can't pass {x: 1, y: 2} to f :: {x :: Int} -> Int

You need to write f :: forall r. { x :: Int | r } -> Int

Maybe we should have each product type say explicitly whether it allows extra rows or not.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants