Syntax and checking for immutable values and functions

[dsainati1]

Issue To Be Solved

A number of issues and PRs currently would benefit from the ability to know whether or not a function is "pure" or has the potential to mutate state. Examples of issues that would be helped by this would be https://github.com/onflow/cadence/issues/1805, https://github.com/onflow/cadence/issues/1304, https://github.com/onflow/flow/pull/1043 and the follow-up work on https://github.com/onflow/flow/pull/703.

Suggested Solution

This would add a new piece of syntax to the language allowing users to annotate their functions as "pure" or "impure". The exact nature of this syntax is up for consideration (What specific names would we use? What would be the default purity for an unannotated function? Which functions require annotations?), but this syntax would then be used to power a semantic analysis as part of type checking to enforce that "pure" functions do not have any side effects: i.e. they do not modify or assign to any external state, and they only call "pure" functions within their bodies. "Impure" functions would have no such restrictions on what operations they can perform and which functions they can call.

[dsainati1]

A couple thoughts for consideration here:

1. We would probably need/want to require that all public/exported functions be explicitly annotated as pure or impure, because the potential bubble effects of making a change to one function could impact the purity of functions arbitrarily far away. Requiring that public functions be explicitly annotated helps keep the scope of any potential analysis we do small, and also prevents an internal implementation change in one contract from affecting the type checking of another contract.

2. What would we do in the case of recursive or mutually recursive functions? The easy thing would be to just require an explicit annotation on functions that are recursive, but in theory we could also do some kind of fixed-point analysis.

3. Do we want to extend this to variables, fields and references? One could imagine a const-like declaration for composites or containers that passing them as arguments to or using them as a receiver for any impure functions.

4. What should the default be for an unannotated function? Having unannotated functions default to being impure would have the benefit of requiring fewer code changes, since if everything is impure then no analysis needs to occur. On the other hand, if we envision a future in which more code is pure, then that would result in more annotation requirements later on.

[SupunS]

One more thing to consider/think about is the covariance/subtype checking between pure/impure functions.

Might be a good reference: D-lang has pure functions: https://dlang.org/spec/function.html#pure-functions.

[turbolent]

We should clearly define what the attribute(s) of a function are.

• For example, GCC has support for pure and const functions.
• Solidity has pure and view functions

[bluesign]

I have some questions to make it a bit clear.

• If I define a function pure I cannot change it later to impure right?
• Isn't pure will be dead on arrival with this? I mean we can say post/pre conditions can call only pure etc but, are there any other use case?
• As #1304 referenced, what is the use case for #1304 here with pure functions?

[dsainati1]

If I define a function pure I cannot change it later to impure right?

You can change the purity annotation, but this would cause type errors in any pure functions that use this function, or in any other places where impure functions are not allowed.

Isn't pure will be dead on arrival with this? I mean we can say post/pre conditions can call only pure etc but, are there any other use case? As https://github.com/onflow/cadence/issues/1304 referenced, what is the use case for https://github.com/onflow/cadence/issues/1304 here with pure functions?

The answers to these are similar; yes requiring that pre/post conditions only use pure functions is one benefit of this, but another is that this allows us to have better mutability guarantees about composite types. Currently although we try to ban field mutation in public fields, when those fields are composites we have no way of knowing whether or not they will be mutated by one of their methods. Purity analysis like this would allow us to actually have this information, so we could enforce that people can only call pure methods on public fields. This helps with security in the case of resource fields and also reentrancy for contract fields.

Having pure functions also helps with immutable references, because then we could statically enforce that a read-only reference can only call pure methods on the value that it references. Without this, we would have to make the read-only guarantee purely runtime, we'd have no static way to determine if a read-only reference was truly read-only.

[bluesign]

I look from another perspective here:

• allowing pure / impure change is big hammer ( hurts composability very much. )
• asking developers to mark every public function pure/impure is a bit too hopeful and fragile
• I think when marked impure ( not marked) it will not be verified, so people will have no reason to mark function as pure.
• Immutable references case: if the developer was lazy, didn't mark getID function as pure, I will not be able to call. ( Even function is not modifying state )

I believe caller should be able to foresee panic ( if it is raised by Cadence ). I mean we are allowing panic in contract scope, I think trying to mutate immutable reference is less foot gun than that.

I think my thinking is more in line with, without modifying state I should be able to access everything ( even developer allows or not ) And to reach that level is only available with runtime panics I guess. Also I think it will be easier to implement.