New syntax for function definitions

[janmasrovira]

• Closes Syntax for mutually recursive types #2060

• Closes Re-think function definitions #2189

• This pr adds support for the syntax described in Re-think function definitions #2189. It does not drop support for the old syntax.

It is possible to automatically translate juvix files to the new syntax by using the formatter with the --new-function-syntax flag. E.g.

juvix format --in-place --new-function-syntax

Syntax changes

Type signatures follow this pattern:

f (a1 : Expr) .. (an : Expr) : Expr

where each ai is a non-empty list of symbols. Braces are used instead of parentheses when the argument is implicit.

Then, we have these variants:

1. Simple body. After the signature we have := Expr;.
2. Clauses. The function signature is followed by a non-empty sequence of clauses. Each clause has the form:

| atomPat .. atomPat := Expr

Mutual recursion

Now identifiers do not need to be defined before they are used, making it possible to define mutually recursive functions/types without any special syntax.
There are some exceptions to this. We cannot forward reference a symbol f in some statement s if between s and the definition of f there is one of the following statements:

1. Local module
2. Import statement
3. Open statement

I think it should be possible to drop the restriction for local modules and import statements

[paulcadman]

In https://github.com/anoma/juvix-stdlib/blob/85751d3a7e5edd97a3d12dae197273731a2088cf/Stdlib/Data/Bool.juvix#L15 we now must write:

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

module BoolTraits;
  Eq : Eq.Eq Bool :=
...

instead of:

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

module BoolTraits;
  Eq : Eq Bool :=
...

(The latter now fails the termination checker).

The reasoning for allowing Eq : Eq Bool was that it was not possible refer to the lhs Eq in its type signature so there was no ambiguity. Did you conclude that this was too confusing so it's better to qualify Eq, or was this change a side-effect of something else?

[paulcadman]

If implementors of traits must use Eq : Eq.Eq A := ... then perhaps we should use the suffix Trait for trait definitions:

--- A trait defining equality
type EqTrait (A : Type) :=
  | mkEq : (A -> A -> Bool) -> EqTrait A;

Then implementors of traits would not have to do any additional imports other than the Prelude (as before) and could write the following (avoiding the stuttering):

Eq : EqTrait A := ...

What do you think?

[janmasrovira]

In https://github.com/anoma/juvix-stdlib/blob/85751d3a7e5edd97a3d12dae197273731a2088cf/Stdlib/Data/Bool.juvix#L15 we now must write:

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

module BoolTraits;
  Eq : Eq.Eq Bool :=
...

instead of:

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

module BoolTraits;
  Eq : Eq Bool :=
...

(The latter now fails the termination checker).

The reasoning for allowing Eq : Eq Bool was that it was not possible refer to the lhs Eq in its type signature so there was no ambiguity. Did you conclude that this was too confusing so it's better to qualify Eq, or was this change a side-effect of something else?

This was a side-effect of allowing forward references. Before the Eq on the rhs referred to the imported Eq. Now it refers to the Eq in the lhs, so it fails the termination checker.

[janmasrovira]

If implementors of traits must use Eq : Eq.Eq A := ... then perhaps we should use the suffix Trait for trait definitions:

--- A trait defining equality
type EqTrait (A : Type) :=
  | mkEq : (A -> A -> Bool) -> EqTrait A;

Then implementors of traits would not have to do any additional imports other than the Prelude (as before) and could write the following (avoiding the stuttering):

Eq : EqTrait A := ...

What do you think?

I agree that Eq.Eq looks bad. But I am not fully convinced by defining type EqTrait (A : Type), since ultimately we want to use traits in many places and it will be tedious to repeat xTrait instead of x potentially multiple times in most of the type signatures. Imagine our Haskell codebase where every class constraint is suffixed by Trait.

One option is to replace the existing

open Eq using {Eq};

By

open Eq using {Eq as EqTrait};

And then have

Eq : EqTrait A := ...

As you suggested.

[paulcadman]

The main issue I have with the Eq.Eq is that trait implementors must write (and discover that they must write) import Stdlib.Trait.Eq as Eq; instead of just importing Stdib.Prelude so open Eq using {Eq as EqTrait}; wouldn't solve that. But I agree that the Trait suffix is not a good idea.

[janmasrovira]

The main issue I have with the Eq.Eq is that trait implementors must write (and discover that they must write) import Stdlib.Trait.Eq as Eq; instead of just importing Stdib.Prelude so open Eq using {Eq as EqTrait}; wouldn't solve that. But I agree that the Trait suffix is not a good idea.

That's true, but this is a temporary problem. In the not so distant future we will have trait instances, which will not bind any name, and so this won't be a problem anymore. So trait implementors (outside of the stdlib) will be able to write

import Stdlib.Prelude;

instance Eq Bool :=
    mkEq ...

In the meanwhile, another possible temporary patch would be to add a local module in the prelude:

module Trait;
  import Stdlib.Trait open public;
end;

And then the users can write:

import Stdlib.Prelude;

Eq : Trait.Eq Bool :=
    mkEq ...

It is maybe slightly better than the option I gave before, but it still does not fully solve the discoverability problem

[paulcadman]

And then the users can write:

import Stdlib.Prelude;

Eq : Trait.Eq Bool :=
    mkEq ...

This is very good - thanks! I'll raise it as an issue against stdlib once this PR is merged.