Proposal: EmptyDataDecls

Compiler support

[Information from language documentation.]

Summary

Allow data declarations with no constructors.

Description

The proposal is to allow empty data declarations, i.e. data types without any constructors. Syntactically, it is basically just a matter of making the "= constrs" part optional in the context free syntax. Semantically, the result is a type (once the type constructor has been fully applied) whose only element is bottom. Examples (assuming Infix Type Constructors is adopted):

data S
  
data T a
  
data a :*: b
  
data (a :**: b) c

Kind inference will of course be carried out for type constructors introduced by empty declarations just as for all other type constructors according to whatever rules are adopted. Unless there are further constraints, the kinds of the constructors above would be

S :: *
T :: * -> *
(:*:) :: * -> * -> *
(:**:) :: * -> * -> * -> *

If kind annotations are adopted, they should obviously also apply to empty declarations. They would possibly be a little more important for empty declarations, though, as empty declarations lack(!) any data constructors to suggest the intended kind of the type arguments. Thus, for a human reader, working out from the program text what the inferred kind of a type constructor for an empty type is would seem a tad harder than for non-empty types, especially if one of the more refined versions of kind inference is adopted. Polymorphic kinds would make this point moot, though, as kind annotations then never would be needed, unless it is decided that kind annotations still would be good documentation.

Note that contexts of course also would be allowed, but, as there are no data constructors, their only impact would be on the inferred kind.

The only real issue is whether or not to allow the optional deriving clause after an empty declaration, and, if not, on what stage to rule them out. Clearly, as there are no data constructors over which to define functions, derived instances would (for consistency) have to be everywhere undefined. GHC seems to syntactically allow a deriving clause after an empty data declaration, but the treats it as a contextual error since no interesting instances can be defined. Presumably the reasoning was that this gives a more regular syntax and better error messages than ruling out deriving for empty declarations syntactically. But the point is that there is a choice.

For this extension, probably the best course of action is to follow GHC and allow deriving () clauses for empty data declarations. That way no deriving clause and deriving () still have the same semantics. To do this, we syntactically allow all deriving clauses for empty data, but semantically limit the clauses to deriving ().

References

• http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#nullary-types GHC documentation.

Report Delta

Replace the syntax in http://www.haskell.org/onlinereport/decls.html 4 Declarations and Bindings:

topdecl → …

| data [context ⇒] simpletype = constrs [deriving]

with

topdecl → …

| data [context ⇒] simpletype [= constrs] [deriving]

Make the same change in the copy of the syntax at the top of 4.2.1 Algebraic Datatype Declarations. Also in that section, replace the sentence:

This declaration introduces a new type constructor T with one or more constituent data constructors K1, …, Kn.

with

This declaration introduces a new type constructor T with zero or more constituent data constructors K1, …, Kn.

Also, in the description of when derived instances are possible for a class C http://www.haskell.org/onlinereport/derived.html#derived-appendix, add the following condition.

1. If the data declaration has no constructors (i.e. when n=0), then no classes are derivable (i.e. m=0).