wiki:RelaxedDependencyAnalysis

Version 6 (modified by ross@…, 8 years ago) (diff)

--

Relaxed Dependency Analysis

Brief Explanation

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

Consider

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.

However GHC, Hugs, Nhc98, and jhc follow the suggestion of Mark Jones that the dependency analysis should ignore references to variables that have an explicit type signature. 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.

References

Tickets

#65
RelaxedDependencyAnalysis

Proposal

Modify the definition of dependency group in the above section to

Two variables bound by value declarations are in the same declaration group if either

1) they are bound by the same pattern binding, or

2) their bindings are mutually recursive (perhaps via some other declarations that are also part of the group), ignoring uses of variables that have an explicit type signature

The semi-formal rules in the rest of the section would have to go: it would no longer be possible to make binding groups explicit with a source-to-source transformation.