|Version 9 (modified by ross@…, 7 years ago) (diff)|
Proposal: Relaxed Dependency Analysis
Haskell 98 specifies that type inference be performed in dependency order to increase polymorphism. However most Haskell implementations use a more liberal rule (proposed by Mark Jones).
In Haskell 98, a group of bindings is sorted into strongly-connected components, and then type-checked in dependency order (H98 s4.5.1). As each dependency group is type-checked, any binders of the group that have an explicit type signature are put in the type environment with the specified polymorphic type, and all others are monomorphic until the group is generalized (H98 s4.5.2).
data BalancedTree a = Zero a | Succ (BalancedTree (a,a)) zig :: BalancedTree a -> a zig (Zero a) = a zig (Succ t) = fst (zag t) zag (Zero a) = a zag (Succ t) = snd (zig t)
As with many operations on non-regular (or nested) types, zig and zag need to be polymorphic in the element type. In Haskell 98, the bindings of the two functions are interdependent, and thus constitute a single binding group. When type inference is performed on this group, zig may be used at different types, because it has a user-supplied polymorphic signature. However, zag may not, and the example is rejected, unless we add an explicit type signature for zag.
Mark Jones suggested that the dependency analysis should ignore references to variables that have an explicit type signature, and most compilers already implement this. Hence zag does not depend on zig, and we can infer the type
zag :: BalancedTree a -> a
and then go on to successfully check the type signature of zig.
Dependency groups are smaller, and more programs type-check.
- Dependency Analysis in the Haskell 98 Report
- Typing Haskell in Haskell, Mark Jones, Haskell Workshop 1999.
Replace section 4.5.1 with:
In general the static semantics are given by the normal Hindley-Milner inference rules. A dependency analysis transformation is first performed to increase polymorphism.
A variable x depends on a variable y (bound in the same list of declarations) if
1) they are bound by the same pattern binding, or
2) y has no type signature and the binding defining x contains an occurrence of y, or
3) x depends on a variable z that depends on y.
A declaration group is a minimal set of bindings of mutually dependent variables. Hindley-Milner type inference is applied to each declaration group in dependency order.
- also tightens up the original wording, which didn't mention that the declarations had to be in the same list and also defined declaration group but not dependency.
- the transformations formerly listed in this section are no longer always possible.
- The Report sometimes speaks of "value bindings", "value declarations" or "function and pattern bindings". It might be best to standardize on "value bindings".
- Similarly "declaration groups" might more precisely be called "binding groups", since other kinds of declaration are not involved.
- The first paragraph of section 4.5.2 isn't quite right:
- It deals with let's consisting of a single binding, instead of declaration groups. Note that we can no longer assume that a let has a single declaration group.
- It does not seem to deal with functions, non-trivial patterns or recursion.