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

Type synonyms #1865

Merged
merged 5 commits into from
Jun 1, 2024
Merged

Type synonyms #1865

merged 5 commits into from
Jun 1, 2024

Conversation

byorgey
Copy link
Member

@byorgey byorgey commented May 27, 2024

Adds type synonym declarations to the language, like so:

tydef Maybe a = Unit + a end
def lookdown : Cmd (Maybe Text) = scan down end

> lookdown
it2 : Maybe Text = inl ()

tydef behaves very similarly to def except that it defines a new (parameterized) type instead of a new term.

Note that higher-kinded types are not yet supported; for example we cannot say tydef Foo f = Unit + f Int (in fact this would be a syntax error since type variables cannot be at the head of an application). However there is nothing stopping us from adding that in the future; I just wanted to keep things simple for now.

If you know of any scenario code that would be a good candidate for using type synonyms, let me know --- it would be nice to update a few scenarios as a better stress test of type synonyms before merging this.

Closes #153.

@byorgey byorgey force-pushed the feature/type-synonyms branch from 7eb5f52 to d72bf4f Compare May 27, 2024 12:52
mergify bot pushed a commit that referenced this pull request May 28, 2024
Splitting out an independent refactoring to simplify #1865.  There were many places in the code where we were pattern-matching on `ProcessedTerm` and/or `Module`, sometimes only to extract a single field, *e.g.*
```
ProcessedTerm (Module s _) _ _ <- maybeInitialCode
```
This was already getting a bit out of hand, and it also meant that any time we wanted to add an extra field to either `ProcessedTerm` or `Module` (as I will be doing in #1865), we would have to change every single such place in the code to add an extra wildcard pattern.

This PR is a refactoring to
1. Derive lenses for all the fields of `ProcessedTerm` and `Module`, and
2. Prefer extracting named fields via lenses over pattern-matching in most places in the code.

There were a few places in the code where we destructure a `ProcessedTerm` and use almost all the fields (e.g. when initializing a robot machine); I left those alone, first because extracting all the individual fields would be tedious, but more importantly because if we ever added any new fields in the future, it's likely we would actually want to use them in those contexts as well.
@byorgey byorgey force-pushed the feature/type-synonyms branch from d72bf4f to d4c3e96 Compare May 28, 2024 10:56
mergify bot pushed a commit that referenced this pull request May 28, 2024
There were a bunch of fused-effects related utils that lived in a module in `swarm-scenario`; but all of them were completely generic except for the `simpleErrorHandle` function which is specific to `SystemFailure`.  So, this PR:
- Moves `simpleErrorHandle` to `Swarm.Game.Failure`
- Moves the rest of the module into the `swarm-util` package so it can be used elsewhere.

This is another refactoring in preparation for #1865.
mergify bot pushed a commit that referenced this pull request May 28, 2024
We used to represent types with a different constructor for each different sort of type, e.g. there was a constructor `TyFunF` which took two types as arguments, etc.  This refactoring creates a new type `TyCon` which has things like `TCFun` and `TCBase` and represents various types as an application of a `TyCon` to some arguments.  For example function type `t1 -> t2` would be represented no longer as `TyFunF t1 t2` but instead as `TyConApp TCFun [t1, t2]`.

This is slightly more roundabout, and it does make parsing slightly trickier, but it greatly simplifies and shortens code for e.g. unification, extracting free variables, etc. (because what used to be many essentially identical cases now turn into a single case).  It also paves the way for #1865, so we have a way to represent new type constructors defined by the user.  E.g. if the user defined `tydef Maybe a = Unit + a` then we would represent the type `Maybe Int` as something like `TyConApp (TCUser "Maybe") [TyBase BInt]`.

This also means that types like `Int Unit` are no longer a parse error, so we need kind checking to rule out applications of type constructors to the wrong number of arguments; this PR adds such kind checking as well.  Having some sort of kind checking is unavoidable when allowing the user to define their own new type constructors (with an arbitrary number of arguments).
@byorgey byorgey force-pushed the feature/type-synonyms branch 3 times, most recently from 4d5d738 to 1a4874a Compare June 1, 2024 14:29
@byorgey byorgey marked this pull request as ready for review June 1, 2024 14:29
@byorgey byorgey force-pushed the feature/type-synonyms branch from 1a4874a to 6d002f5 Compare June 1, 2024 14:45
@byorgey byorgey requested review from kostmo and nitinprakash96 June 1, 2024 14:46
@byorgey byorgey changed the title [WIP] Type synonyms Type synonyms Jun 1, 2024
@@ -1,4 +1,4 @@
syn keyword Keyword def end let in require
syn keyword Keyword def tydef end let in require
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wanted to update the vscode configuration as well but wasn't sure of the right way to do it --- @kostmo?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess it's here, but I'm not acquainted with the mechanics:

Copy link
Member Author

@byorgey byorgey Jun 1, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, OK, no worries, for some reason I thought you had created the VSCode configuration, but I see now I was misremembering. I'll create an issue for it: #1887 .

src/swarm-lang/Swarm/Language/Parser/Term.hs Outdated Show resolved Hide resolved
src/swarm-lang/Swarm/Language/Types.hs Outdated Show resolved Hide resolved
@byorgey byorgey added the merge me Trigger the merge process of the Pull request. label Jun 1, 2024
@mergify mergify bot merged commit 01c45ab into main Jun 1, 2024
11 checks passed
@mergify mergify bot deleted the feature/type-synonyms branch June 1, 2024 21:10
@byorgey byorgey added the CHANGELOG Once merged, this PR should be highlighted in the changelog for the next release. label Jun 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CHANGELOG Once merged, this PR should be highlighted in the changelog for the next release. merge me Trigger the merge process of the Pull request.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add type synonyms (or just generalize to System Fω)
2 participants