I'd like to respond to recent comments about `strange' newtype
definitions. Definitions like
newtype Void = Void Void
or variants using mutual recursion are, in my opinion, entirely
reasonable (even if they are perhaps almost as entirely useless
in practice). I don't really think it has anything to do with
representations.
I start with the axiom that every type contains at least one
element: a bottom value.
In the case of a "data"type, all remaining elements of the type
are generated by applying its constructors to values of the
appropriate type.
In the case of a "newtype", all remaining elements of the type
are, once again generated by applying its constructor to a value
of the appropriate type. The only difference here---apart from
allowing only a single constructor, N, and with only a single
argument---is that we expect N bottom = bottom.
So the values of type Void are just bottom, Void bottom,
Void (Void bottom), Void (Void (Void bottom)), ... But, of
course, because Void bottom = bottom, it quickly follows that
all of these values are just bottom. Thus bottom is the only
value of type Void.
For the purposes of type checking, "newtype"s are treated just
like "data"types. For the backend, you can use exactly the
same representation for the argument of the newtype constructor
as you use for the "newtype" itself. And then constructor
functions like N or Void (and their inverses, used in pattern
matches) can be translated into identity functions, many of
which can be removed by a trivial optimization: id e = e.
All the best,
Mark
