wiki:EmptyDataDecls

Version 6 (modified by sweirich, 5 years ago) (diff)

Start on format. Still need to update some sections.

Proposal: EmptyDataDecls

Ticket #25
Dependencies names of other proposals on which this one depends
Related

#85
more liberal kind inference

#84
Kind Annotations

#78
Add infix type constructors

Compiler support

GHC [ full (flagname) | partial (flagname) (comments) | none ]
nhc98 [ full (flagname) | partial (flagname) (comments) | none ]
Hugs [ full (flagname) | partial (flagname) (comments) | none ]
UHC [ full (flagname) | partial (flagname) (comments) | none ]
JHC [ full (flagname) | partial (flagname) (comments) | none ]
LHC [ full (flagname) | partial (flagname) (comments) | none ]

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 types constructors introduced by empty declarations just as for any 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.

  • A simple and natural generalisation of data declarations, seemingly without any hidden complications.

References

Report Delta

The changes to the report necessary to implement the proposal. Required for a proposal to move to the "accepted" state.