Records

[byorgey]

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.

[kostmo]

I enjoy the pun. I wonder, however, if there is an opportunity to distill more precisely the nature of records as a programming construct? Preferably still with puns. I kind of feel that the "audio" aspect of victrola stretches the analogy to the point of distraction.

For contrast, the convenience of records might be considered to be their "dot syntax". So perhaps the device that provides the capability for records is a dot? I feel like a pun on "dots" would better leverage familiar programming jargon as an inside joke. The recipe ingredients to construct a "dot" may entail a "finely-pointed instrument" or scribing utensil.

Or perhaps instead of a device named dot providing the capability, the dot-making utensil (yet to be named) is the device. And the "description" could craft the suggestion that "making dots" is the physical process of "making a record".

[kostmo]

Or, how about a quantum dot? Sounds sufficiently lofty for an end-game item?

[byorgey]

I still like victrola: it lets you "play (with) records". And "records" in the audio sense are actually a nice analogue for records in the programming sense: both let you store multiple pieces of data in one object. In contrast a dot lets you project out fields from a record, but why would it let you create records?

What if I just get rid of the description text that mentions "pressure waves through the air"? I agree it's probably distracting.

[byorgey]

the convenience of records might be considered to be their "dot syntax"

The convenience of records is the ability to put multiple pieces of data together into one, where the pieces of data are named instead of identified by position (as they would be with a normal product type). If you still don't like victrola, maybe we could consider something related to (name)tags? Just brainstorming here...

[kostmo]

I can live with it. Given that projection is nonetheless an integral operation to record usage, I wonder if we can still work quantum dot in somehow. How about as an ingredient to the victrola recipe?

Another consideration is generic vs. trademarked name of the record player. I take it that victrola has become a somewhat genericized brand name, as "kleenex" has become for facial tissues. There's a whole Wikipedia section on terminology, but if we want to aim for the least ambiguous, brand-neutral term for the device, maybe we would choose turntable.

[byorgey]

I wonder if we can still work quantum dot in somehow. How about as an ingredient to the victrola recipe?

Sounds fun to me. What should be the recipe for a quantum dot?

I take it that victrola has become a somewhat genericized brand name, as "kleenex" has become for facial tissues. There's a whole Wikipedia section on terminology, but if we want to aim for the least ambiguous, brand-neutral term for the device, maybe we would choose turntable.

Sure, I'm aware that victrola is a genericized brand name. Why would it be better to use an unambiguous, brand-neutral term? To me, victrola sounds a lot funnier than turntable.

[byorgey]

@kostmo I added a recipe for quantum dot (the Wikipedia page tells me one way to make quantum dots is with silicon with nonthermal plasma, which is created by passing an electric current through a gas; and the resulting quantum dots are often suspended in e.g. water; hence the recipe I came up with), and I added quantum dot to the victrola recipe and updated the description. Let me know what you think.

[kostmo]

Looks good.

[kostmo]

Reminds me of The Portable Phonograph from high school:

"I have been using thorns as needles," he said. "But tonight, because we have a musician
among us" - he bent his head to the young man, almost invisible in the shadow - "I will use
a steel needle. There are only three left."

The two middle-aged men stared at him in speechless adoration. The one with the big
hands, who wanted to write, moved his lips, but the whisper was not audible.

"Oh, don't," cried the young man, as if he were hurt. "The thorns will do beautifully."

"No," the old man said. "I have become accustomed to the thorns, but they are not really
good. For you, my young friend, we will have good music tonight."

"After all," he added generously, and beginning to wind the phonograph, which creaked,
"they can’t last forever."

[byorgey]

I wasn't familiar with that story, thanks for the reference! I just went and read the whole thing. I wonder if we could somehow stick a reference to the story into the description...

[byorgey]

How come this got merged even though the checks failed!? I assumed putting an XXX in would mean it wouldn't get merged yet.

[byorgey]

Oh, I see, our mergify configuration only specifies that the 8.7, 9.0, and 9.2 builds have to succeed! So currently the TODO check or the 9.4 build could fail and it would still merge. Whoops.

[kostmo]

Should be T.unwords?

[byorgey]

Yes, it should! See, this is exactly why I didn't want to merge it yet - I wanted you to look at the new code first!