Following recent discussions about strictness annotations, and the
reservations people had about introducing them into standard Haskell, I
thought I would mention that there is another way of thinking about them that
might be helpful.
You can think of a type !t as meaning `t without _|_' (a subtype of t, if you
like), and a type declaration
f :: !t -> u
as meaning `in a correct program, f will never be applied to _|_', just as f
:: t -> u means `in a correct program, f will never be applied to values
outside of the type t'. The difference is that the restriction is not
enforceable by the type checker.
This can then be interpreted as meaning that the value of (f _|_) is not
constrained, so that the implementation is free to evaluate its argument or
not, as convenient; the usual treatment forces (f _|_) to be _|_. For example,
if you have a strict constructor applied to a function, (one of the difficult
cases mentioned in the discussions) the implementation is free to leave the
function unevaluated.
Incidentally, I find the unlifted function type in Haskell rather odd. It
seems inconsistent with the rest of the language, and it makes the language
internally incomplete. What I mean is that Haskell is externally complete in
the sense that any computable real-life problem can be modelled using Haskell
types and functions. However, internally, there are functions on Haskell's
value space which are computable and type correct, but which can't be defined
(as opposed to simulated). Of course, these are just the ones definable using
seq or strict. You can think of seq as the destructor function for _|_, just
as if it were a (slightly special, I admit) data constructor. I know there are
implementation reasons for the choice in some compilers, but...
I would like to use such annotations for two purposes, which you could call
subtypes and supertypes:
Subtypes
--------
It is fairly easy to see how the above discussion about !t might be extended
to more general subtypes (types with invariants). I wrote an internal report
on this a long time ago, and it was developed a bit further in a recent PhD
report by a student of mine.
Supertypes
----------
There are semantic problems with classes that have haunted me (and others) for
ages. I think classes should be eliminable in the same sense as types: if you
remove them, you should get a correct uni-typed program (ie as if all the
constructors were lumped together into one giant data type). One way to do
this is to add strictness annotations to the method types to specify how they
can evaluate their arguments in such a way as to determine at run time which
version to use. An overloaded function can then be regarded as an ordinary
function defined on a supertype; a class is like the union of a collection of
types. This is a restriction on some current freedoms, but I am becoming
convinced that it would open up new possibilities which would outweigh this.
Maybe when brisk is further advanced, I can make some of these ideas more
concrete.
Ian [EMAIL PROTECTED], Tel: 0272 303334
