The idea that all ADT's must be `lifted' appears clunkier and clunkier
over time, so I support Simon's suggestion.
Note that Simon's suggestion can be easily generalised. Our current
declaration form is
datatype T a_1 ... a_k = C t_1 ... t_n | ...
Simon suggests we add
newtype T a_1 ... a_k = C t
with the (semantic) difference that C bottom = bottom, whereas if we
had used the corresponding datatype then C bottom /= bottom. The
generalisation is to instead add
newtype T a_1 ... a_k = C t_1 ... t_n
with the difference that C bottom ... bottom = bottom, whereas if we
had used the corresponding datatype then C bottom ... bottom /=
bottom. In other words, the generalisation of Simon's idea is unlifted
products.
Thus I propose:
(1) We generalise the `newtype' construction as outlined above.
(2) We make products unlifted rather than lifted. That is, instead of
datatype (a_1, ..., a_n) = MakeTuple_n a_1 ... a_n
we have
newtype (a_1, ..., a_n) = MakeTuple_n a_1 ... a_n
This makes programs more defined, so all valid programs still run.
My main reason for making the suggestion is that just as lifted ADT's
appear clunkier and clunkier over time, so do lifted products. There
have been a number of times I have been forced to write
f ~(x,y) = ...
which is rather obscure. I was especially galled to realise that in
language called Haskell, the main equation of Currying does not hold.
That is, the types
(a,b) -> c and a -> b -> c
are not isomorphic. They would be with unlifted products.
Our main reason for avoiding unlifted products before was that we
wanted to avoid complexity. Simon has rightly pointed out that we
need this complexity anyway. We ought to make the most of it.
A secondary reason was that we were afraid of the potential cost
of unlifted products. We now have the tools in place to measure
such costs. Simon, Lennart, Paul, would this be difficult to do?
Cheers, -- P
-----------------------------------------------------------------------
Professor Philip Wadler [EMAIL PROTECTED]
Department of Computing Science tel: +44 41 330 4966
University of Glasgow fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND
