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
Comments
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! |
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). |
Comment author: @xavierleroy @gasche your bias towards empty types is well known! |
Comment author: @Octachron On the typographic side, I am wondering if type t = I might be a little too close for comfort |
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. |
Comment author: @yallop One possible alternative is to give an empty variant an empty right hand side, like this type t = |
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:
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 (One solution which does work at the moment:
) |
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] |
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. |
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 |
Comment author: @alainfrisch
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? |
Comment author: @yallop In Protobuf files, all of the following enumerated types are valid: enum A { X = 0; Y = 1; }; 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. |
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. |
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...) |
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. |
Comment author: @alainfrisch
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. |
Comment author: @yallop
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. |
Comment author: @yallop #7583#c18190:
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. |
Comment author: runhang A pull request for empty variants is ready for review: #1546 |
#1546 is merged and I am not sure if we want to continue discussion on empty record. |
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:
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 I'm interested in this feature for the |
Not that I want to really re-open the discussion, but you could as well define initially-constant constructors as |
I suppose that would work as well! |
Thanks for the suggestion |
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. |
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 _ -> .'
The text was updated successfully, but these errors were encountered: