Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Request: empty record and variant types #7583

Closed
vicuna opened this issue Jul 12, 2017 · 25 comments
Closed

Request: empty record and variant types #7583

vicuna opened this issue Jul 12, 2017 · 25 comments

Comments

@vicuna
Copy link

vicuna commented Jul 12, 2017

Original bug ID: 7583
Reporter: @yallop
Status: acknowledged (set by @xavierleroy on 2017-07-12T16:58:57Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing

Bug description

At present record types must have at least one field. However, it would sometimes be useful to have record types without fields.

For example, I have a library that generates OCaml types from message descriptions. Messages in the protocol may have no fields, and such messages would naturally map into records with no fields.

The behaviour of zero-field records is straightforward: the following declarations declare two incompatible types, each with the same representation as unit, and with '{ }' as constructor and pattern:

type s = { }
type t = { }

There was once a good reason to disallow records with no fields: field names were used to determine the record type being constructed. Back then the expression '{ }' would have constructed a record of type 't', and there would have been no way to construct a record of type 's' when the declaration for 't' was in scope. However, now that OCaml has type-based disambiguation (PR5759) there's an easy way to construct values of either type by writing '({ } : s)' or '({ } : t)'.

Similarly, OCaml currently requires that variant types have at least one constructor. However, it is sometimes useful to have variant types with no constructors. For example, just as a message in a protocol may have no fields, an enumerated type in a protocol may have no enumeration values. Such enumerated types would map naturally into variants with no constructors.

Since a variant declaration can start with '|', one possible syntax is as follows

type u = |

There was once a good reason to disallow variants with no constructors: there was no reasonable way to write an eliminator for such a type. (It would have been possible to write something arbitrary, like 'function _ -> assert false'.) However, now that OCaml has refutation patterns (PR6437) there's an easy way to eliminate empty types by writing 'function _ -> .'

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @gasche

I support this proposal which I agree would be very useful, even if the "= |" syntax looks odd. The empty type is proud of its oddity!

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @xavierleroy

That's a reasonable and well-argumented suggestion.

Inductive (variant) types with zero constructors are used in Coq as empty types / false propositions, although I'm not completely sure why they are preferred to other empty types such as forall (A: Type), A.

Concerning empty records, it would be more regular and it would avoid some special cases in the compiler to represent them by Atom(0) (the block of size 0, also used for arrays of length 0) rather than by Val_int(0) (the representation of the () value of type unit).

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @xavierleroy

@gasche your bias towards empty types is well known!

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @Octachron

On the typographic side, I am wondering if

type t = I
type t = |

might be a little too close for comfort

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @gasche

People may get into the habit of writing

type t = (* empty *) |

and I wouldn't expect this feature to be used very often anyway -- if it occurs in generated code, it may be a part that people do not read, and if people intentionally declare an empty type the name "empty" or "void" may be a hint to distinguish.

@vicuna
Copy link
Author

vicuna commented Jul 12, 2017

Comment author: @yallop

One possible alternative is to give an empty variant an empty right hand side, like this

type t =

@vicuna
Copy link
Author

vicuna commented Jul 14, 2017

Comment author: @stedolan

An empty type would certainly be useful, but I'm not sure why we need many of them. Wouldn't a single type 'empty' suffice? Similarly, what's the advantage of having many different empty record types instead of just using 'unit'?

By the way, here's a concrete example I ran into this morning where I really wanted an empty type:

(* computations that might fail *)
type ('a, 'err) comp = unit -> ('a, 'err) result
val map_success : ('a -> 'b) -> ('a, 'err) comp -> ('b, 'err) comp

It is nice to be able to use combinators like map_success with computations that are known not to fail, but it's tricky to make let Ok x = map_success ... not give an exhaustivity warning.

(One solution which does work at the moment:

  type _ is_unit = U : unit is_unit
  type empty = bool is_unit

)

@vicuna
Copy link
Author

vicuna commented Jul 14, 2017

Comment author: @yallop

It would be quite strange to make all empty types (or all unit types) equal. We don't do that for any other types, even where they're isomorphic. In fact, OCaml has just acquired a new way of introducing fresh types that are exactly isomorphic to (but not equal to) existing types, even to the point of sharing the same representation:

type 'a t = { x: 'a t } [@@unboxed]

@vicuna
Copy link
Author

vicuna commented Jul 14, 2017

Comment author: @gasche

As you point out we can already define an empty sum type using GADTs with an absurd constructor. So it's more about regularity of the language (in particular in the context of derived/generated definitions) than expressivity. Same thing for the empty record, we could use () instead.

@vicuna
Copy link
Author

vicuna commented Aug 22, 2017

Comment author: runhang

As I'm trying my hands on this feature (https://github.com/ocamllabs/compiler-hacking/wiki/Compiler-or-Language-projects-to-work-on#empty-record-and-variant-types), I met a difficulty and would like to have some suggestions here. typecore.ml uses labels to determine/disambiguate the types of a record. However, since we have no labels here, it seems that we can only rely on the function Env.find_type: Path.t -> t -> type_declaration, but there is no value of type Path.t involved here. It seems one solution here is to add a function in Env module to search the most recent empty record declaration in environment.

@vicuna
Copy link
Author

vicuna commented Aug 31, 2017

Comment author: @alainfrisch

It seems one solution here is to add a function in Env module to search the most recent empty record declaration in environment.

Indeed.

Honestly, I've the feeling that this is a lot of work for an unclear practical benefit.

For empty records, what's the advantage of generating "type t = { }" instead of e.g. "type t = SINGLETON" (assuming one wants to avoid collapsing all such "empty records" to "unit")? (Btw, this might suggest an implementation strategy for empty record: simply consider { } as a syntactic constructor).)

For empty sums, I'd be interested to see an actual instance of "For example, just as a message in a protocol may have no fields, an enumerated type in a protocol may have no enumeration values" in a protocol. Why would protocol introduce an enumeration without a value?

@vicuna
Copy link
Author

vicuna commented Aug 31, 2017

Comment author: @yallop

In Protobuf files, all of the following enumerated types are valid:

enum A { X = 0; Y = 1; };
enum B { X = 0; };
enum C { };

A conforming Protobuf compiler that generates OCaml code must handle all of these cases. There's a natural mapping to OCaml variants for the first two, and it would be useful if the mapping extended to the third.

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: @alainfrisch

But is there any useful Protobuf protocol using an empty enum? If not, you can be compliant by using any empty type -- I guess nothing forces a compliant Protobuf compiler to use generative types. The rationale seems weak enough to justify a language change.

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: @alainfrisch

(Or you can even generate fresh empty types {l: 'a. 'a}. It's not like users would need to build values of such a type...)

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: @yallop

Empty variants are a natural base case, as is shown by the fact that they're supported by many other languages with variants (e.g. Haskell, SML/NJ, Agda, Coq).

So the real question is: why should they be disallowed? The description gave one past reason (no way to write a destructor) that is no longer an issue. I can't think of any other reason to continue to outlaw them.

@vicuna
Copy link
Author

vicuna commented Sep 6, 2017

Comment author: @alainfrisch

So the real question is: why should they be disallowed?

I'm not saying they should be disallowed. I just don't believe that spending time on allowing them is a good use of our scarce development/reviewing resources.

@vicuna
Copy link
Author

vicuna commented Dec 14, 2017

Comment author: @yallop

However, now that OCaml has type-based disambiguation (PR5759) there's an easy way to construct values of either type by writing '({ } : s)' or '({ } : t)'.

Of course, it should also be possible to disambiguate using qualified names (cf. PR6054, GPR144):

M.{}, N.{}

I'd expect having paths available to be the usual case; relying on type-based disambiguation should be rare.

@vicuna
Copy link
Author

vicuna commented Dec 14, 2017

Comment author: @yallop

#7583#c18190:

However, since we have no labels here, it seems that we can only rely on the function Env.find_type: Path.t -> t -> type_declaration, but there is no value of type Path.t involved here. It seems one solution here is to add a function in Env module to search the most recent empty record declaration in environment.

I think the situation for {} is the same as for [], which is nowadays allowed as a user-defined constructor (#234). The similarity suggests a solution: add '{}' to the environment as a constructor, at which point the standard resolution mechanism should work without further changes.

@vicuna
Copy link
Author

vicuna commented Jan 24, 2018

Comment author: runhang

A pull request for empty variants is ready for review: #1546

@vicuna vicuna added the typing label Mar 14, 2019
@objmagic
Copy link
Contributor

#1546 is merged and I am not sure if we want to continue discussion on empty record.

@ghost
Copy link

ghost commented Apr 18, 2019

I have another compelling use case for empty records; they provide a great way to design a fully stable and extensible AST. More precisely, let's assume that we have an AST where:

  • all types are variant types
  • all constructors are inline records
  • values are always represented in the oldest possible way. More precisely, a file parses to the a value with the same structure no matter the version of the parser. This is enforced by making all types private and providing construction functions

Then you get an AST that you can extend at any time to either represent new language constructions or capture more information without breaking backward compatibility. However, that does mean that all constant constructors must be defined as X of {} just in case they get new arguments in the future.

I'm interested in this feature for the Astlib library we are currently designing, so I'm ready to spend some time on this.

@alainfrisch
Copy link
Contributor

Not that I want to really re-open the discussion, but you could as well define initially-constant constructors as X of unit and use patterns like X _. If you fear that people write X (), you should use an abstract type instead of unit.

@ghost
Copy link

ghost commented Apr 18, 2019

I suppose that would work as well!

@ghost
Copy link

ghost commented Apr 18, 2019

Thanks for the suggestion

@github-actions
Copy link

github-actions bot commented Sep 7, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label Sep 7, 2020
@github-actions github-actions bot closed this as completed Oct 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants