Extending type modules

[janmasrovira]

Context

While writing apps, we've realized that the following pattern is quite common:

module ExternalIdentity;
  type ExternalIdentity :=
    mkExternalIdentity@{
      unExternalIdentity : ByteArray;
    };

  fromByteArray : ByteArray -> ExternalIdentity := mkExternalIdentity;

  toByteArray : ExternalIdentity -> ByteArray :=
    ExternalIdentity.unExternalIdentity;

  toNat : ExternalIdentity -> Nat := toByteArray >> toAnomaContents;
end;

open ExternalIdentity using {ExternalIdentity} public;

We follow this pattern because we always want to use ExternalIdentity.toNat rather than toNat directly.
Essentially, this pattern is a workaround to extend the local module SatisfiedIndent implicitly defined by the type definition of SatisfiedIntent.

Proposal

I propose that we allow users to extend the module implicitly defined by type definitions by appending with module to the type definition. Then, all definitions in that (nameless) module will be appended to the implicit module that we generate.

With the proposed syntax the example above would become:

type ExternalIdentity :=
  mkExternalIdentity@{
    unExternalIdentity : ByteArray;
  }
 with
  fromByteArray : ByteArray -> ExternalIdentity := mkExternalIdentity;

  toByteArray : ExternalIdentity -> ByteArray :=
    ExternalIdentity.unExternalIdentity;

  toNat : ExternalIdentity -> Nat := toByteArray >> toAnomaContents;
end;

example (i : ExternalIdentity) : Nat := ExternalIdentity.toNat i;

[lukaszcz]

Just a note on the syntax: these semicolons in the middle (before with and after module) seem somewhat out of place for me. I think people can keep getting tripped on that - I definitely would. My intuition is that a semicolon in Juvix ends a definition (the only exception to this seems to be module definition - but maybe we should actually rethink that?).

[janmasrovira]

Just a note on the syntax: these semicolons in the middle (before with and after module) seem somewhat out of place for me.

Agreed, we could remove them

the only exception to this seems to be module definition - but maybe we should actually rethink that?

I think we kept them so that if we add module arguments we don't have parsing problems. But maybe parse it correctly with some backtracking even if we have module arguments.

[lukaszcz]

I think we kept them so that if we add module arguments we don't have parsing problems. But maybe parse it correctly with some backtracking even if we have module arguments.

Or we could (more consistently) use, e.g.,:

module M :=
  f1 (x : Nat) : Nat := ..;
  z := 10;
end;

?

[janmasrovira]

That makes sense