Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007583OCamltypingpublic2017-07-12 18:042017-09-06 09:50
Reporteryallop 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007583: Request: empty record and variant types
DescriptionAt 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 _ -> .'
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0018067)
gasche (developer)
2017-07-12 18:08

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!
(0018068)
xleroy (administrator)
2017-07-12 18:58

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).
(0018069)
xleroy (administrator)
2017-07-12 18:59

@gasche your bias towards empty types is well known!
(0018072)
octachron (developer)
2017-07-12 22:56

On the typographic side, I am wondering if

type t = I
type t = |

might be a little too close for comfort
(0018073)
gasche (developer)
2017-07-12 23:00

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.
(0018074)
yallop (developer)
2017-07-12 23:10
edited on: 2017-07-12 23:17

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

  type t =

(0018077)
stedolan (developer)
2017-07-14 14:32
edited on: 2017-07-14 14:32

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)

(0018078)
yallop (developer)
2017-07-14 15:05

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]
(0018079)
gasche (developer)
2017-07-14 15:06

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.
(0018190)
runhang (reporter)
2017-08-22 09:07

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.
(0018209)
frisch (developer)
2017-08-31 17:10

> 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?
(0018210)
yallop (developer)
2017-08-31 20:43

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.
(0018216)
frisch (developer)
2017-09-05 11:07

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.
(0018217)
frisch (developer)
2017-09-05 11:09

(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...)
(0018218)
yallop (developer)
2017-09-05 11:49

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.
(0018230)
frisch (developer)
2017-09-06 09:50

> 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.

- Issue History
Date Modified Username Field Change
2017-07-12 18:04 yallop New Issue
2017-07-12 18:08 gasche Note Added: 0018067
2017-07-12 18:58 xleroy Note Added: 0018068
2017-07-12 18:58 xleroy Status new => acknowledged
2017-07-12 18:59 xleroy Note Added: 0018069
2017-07-12 22:56 octachron Note Added: 0018072
2017-07-12 23:00 gasche Note Added: 0018073
2017-07-12 23:10 yallop Note Added: 0018074
2017-07-12 23:17 yallop Note Edited: 0018074 View Revisions
2017-07-14 14:32 stedolan Note Added: 0018077
2017-07-14 14:32 stedolan Note Edited: 0018077 View Revisions
2017-07-14 15:05 yallop Note Added: 0018078
2017-07-14 15:06 gasche Note Added: 0018079
2017-08-22 09:07 runhang Note Added: 0018190
2017-08-31 17:10 frisch Note Added: 0018209
2017-08-31 20:43 yallop Note Added: 0018210
2017-09-05 11:07 frisch Note Added: 0018216
2017-09-05 11:09 frisch Note Added: 0018217
2017-09-05 11:49 yallop Note Added: 0018218
2017-09-06 09:50 frisch Note Added: 0018230


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker