Records #1093
Assignees
Labels
C-Project
A larger project, more suitable for experienced contributors.
L-Language design
Issues relating to the overall design of the Swarm language.
L-Type inference
The process of inferring the type of a Swarm expression.
L-Type system
Issues related to the Swarm language type system.
S-Nice to have
The bug fix or feature would be nice but doesn't currently have much negative impact.
Z-Feature
A new feature to be added to the game.
Comments
byorgey
added
Z-Feature
|
Whatever the final implementation will be, I would love to have records as an end-game language feature. 😍 Bonus points for optics in Swarm. 😀 |
|
The device for giving record capability could be a |
Merged
mergify bot
pushed a commit
that referenced
this issue
Mar 25, 2023
Add record types to the language: record values are written like `[x = 3, y = "hi"]` and have types like `[x : int, y : text]`. Empty and singleton records are allowed. You can project a field out of a record using standard dot notation, like `r.x`. If things named e.g. `x` and `y` are in scope, you can also write e.g. `[x, y]` as a shorthand for `[x=x, y=y]`. Closes #1093 . #153 would make this even nicer to use. One reason this is significant is that record projection is our first language construct whose type cannot be inferred, because if we see something like `r.x` all we know about the type of `r` is that it is a record type with at least one field `x`, but we don't know how many other fields it might have. Without some complex stuff like row polymorphism we can't deal with that, so we just punt and throw an error saying that we can't infer the type of a projection. To make this usable we have to do a better job checking types, a la #99 . For example `def f : [x:int] -> int = \r. r.x end` would not have type checked before, since when checking the lambda we immediately switched into inference mode, and then encountered the record projection and threw up our hands. Now we work harder to push the given function type down into the lambda so that we are still in checking mode when we get to `r.x` which makes it work. But it is probably easy to write examples of other things where this doesn't work. Eventually we will want to fully implement #99 ; in the meantime one can always add a type annotation (#1164) on the record to get around this problem. Note, I was planning to add a `open e1 in e2` syntax, which would take a record expression `e1` and "open" it locally in `e2`, so all the fields would be in scope within `e2`. For example, if we had `r = [x = 3, y = 7]` then instead of writing `r.x + r.y` you could write `open r in x + y`. This would be especially useful for imports, as in `open import foo.sw in ...`. However, it turns out to be problematic: the only way to figure out the free variables in `open e1 in e2` is if you know the *type* of `e1`, so you know which names it binds in `e2`. (In all other cases, bound names can be determined statically from the *syntax*.) However, in our current codebase there is one place where we get the free variables of an untyped term: we decide at parse time whether definitions are recursive (and fill in a boolean to that effect) by checking whether the name of the thing being defined occurs free in its body. One idea might be to either fill in this boolean later, after typechecking, or simply compute it on the fly when it is needed; currently this is slightly problematic because we need the info about whether a definition is recursive when doing capability checking, which is currently independent of typechecking. I was also planning to add `export` keyword which creates a record with all names currently in scope --- this could be useful for creating modules. However, I realized that very often you don't really want *all* in-scope names, so it's not that useful to have `export`. Instead I added record punning so if you have several variables `x`, `y`, `z` in scope that you want to package into a record, you can just write `[x, y, z]` instead of `[x=x, y=y, z=z]`. Though it could still be rather annoying if you wanted to make a module with tons of useful functions and had to list them all in a record at the end... Originally I started adding records because I thought it would be a helpful way to organize modules and imports. However, that would require having records that contain fields with polymorphic types. I am not yet sure how that would play out. It would essentially allow encoding arbitrary higher-rank types, so it sounds kind of scary. In any case, I'm still glad I implemented records and I learned a lot, even if they can't be used for my original motivation. I can't think of a way to make a scenario that requires the use of records. Eventually once we have proper #94 we could make a scenario where you have to communicate with another robot and send it a value of some required type. That would be a cool way to test the use of other language features like lambdas, too.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Records were mentioned in #1087 as a way to represent imported modules. They would also be a cool, handy feature on their own. Records can make it very convenient to package and work with "objects". For example, compare:
However, records have one very big downside: inferring record types requires some fancy type system features such as e.g. subtyping and row polymorphism. A simple alternative could be to just give up on inferring record types and require type annotations (would probably require #10).
I do not know whether adding records would be worth it, or what the right tradeoffs would be if we did add them. For now, just adding this issue as a placeholder for discussion.
The text was updated successfully, but these errors were encountered: