Type generalization ``order''?

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

Simon Peyton-Jones <simonpj@microsoft.com> wrote:
 
> If, however, you can suggest some specific sentences that would help
> to eliminate confusion, then please do suggest them.

It is, to a certain extent, a design decision.

One possibility might be to change

 > 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.

to

 > Types are related by a generalization preorder (specified below);
 > the most general type (up to the equivalence induced by that preorder)
 > that can be assigned to a particular expression
 > (in a given environment) is called its principal type.

Another possibility might be to leave generalization as it is:

 > 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.

and add a sentence here:

 > This implies that two contexts are considered equal
 > if and only if they imply the same set of class assertions
 > in the class environment.

Instead of ``equal'' one might consider
the somewhat less precise ``equivalent''.


Wolfram