Type generalization ``order''?
20 Jul 2001 14:37:54 -0000
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  and Jones  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.