~sircmpwn/public-inbox

4 2

BARE extra proposals

Victorien Elvinger <victorien.elvinger@inria.fr>
Details
Message ID
<057d4f02-984e-b988-57df-297c078ea283@inria.fr>
DKIM signature
pass
Download raw message
Hi!

I finally come back with some new feedback.


## Root types and void types

void types are already well constrained since they are only allowed in
tagged unions.

I would like to add an extra invariant:

     A type that is ultimately a void type (either directly or via a
     user-defined type) MUST be used by at least one tagged union.

Another way to express that could be:

     A root type is a type that is not used by another type.
     A root type MUST NOT be ultimately a void type (either directly or
     via a user-defined type).

This allows to ensure that any root types do not resolve to void.
Implementations could rely on this to generate specific decoder/encoder
for root types.


## BARE messages and void types

I am wondering if we should not add also the following invariant:

     A BARE message is a single value of a type that MUST NOT
     be ultimately a void type (either directly or via a user-defined
     type).

However I am not sure it is useful. Maybe the spec already rule out this
case?


## @extern

We already discussed about annotations and ruled it out.

However, I would like to propose the addition of a single predefined
annotation for annotating type-definitions.

This annotation could allow implementations to import external
decoders/encoders and/or to provide a way to define custom decoders
and encoders for a type (it is one of the goals of BARE).

It is an annotation, because implementations may ignore it.

I am not sure for the name: maybe @extern?

e.g.

     @extern
     type WrappedMessage data

     type Message struct {
         metadata: map<str><str>
         wrapped: WrappedMessage
     }

The ABNF could be changed as follows:

     user-type = ["@extern" WS] "type" WS user-type-name WS any-type

Have a nice evening!
Details
Message ID
<20220509162413.GA5191@gmail.com>
In-Reply-To
<057d4f02-984e-b988-57df-297c078ea283@inria.fr> (view parent)
DKIM signature
pass
Download raw message
> void types are already well constrained since they are only allowed in
> tagged unions.
> 
> I would like to add an extra invariant:
> 
>     A type that is ultimately a void type (either directly or via a
>     user-defined type) MUST be used by at least one tagged union.

I'm not sure why is that. Wouldn't this disallow used-in-the-future
types? An example:

	type Nowadays void
	type Future void
	type Msg union {Nowadays}

But Future will not be encoded, so I'm probably missing something.

> This allows to ensure that any root types do not resolve to void.
> Implementations could rely on this to generate specific
> decoder/encoder for root types.

It's probably my lack of knowledge, again. What is meant by root type?

> I am wondering if we should not add also the following invariant:
> 
>     A BARE message is a single value of a type that MUST NOT
>     be ultimately a void type (either directly or via a user-defined
>     type).
> 
> However I am not sure it is useful. Maybe the spec already rule out this
> case?

I think it's not necessary. As you said, void types can be used in
tagged union only. Therefore, the following example results to nothing
being encoded:

	type Nowadays void
	type Msg Nowadays

> ## @extern
> 
> We already discussed about annotations and ruled it out.
> 
> However, I would like to propose the addition of a single predefined
> annotation for annotating type-definitions.

I don't think it's good idea to introduce just one small annotation. We
should do this properly. I think it's better to miss some small feature
than to be inconsistent or half-made.

> This annotation could allow implementations to import external
> decoders/encoders and/or to provide a way to define custom decoders
> and encoders for a type (it is one of the goals of BARE).

I think it's ok to keep the list of types and external decoders/encoders
separated from the schema. That would be necessary anyway if different
encoders/decoders would be used for different types or one type having
different decoder and different encoder, as @extern just says that
something else should be used to decode/encode, IMO.
Details
Message ID
<2789f44d-eed9-13d5-0805-5de069544802@elvinger.fr>
In-Reply-To
<20220509162413.GA5191@gmail.com> (view parent)
DKIM signature
missing
Download raw message
 > I'm not sure why is that. Wouldn't this disallow used-in-the-future
 > types? An example:
 >
 >	type Nowadays void
 >	type Future void
 >	type Msg union {Nowadays}

Yes this disables this schema.
This is a kind of unused type.

IMO void should always be used (in at least one union).


 > What is meant by root type?

A root type is a user-defined type that is not referred
by another type.
In your example, Msg and Future are root types.

I am using this concept in bare-ts to automatically generate
root decoders and encoders.

I noted that it is a non-sense to generate root decoders/encoders
for a type that resolves to void.

It is possible to filter out types that resolve to void.
However, this looks nicer to add a constraint to rule out
root types that resolve to void.

Anyway it is a minor change.
Do what you think is best.


 > I don't think it's good idea to introduce just one small annotation.
 > We should do this properly. I think it's better to miss some small
 > feature than to be inconsistent or half-made.

Makes sense.
Details
Message ID
<Ynrb/74Z2ITkW0GT@gmail.com>
In-Reply-To
<2789f44d-eed9-13d5-0805-5de069544802@elvinger.fr> (view parent)
DKIM signature
pass
Download raw message
> > I'm not sure why is that. Wouldn't this disallow used-in-the-future
> > types? An example:
> >
> >	type Nowadays void
> >	type Future void
> >	type Msg union {Nowadays}
> 
> Yes this disables this schema.
> This is a kind of unused type.
> 
> IMO void should always be used (in at least one union).

I'm afraid this could complicate debugging. I can imagine situation when
you want to disable/change some type temporarily.
Details
Message ID
<ea93f0c6-4851-5e8a-47b6-7cb30adc3dfe@elvinger.fr>
In-Reply-To
<Ynrb/74Z2ITkW0GT@gmail.com> (view parent)
DKIM signature
missing
Download raw message
 > I'm afraid this could complicate debugging. I can imagine situation
 > when you want to disable/change some type temporarily.

Ok.

I think we can proceed to publication :)
Reply to thread Export thread (mbox)