Dhall-lang: Versioning scheme and release process for the language standard

[f-f]

Moving over here from the conversation on #141.

Basically there it's being proposed that:

1. we adopt a versioning scheme for the language (to signal breakage)
2. and a release process for the specification independent of the release process for the Haskell implementation

I would add that this is probably not super urgent until there is another complete and independent implementation of the language. However, it's worth thinking this through already.

An important aspect is "how to detect breakage". I think there is 3 types of changes; changes can:

1. not break semantics
2. accidentally break semantics
3. voluntarily break semantics

If we go by SemVer, we know that option 1 is a minor version bump, and option 3 is a major version. Option 2 is also a major version, but we need a way to find out.

I have the feeling that given an ABNF we cannot prove that by changing something we don't change some "relevant output", because defining "relevant" would mean sticking to a concrete implementation. (e.g. is "whitespace" removal considered breaking?)

A more practical approach (and imperfect implementation of the paragraph above) would be to say:

"we generate a parser from the ABNF (for example with this) and we run the same tests of the Haskell reference implementation"

In this way when a test breaks, we need a new major version. If making a change doesn't break tests that's a minor version. Every bugfix should ship more regression tests (which we already do), so there's as less accidental breakage as possible.
In this way, if a language case is not covered by enough tests, it should be considered correspondingly unstable. (I'm not sure how to define this "instabiliy" though)

This kind of behaviour is also what they adopt in the Matrix spec, which looks to me like a better specified SemVer.
Relevant quote:

The specification for each API is versioned in the form rX.Y.Z.

• A change to X reflects a breaking change: a client implemented against r1.0.0 may need changes to work with a server which supports (only) r2.0.0.
• A change to Y represents a change which is backwards-compatible for existing clients, but not necessarily existing servers: a client implemented against r1.1.0 will work without changes against a server which supports r1.2.0; but a client which requires r1.2.0 may not work correctly with a server which implements only r1.1.0.
• A change to Z represents a change which is backwards-compatible on both sides. Typically this implies a clarification to the specification, rather than a change which must be implemented.

Another interesting point is: should the versioning scheme of the implementations follow the versioning scheme of the language? Something like this could work, but might confuse some package managers: LangMajor.LangMinor.ClientMajor.ClientMinor.

/cc @Gabriel439 @ocharles

[Gabriel439]

I'll propose that the release process should be just creating a tag (i.e. what GitHub calls a release).

In terms of release frequency, we can use roughly the same process as the Haskell repository does:

• Anybody can cut a release if:
  
  
  
  • ... there is an unreleased change at least 1 month old,
  
  
  • ... and no unreleased changes fewer than 3 days old.
  
  
  • The goal is to encourage releasing early and often and to give anybody permission to cut a release
  
  
  • This includes people without the "commit bit". They should be able to request that somebody cut a release on their behalf
  
  
  • This implies that the master branch of the specification should always be "release-ready"
  
  
• Cutting a release earlier than that requires opening an issue against this repository
  
  
  
  • Acceptance criteria are: minimum review period of 3 days without any objections
  
  

As far as detecting breaking changes, I think the best we can do is "best effort". Specifically, we make sure that there is a sufficiently large conformance test suite and also reason through the potential breakage of changes we introduce. If we unintentionally release a breaking change as a minor version then we just release a new major version and update the old release to reflect that it is a bad release (such as by updating the description).

For breaking change I think we can actually formally specify what it means. The contract for a non-breaking change is that any code that parsed/resolved/type-checked/normalized successfully before must continue to do so (modulo imported resources changing). Carefully note that this does not include pretty-printing or formatting the code.

I don't think we should assign any rating of the stability of features. The only statuses for a feature are "proposed", "merged", and "released". If we don't think a proposal is sufficiently mature then we don't merge it. The standard I've applied so far for non-trivial is that there needs to be a proof-of-concept implementation as a sanity check and changes to the type system need to have an informal proof sketch of the following four soundness rules:

• Type-inference won't diverge
• If an expression type-checks, normalizing that expression won't diverge
• Normalizing an inferred type won't diverge
• Normalizing an expression doesn't change its type

I also think that it's not correct to think of the implementation as the "client" of the specification. The true client in my opinion is Dhall code, not the interpreter.

A given release of an interpreter can only sensibly support exactly one version of the language specification. For example: what would it mean for an implementation to support the specification before and after the change to the grammar of Natural numbers? If you gave it a file like:

2 : Natural

... the interpreter wouldn't be able to say for sure whether or not the expression type-checks if it is supporting multiple versions of the language specification.

Even for non-breaking changes it still doesn't make sense to support multiple versions: either you support the language feature or you don't and the set of language features you do support uniquely determines the version of the language specification that you correspond to.

On the other hand, it does make sense for Dhall code to be compatible with a range of language specifications so we should treat that as the client for the purposes of reasoning about the language specification version.

If you think of the Dhall code as the client, then if we go with the Matrix spec that would imply that:

• A change to "X" reflects a backwards-incompatible change to the specification
• A change to "Y" reflects a new language feature
  
  
  
  • ... since any Dhall code that depends on that language feature is incompatible with older specifications
  
  
• A change to "Z" is basically semantics-preserving refactors of the specification
  
  
  
  • i.e. documentation/whitespace changes or renaming terminals in the grammar, etc.
  
  

Going back to versioning implementations, I also think each implementation should use the versioning scheme appropriate for their language since each language imposes unique constraints on what versions mean (such as PVP for Haskell). The only requirements we should impose on the version of the interpreter are:

• every release of the interpreter must explicitly declare which version of the language specification it supports
• if the supported language specification undergoes a breaking change then so should the interpreter
  
  
  
  • ... using whatever mechanism is appropriate to that interpreter/language to signal breaking change
  
  

[f-f]

I'll propose that the release process should be just creating a tag (i.e. what GitHub calls a release).

+1

In terms of release frequency, we can use roughly the same process as the Haskell repository does

+1 and this should go in a CONTRIBUTING.md

For breaking change I think we can actually formally specify what it means. The contract for a non-breaking change is that any code that parsed/resolved/type-checked/normalized successfully before must continue to do so (modulo imported resources changing). Carefully note that this does not include pretty-printing or formatting the code.

I like this. Should we then run the tests and match with golden-tests the AST of the normalized forms? And how should we go for the α and β normalizations defined in the semantics document? Can we run tests against that specification?

I also think that it's not correct to think of the implementation as the "client" of the specification. The true client in my opinion is Dhall code, not the interpreter.

Right, I didn't specify that properly, I agree with this.

I also think each implementation should use the versioning scheme appropriate for their language since each language imposes unique constraints on what versions mean (such as PVP for Haskell)

Yes, I had PVP in mind when I said that package managers would get confused. This is good.

[f-f]

I just realized something we didn't consider, so I'll leave this here: the Prelude should be versioned with the same release number as the language standard.

[f-f]

This said, I'd say we could go ahead with the semantics defined by @Gabriel439 some comments ago - in https://github.com/dhall-lang/dhall-lang/issues/145#issuecomment-387606748.

To make this happen I think we'd need to:

• make a VERSIONING.md in which we define the semantics of how we version (basically the content of that comment)
• tag the 1.0.0 after merging that commit
• tag the same version in the Prelude repo

Questions:

1. Did I miss anything?
2. Should we instead wait for the formalization of something before releasing 1.0.0?

[Gabriel439]

I think we shouldn't wait for the formalization to be done and we should go ahead and start versioning things. We'll need to exercise the versioning process early and often anyway to test drive it

[f-f]

Awesome, I'll put together a PR for this :)