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

Recursive types #1894

Merged
merged 8 commits into from
Jun 6, 2024
Merged

Recursive types #1894

merged 8 commits into from
Jun 6, 2024

Conversation

byorgey
Copy link
Member

@byorgey byorgey commented Jun 3, 2024

Implements recursive types. Example:

tydef List a = rec l. Unit + a * l end

def nil : List a = inl () end
def cons : a -> List a -> List a = \x. \l. inr (x, l) end

def foldr : (a -> b -> b) -> b -> List a -> b = \f. \z. \xs.
  case xs
    (\_. z)
    (\c. f (fst c) (foldr f z (snd c)))
end

def map : (a -> b) -> List a -> List b = \f.
  foldr (\y. cons (f y)) nil
end

As discussed at #154, this uses the syntax rec x. F(x) to define the type x which is a solution to x = F(x). However, unlike the discussion there, I ended up going with equirecursive types (so a recursive type is equal to its unfolding). For example, as you can see above, if we have a value of type List a (defined as rec l. Unit + a * l), then it actually has the equivalent type Unit + a * List a, so we can simply do a case on it, without having to unroll first. This actually turned out to be easier to implement (and it is cooler).

There are multiple built-in functions that conceptually return a list but currently do something different (like return a fold, or take an index and return a single element, etc.) We should consider changing them to actually return lists, but that should definitely be in a separate PR.

Closes #154.

@byorgey
Copy link
Member Author

byorgey commented Jun 3, 2024

I just realized I need to rule out types like rec t. t since any value may have that type, and it breaks type soundness. Should not be too hard to address, but in the meantime feel free to take a look at what's already in the PR and try it out.

@byorgey
Copy link
Member Author

byorgey commented Jun 3, 2024

@xsebek I wanted to see if I could entice you back with a juicy new language feature... 😉 (also there will be another Swarm swarm June 15th: #829)

@xsebek
Copy link
Member

xsebek commented Jun 4, 2024

@byorgey Ha, thanks, I will try this out! 👍

I noticed you needed the VSCode syntax updated and I see the rec keyword will also need to be added. 🙂

@byorgey byorgey force-pushed the feature/recursive-types branch from 6bdfcb4 to c448db6 Compare June 4, 2024 13:53
@byorgey byorgey marked this pull request as ready for review June 4, 2024 14:09
@byorgey byorgey added the CHANGELOG Once merged, this PR should be highlighted in the changelog for the next release. label Jun 4, 2024
@byorgey
Copy link
Member Author

byorgey commented Jun 4, 2024

This should be ready now. In theory we ought to have a device that provides the capability to use recursive types, but that will require some refactoring of the requirements analysis code so I opted to leave it for another PR: see #1898.

@@ -163,7 +163,7 @@ primitiveTypeNames = "Cmd" : baseTypeNames

-- | List of keywords built into the language.
keywords :: [Text]
keywords = T.words "let in def tydef end true false forall require requirements"
keywords = T.words "let in def tydef end true false forall require requirements rec"
Copy link
Collaborator

Choose a reason for hiding this comment

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

This should probably be followed up with updating the editor configurations (swarm-mode.el, swarm.vim etc)?

Copy link
Member Author

Choose a reason for hiding this comment

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

Good catch. I will update that shortly.

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 updated the emacs and vim configs to add a rec keyword. I was not sure how to update the vscode config (and it seems like @xsebek is in the middle of updating it anyway).

@byorgey byorgey force-pushed the feature/recursive-types branch from c448db6 to 1aec278 Compare June 6, 2024 14:14
@byorgey byorgey force-pushed the feature/recursive-types branch from 1aec278 to faeb898 Compare June 6, 2024 14:19
@byorgey byorgey added the merge me Trigger the merge process of the Pull request. label Jun 6, 2024
@mergify mergify bot merged commit de0d025 into main Jun 6, 2024
11 checks passed
@byorgey byorgey deleted the feature/recursive-types branch June 6, 2024 15:02
mergify bot pushed a commit that referenced this pull request Jun 6, 2024
Closes #1898.  Adds the `hyperloop` device (recipe: `ADT calculator` + `strange loop`) which provides the ability to use recursive types (#1894).  Also refactors requirements analysis code and adds the ability for types to trigger capability requirements.
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.

Recursive types
3 participants