Pointers and heap assignment (concept discussion)

[MattWindsor91]

Since GRASShopper is now an integral part of the Starling story, I feel like it's time to consider first-class support for pointers and heap assignment. This would allow us to:

• more strongly check these operations in Starling to avoid errors propagating all the way to GRASShopper;
• make it easier to re-use heap proofs with other backends in future;
• make it easier to explain Starling's heap capabilities to other people, e.g. without having to talk about symbolics or GRASShopper in general.

I'll probably propose some syntax in a bit, but I thought I'd get the discussion open.

[MattWindsor91]

Quick syntax sketch for heap assignment:

<| *PVALUE = EXPR; |>
<| LVALUE = *PVALUE; |>

where PVALUE is an lvalue of pointer type. (We'd have to add pointer types to Starling, but can probably get away with treating them as a scalar type rather than a compound type for now.)

In this case, * would be part of the assignment operator, which is perhaps surprising. I'm not sure of a better way of marking this up though. One possibility that works for the first type is a new assignment operator <- or :=, but I'm not sure how you'd mark up the second type.

[septract]

Hm, I think this is a good idea given infinite time, but is it a priority? Does it let us do something that we can't do now?

…

On Thursday, 23 February 2017, Matt Windsor ***@***.***> wrote: Quick syntax sketch for heap assignment: <| *PVALUE = EXPR; |> <| LVALUE = *PVALUE; |> where PVALUE is an lvalue of pointer type. (We'd have to add pointer types to Starling, but can probably get away with treating them as a scalar type rather than a compound type for now.) In this case, * would be part of the assignment operator, which is perhaps surprising. I'm not sure of a better way of marking this up though. One possibility that works for the first type is a new assignment operator <- or :=, but I'm not sure how you'd mark up the second type. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#148 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9nC8AI3OfU78KU5Q_Ln7IvIHm1ZHks5rfcFbgaJpZM4MI97T> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

It's not a priority, though it's something I might be tempted to knock together over a few weekends.

The main advantages I can see are:

• Tidier and easier to read proofs (fits with the idea of Starling being a model for 'developer-friendly' tools);
• Not having to explain or skirt around symbols when explaining Starling to other people;
• Having a stronger amount of syntax and semantic checking before handing to GRASShopper (ideally, there should never be any GRASShopper syntax errors);
• Eventually, allowing more optimisations (symbols are a complete black hole when it comes to optimisations; there might be some things we can do with heap writes, but they'd probably be limited to eg. simplifying atomic actions).

On the other hand, doing this through symbols is a good demonstration of how flexible Starling is.

[septract]

All noble goals, but they don't add much to your thesis: I'd suggest skipping it and working on better inference.

…

On 24 February 2017 at 09:04, Matt Windsor ***@***.***> wrote: It's not a priority, though it's something I might be tempted to knock together over a few weekends. The main advantages I can see are: - Tidier and easier to read proofs (fits with the idea of Starling being a model for 'developer-friendly' tools); - Not having to explain or skirt around symbols when explaining Starling to other people; - Having a stronger amount of syntax and semantic checking before handing to GRASShopper (ideally, there should never be any GRASShopper syntax errors); - Eventually, allowing more optimisations (symbols are a complete black hole when it comes to optimisations; there might be some things we can do with heap writes, but they'd probably be limited to eg. simplifying atomic actions). On the other hand, doing this through symbols is a good demonstration of how flexible Starling is. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#148 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AANd9hr9NjkVwaL5xNNJgJMatRAkZ-k7ks5rfp0agaJpZM4MI97T> .

-- http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

Adding noncritical as per Mike's assessment.