Feedback on region articles

[davidfstr]

Vale’s regions look interesting to me. So I read your series on regions. However I got tripped up by various inconsistencies, so here’s some feedback that hopefully will make these articles easier to read for others:

https://verdagon.dev/blog/zero-cost-borrowing-regions-part-1-immutable-borrowing

It then creates a raw reference 7 (without a generation) pointing to ship, and passes it to printShipNames.

Did you mean “myShips” instead of “ship”. The latter variable does not exist in code.

// Same function as before pure func printShipNames( tenShips &List<Ship> ) { foreach i in 0..tenShips.len() { ship = tenShips[i]; // Gen check here name = ship.name; // Gen check here println(name); } }

I don’t think there’s a gen check on the lines marked by the comments, since this is a pure function.

Or if there are gen checks, I’d like an explanation of:

1. how this version of “printShipNames” can be textually identical to the earlier version of “printShipNames” yet have gen checks in different places; and
2. how a gen check can be performed given that parameter “tenShips” is a raw reference.

pure func printShipNames<r'>( tenShips &r'List<r'Ship>) 13 my'{ foreach

Why is there a 13 in the middle of the code? Broken footnote reference?

• This article (and the whole region article series) says that regions are useful to avoid gen checks. It would probably be useful to link to instructions showing how to ask Vale where gen checks are (statically). Or link to how one can profile a Vale function (dynamically) to count the number of gen checks actually used in a block of code.

https://verdagon.dev/blog/zero-cost-borrowing-regions-part-2-isolates

An isolate is a hierarchy of data that nobody outside can point to, except for one owning reference outside that points at the root.

Could you add a diagram or picture showing this kind of constraint? I think more quickly in diagrams than text. I suspect others do too.

One would '-annotate only the parts of their program that profiling suggests would benefit from optimization.

This paragraph seems a good opportunity to link to instructions about how to profile Vale code.

We added <c'> after func fire so that the function can receive things in a read-only region, referred to as c.

Can this new “fire” function still receive a non-isolate “&Cannon” type rather than “&c’Cannon”? (Might be nice to mention the answer in the article text or as a footnote.)

In this example, reading anything from cannon is zero cost, because we used .imm to open the isolate immutably.

Does “.imm“ incur some kind of cost? If so, why? If so, how does that cost compare to the cost of a gen check? (Might be nice to mention the answer in the article text or as a footnote.)

The image.read in coalesceImage(&rand, image.read) will open up the image isolate as immutable

I thought “.imm” opened an isolate as immutable but “.read” is used here. Typo? If not, could you explain the difference between “.imm” and “.read”, and explain why the latter is being used here?

However, when a struct member is an isolate, it can only be accessed when: 13

The containing struct is destroyed first. 14 15 The containing struct is also an isolate. The containing struct is in an immutable region. We use a cell. — Could you put the word “or” before the “We use a cell” sentence to clarify that only one of the bulleted conditions needs to apply, rather than all of them?

A cell relaxes these restrictions

Which restrictions? The first three bullets?

For example, this Ship contains an "Engine cell". [example code]

It looks like the syntax for a cell looks like ‘’Engine, with double apostrophe. Could that be called out in the text explicitly if so?

foo uses the .read syntax to gain access to the contained 'Engine.

Actually it looks like “.imm” is used in this sample code rather than “.read”.

• Could you name the “foo” function something more descriptive, like “getEngineFuel”?

The above example did an immutable borrow using .imm.

It sounds like “.imm” differs from “.read” in that nobody is allowed to modify what the region points to so long as the .imm region exists. If so, would be worth clarifying that in contrast to .read.

In general “immutable” and “read-only” sound like the same thing, yet confusingly are different, so being careful to distinguish the difference early would be valuable.

When the CellGuard goes out of scope, will inform the original cell that we're done borrowing it.

Nit: Missing word “it” before “will”.

This is how the language enforces that we don't immutably borrow and readwrite borrow the cell at the same time, which protects us from memory problems.

Is “readwrite borrow” the same as “mutably borrow”? If so then recommend picking one or the other term to use and then use that term consistently.

With regionsthe compiler

Nit: Missing a space

We can hand a mutably-opened isolate

Presumably “mutably opened” means the same thing as “mutably borrowed”. Recommend picking one of those terms to use consistently.

We can completely contain a third-party library's code inside an isolate if we wanted to; isolates are very composable.

I didn’t see any examples of composing isolates. Maybe it would be useful to elaborate on compositional techniques in a different article.

https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3-one-way-isolation

&cannon became cannon.imm, which immutably borrows the iso's contents.

Does “iso” mean “isolate”? If so, recommend sticking with the latter term.

But there are a couple extra changes now, in Cannon and fire:

• cannon is now of type 'Cannon<main'> which […]

I don’t see 'Cannon<main'> anywhere in the example code…

As you can see, we're still able to isolate Cannon and open it immutably, even though it points to something outside its own isolated region.

I don’t actually see Cannon pointing to anything outside the main region. In particular I don’t see it pointing to anything inside the fire region. Could you clarify where such a reference to something inside the fire region is happening?

Part 4 shows how one object can contain another region's data inline

Sorry, as I just mentioned I didn’t see where Cannon was making a cross-region reference.

https://verdagon.dev/blog/zero-cost-borrowing-regions-part-4-multi-region-data

next priv vary ?^ShipListNode; 2

Why is there a “2” floating there? A broken footnote reference?

Also, could you explain what “priv” and “vary” mean, probably as a footnote?

We specify self' for the Ships to tell the compiler that they're in main's region.

“self’” does not appear in any of the example code… I only see “main’”.

set cur.hp -= 5; println("Damaged {cur.name}!");

“cur” has neither “hp” nor “name”. You probably meant “ship” instead.

That's all for now! We hope you enjoyed this article. Stay tuned for the next article, which shows how one-way isolation works.

One-way isolation is not the topic of the next article. That was the topic of this article.

https://verdagon.dev/blog/zero-cost-borrowing-regions-part-5-region-scoped-data

First, it takes the expression after in (here, list.iter()) and puts it in a local, iterable. (1)

The sample code says “list.imm”, not “list.iter()”

Here we're returning that cell guard.

There are no “return” statements in the example code shown here. Perhaps it is “list.iter()” that is returning the cell guard?

LinkedList.vale has a function which accepts that type:

What is “LinkedList.vale”? I don’t see it mentioned anywhere in the example code. Did you just mean “LinkedList”? Or maybe “The file ‘LinkedList.vale’”?

return LinkedListIter<x', T>(head); 3

Another number (3) just floating in the example code. A footnote?

array priv vary ''[]E;

Again, “priv” and “vary” could use some explanation, perhaps as a footnote.

That's all for now! We hope you enjoyed this article. Stay tuned for the next article, which shows how one-way isolation works.

I don’t think one-way isolation is the topic of the next article, since that was covered earlier.