Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement ADT contracts #1821

Merged
merged 7 commits into from
Feb 19, 2024
Merged

Implement ADT contracts #1821

merged 7 commits into from
Feb 19, 2024

Conversation

yannham
Copy link
Member

@yannham yannham commented Feb 16, 2024

Depends on #1820

Several previous PRs (starting with #1770) introduced various stage of structural ADTs. A missing follow-up was that enum contracts weren't yet updated to handle the new enum variants. This PR implements correctly contracts for those new extended enums.

Content

  • refactoring: various type components (enum rows, record rows, etc.) had a similar method subcontract. As a first step, this PR refactors that into a proper trait (it's a bit orthogonal to the ADT contracts, and is more an incidental cleaning). Although the diff is a bit large, most of subcontract() methods have been left untouched and are just moving around - the only interesting changes are of course in the EnumRows::subcontract method.

  • refactoring: moving code around in internals.ncl to group internals by theme (record, enums, etc.). Same here: moderate diff, but actually very little new content, beside comments

  • Extend the translation of an enum type to a contract. As before, the translation relies on a match expression: [| 'Foo, 'Bar Contract; r |] is just translated as (the example is just written in a slightly higher level code than in reality)

    fun label value => value |> match {
      'Foo => value,
      'Bar arg => std.contract.apply Contract label arg,
      _ => $enum_tail value
    }
    |> $enum
    

    Where $enum is just a wrapper that checks that the value is an enum first.

Parametricity

As explained inside internals.ncl, the enum contracts don't enforce parametricity. The first reason is that it's not trivial to do, as we would need to let match expressions see through a sealed value but only if it ends up matching the catch-all case. Although annoying, this is doable.

The main reason is that the contract wasn't enforcing parametricity correctly before, and thus such a change would be backward incompatible. As an illustration that this isn't just a theoretical case (user code relying on enum contracts not enforcing parametricity): even in the standard library we are abusing enums, for example in std.string.from_enum: forall r. [|; r|] -> String. While forall r. [| ; r |] -> ... can look like a reasonable type for a function that takes any enum as a parameter, parametrictiy would enforce that such a function doesn't actually look into its argument. Thus, a parametric contract would make from_enum fail on valid input, which would require to change its contract, which means changing the stdlib interface.

@github-actions github-actions bot temporarily deployed to pull request February 16, 2024 16:33 Inactive
@yannham yannham mentioned this pull request Feb 16, 2024
@github-actions github-actions bot temporarily deployed to pull request February 16, 2024 16:57 Inactive
@yannham yannham requested review from vkleen and jneem February 16, 2024 18:26
core/stdlib/internals.ncl Outdated Show resolved Hide resolved
core/src/typ.rs Outdated Show resolved Hide resolved
@github-actions github-actions bot temporarily deployed to pull request February 19, 2024 14:36 Inactive
Base automatically changed from feat/full-pattern-matching to master February 19, 2024 16:50
Copy link

dpulls bot commented Feb 19, 2024

🎉 All dependencies have been resolved !

yannham and others added 6 commits February 19, 2024 18:02
Before the introduction of ADT, enum types couldn't contain other type
components. Now they can, as in e.g. `[| 'Foo (String -> Number) |]`.
The optimizer is updated to recurse into those types as well.
ADTs have been introduced (experimentally) in previous commits. In
practice, this means that the enum types have become more expressive,
where value can now be variant with an associated argument.

The contract derived from an enum type hasn't been updated yet, and
wasn't correctly handling more elaborate enums. This commit implements
the proper behavior for full enum types.

This commit doesn't change the previous status quo around polymorphic
enum types, in that it doesn't enforce parametricity at run-time. While
this is questionable, we are somehow stuck with this choice for now,
because suddenly enforcing parametricity would break
backward-compatibility, including the types of some functions from the
stdlib.
Since optimization has been introduced, eliding some contract
application for type annotations, it's safer to use contract annotation
in test whenever we really want to check the behavior of contracts at
run-time.

While this change shouldn't make any difference right now, it's probably
more future-proof, if further optimizations one day elide those
contracts.
@github-actions github-actions bot temporarily deployed to pull request February 19, 2024 17:08 Inactive
@yannham yannham added this pull request to the merge queue Feb 19, 2024
Merged via the queue into master with commit 8ab2c56 Feb 19, 2024
5 checks passed
@yannham yannham deleted the fix/adt-contract branch February 19, 2024 17:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants