Type generalization ``order''?

[kahl@heraklit.informatik.unibw-muenchen.de]

The Haskell 98 report (also in the current revised version)
includes the following in section 4.1.4:

 > Types are related by a generalization order (specified below);
 > the most general type that can be assigned to a particular expression
 > (in a given environment) is called its principal type.
 > Haskell 's extended Hindley-Milner type system can infer the
 > principal type of all expressions, including the proper use of
 > overloaded class methods (although certain ambiguous overloadings
 > could arise, as described in Section 4.3.4). Therefore, explicit typings
 > (called type signatures) are usually optional (see Sections 3.16 and 4.4.1).
 > 
 > The type  forall u. cx1 =>t1  is more general than the type
 > forall w. cx2 =>t2  if and only if there is a substitution S
 > whose domain is u such that:
 > 
 >    t2 is identical to S(t1).
 > 
 >    Whenever cx2 holds in the class environment, S(cx1) also holds.

The relation defined here clearly is a preorder.
If it is an order, then in particular the following types are equal
(via identical substitutions):

(Eq a, Ord b) => (a,b)
(Ord b, Eq a) => (a,b)
(Eq b, Ord b, Eq a) => (a,b)
(Eq [a], Ord b) => (a,b)

It seems to me that this arises since the report only defines
the SYNTAX of contexts
(see the heading ``4.1.3  Syntax of Class Assertions and Contexts''),
but never defines what a context IS, that is, the SEMANTICS of contexts.

A context could be:

 * a SEQUENCE of class assertions (according to the syntax)

 * a SET      of class assertions (slightly more intuitive)

 * a THEORY   of class assertions

If type generalisation is an order,
then the third alternative was chosen.

I suggest to include an appropriate hint in the report...
(I am aware of the beginning of 4.1.4:

 > In this subsection, we provide informal details of the type system.
 > (Wadler and Blott [11] and Jones [6] discuss type and constructor classes,
 > respectively, in more detail.)

 I think this kind of outsourcing of essential parts of the
 language definition is not desirable.
)


Best regards,

Wolfram