Add functions

[effectfully]

We need functions. Even non-recursive ones would be handy, but we probably want statically unrollable recursive functions.

Lambdas or proper function declarations? Having debugged Plutus Core code, I'm leaning towards the latter as we already have let-statements anyway.

[effectfully]

we probably want statically unrollable recursive functions

Let's not do that for now. I'm still not quite sure as to whether unroll things on the language side of Zonk or on the compiler side. The former is simpler, the latter can be more efficient, because we unroll, compile and optimize at the same time, so a recursive function that computes some value would be optimized away to that value on the compiler side. We could interleave unrolling and evaluation on the language side as well, but then

1. we need to duplicate parts of the compiler and preserve the semantics
2. the compiler is still in a better position, because it could unroll, compile and optimize functions evaluating to complex expressions (not just constants) on the fly

One disadvantage of unrolling things on the compiler side is that this requires dealing with non-uniqueness of variable names. When we were unrolling loops on the language it was simple "unroll all the loops, then rename the entire program". But if we interleave unrolling and compilation, we'd have to worry about preserving global uniqueness of variables, which might be annoying and is certainly error-prone.

Although we are going to face a similar problem even when implementing function-unrolling on the language side, because unrolling stuff like f v (where v is a variable) can easily result in name capturing, so we have to be careful anyway.

I think it makes sense to try both the options. I'm already going to implement loop-unrolling on the compiler side, so let's implement function-unrolling on the language side and see if it gives us any more info.

[effectfully]

Regarding the design. Quoting this comment:

We can have the same convention as in Haskell: main is the entry point.

That means that we'll have to distinguish between functions and procedures, though. Just like we distinguish between expressions and statements right now (which is something that we have to do, because assertions can only be compiled when they're at the top level, see this comment, so "statements" arise naturally).

I.e. you can call a function (that can't contain any statements) only from an expression and a procedure (which is a bunch of statements) call is a treated as a statement. In that sense a for loop is a procedure.

We have two options for syntax.

C-style: function int f (int x, int y) { ... }. Pros: crypto people are comfortable with that syntax.

Haskell-style:

f : Int -> Int -> Int
f x y = ...

p : Int -> Int -> Statement
p x y = ...

where p is a "procedure", since it returns a Statement.

I much prefer the latter option as it also allows us to do things like (pseudosyntax)

p : (Int -> Statement) -> Int -> Statement
p f i = do
    f (i - 1)
    f i
    f (i + 1)

use partial application, etc.

[effectfully]

p : (Int -> Statement) -> Int -> Statement
p f i = do
    f (i - 1)
    f i
    f (i + 1)

We don't have indentation-sensitive syntax yet, so that would be

p : (Int -> Statement) -> Int -> Statement
p f i = do
    f (i - 1);
    f i;
    f (i + 1);
end;

or something like that in the current syntax.

[jakzale]

Regarding syntax, should we follow Haskell syntax or Rust syntax? We already follow Rust syntax for C-family like comments. We probably need #44 for functions.

I think we should start with lambdas and applications, as that will be the most straightforward to implement.

For instance the built-in neq0 could be expressed as

let neq0 : field -> bool = fun x do not (x == 0) end

[effectfully]

Regarding syntax, should we follow Haskell syntax or Rust syntax?

I honestly have no idea what's better for us. My instinct would be just to have as Agda-like syntax as possible, but then our users are cryptographers and they'll be more comfortable with C/Rust-style syntax. Maybe we should ask people directly what they want.

We probably need #44 for functions.

Why? That issue is closed.

For instance the built-in neq0 could be expressed as

let neq0 : field -> bool = fun x do not (x == 0) end

It's the other way around: x == y = not (x - y /= 0). Not-equal-to-zero is one of the central primitives in this setting (see e.g. the "Zero-Equality Gate" section of Pinocchio: Nearly Practical Verifiable Computation, but it's literally everywhere: in the "Desiging zero knowledge circuits" slides, in the Snarkl repo etc).

[jakzale]

Maybe we should ask people directly what they want
I think that is a good option.

Why?
We moved to a statement-based language, therefore I believe that we need the following:

• a statement for returning a value from a function, or
• implicitly returning the value of the last statement of a function, and
• a type for functions that do not return values.

It's the other way around
Ah, my bad. Thanks for the references.

[effectfully]

Maybe we should ask people directly what they want

I think that is a good option.

Could you do that? (Note though that we still should feel free to make whatever decisions we think are sensible, so it's not that we ask something and then blindly implement what we are told to)

a type for functions that do not return values.

I think we should start with this. It's not Unit, though! It's something more specific, like Statement. Maybe eventually we'll end up having a Statement monad, i.e.

a statement for returning a value from a function, or

and ; meaning Monad's "bind", but let's start with something simpler.

While we're here, could you also ask people about syntax for functions? I wrote on that before and I think there are benefits to using Haskell-like syntax for them, but not sure what people think. Also make sure to ask Manuel as he might want to say "this all will be used within Plutus and we don't want any imperative syntax there".