|
|
# Proposal: Relaxed Dependency Analysis
|
|
|
|
|
|
<table><tr><th> Ticket </th>
|
|
|
<th>[\#65](https://gitlab.haskell.org//haskell/prime/issues/65)</th></tr>
|
|
|
<tr><th> Dependencies </th>
|
|
|
<th> none
|
|
|
</th></tr>
|
|
|
<tr><th> Related </th>
|
|
|
<th>[\#103](https://gitlab.haskell.org//haskell/prime/issues/103): [MonomorphicPatternBindings](monomorphic-pattern-bindings)</th></tr>
|
|
|
<tr><th></th>
|
|
|
<th>[\#80](https://gitlab.haskell.org//haskell/prime/issues/80): [MonomorphismRestriction](monomorphism-restriction)</th></tr></table>
|
|
|
|
|
|
## Compiler support
|
|
|
|
|
|
<table><tr><th> GHC </th>
|
|
|
<th> full
|
|
|
</th></tr>
|
|
|
<tr><th> nhc98 </th>
|
|
|
<th> full
|
|
|
</th></tr>
|
|
|
<tr><th> Hugs </th>
|
|
|
<th> full
|
|
|
</th></tr>
|
|
|
<tr><th> UHC </th>
|
|
|
<th> full
|
|
|
</th></tr>
|
|
|
<tr><th> JHC </th>
|
|
|
<th> full
|
|
|
</th></tr>
|
|
|
<tr><th> LHC </th>
|
|
|
<th> full
|
|
|
</th></tr></table>
|
|
|
|
|
|
## Summary
|
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
## Description
|
|
|
# Relaxed Dependency Analysis
|
|
|
|
|
|
|
|
|
|
|
|
In Haskell 98, a group of bindings is sorted into strongly-connected components, and then type-checked in dependency order ([ H98 s4.5.1](http://haskell.org/onlinereport/decls.html#sect4.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](http://haskell.org/onlinereport/decls.html#sect4.5.2)).
|
|
|
|
|
|
|
|
|
|
|
|
Consider
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
data BalancedTree a = Zero a | Succ (BalancedTree (a,a))
|
|
|
|
... | ... | @@ -59,7 +24,9 @@ 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
|
|
|
|
|
|
However GHC, Hugs and Nhc98 follow the suggestion of Mark Jones in [ Typing Haskell in Haskell](http://www.cse.ogi.edu/~mpj/thih/), 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
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
zag :: BalancedTree a -> a
|
... | ... | @@ -69,89 +36,7 @@ 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
|
|
|
|
|
|
- [ Dependency Analysis](http://haskell.org/onlinereport/decls.html#sect4.5.1) in the Haskell 98 Report
|
|
|
- [ Typing Haskell in Haskell](http://www.cse.ogi.edu/~mpj/thih/), Mark Jones, Haskell Workshop 1999.
|
|
|
|
|
|
## Report Delta
|
|
|
|
|
|
|
|
|
Replace the body of [ section 4.5.1](http://haskell.org/onlinereport/decls.html#sect4.5.1)**Dependency analysis**:
|
|
|
|
|
|
>
|
|
|
> In general the static semantics are given by the normal Hindley-Milner inference rules. A *dependency analysis transformation* is first performed to increase polymorphism. 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).
|
|
|
|
|
|
>
|
|
|
> Application of the following rules causes each `let` or `where` construct (including the `where` defining the top level bindings in a module) to bind only the variables of a single declaration group, thus capturing the required dependency analysis: (A similar transformation is described in Peyton Jones' book \[10\].)
|
|
|
|
|
|
> >
|
|
|
> > 1) The order of declarations in where/let constructs is irrelevant.
|
|
|
|
|
|
> >
|
|
|
> > 2) `let` {*d<sub>1</sub>*; *d<sub>2</sub>*} `in`*e* = `let` {*d<sub>1</sub>*} `in` (let {*d<sub>2</sub>*} `in`*e*)
|
|
|
> >
|
|
|
> > >
|
|
|
> > > (when no identifier bound in *d<sub>2</sub>* appears free in *d<sub>1</sub>*)
|
|
|
|
|
|
|
|
|
with:
|
|
|
|
|
|
>
|
|
|
> In general the static semantics are given by applying the normal Hindley-Milner inference rules. In order to increase polymorphism, these rules are applied to groups of bindings identified by a *dependency analysis*.
|
|
|
|
|
|
>
|
|
|
> A binding *b<sub>1</sub>**depends* on a binding *b<sub>2</sub>* in the same list of declarations if either
|
|
|
|
|
|
> >
|
|
|
> > 1) *b<sub>1</sub>* contains a free identifier that has no type signature and is bound by *b<sub>2</sub>*, or
|
|
|
|
|
|
> >
|
|
|
> > 2) *b<sub>1</sub>* depends on a binding that depends on *b<sub>2</sub>*.
|
|
|
|
|
|
>
|
|
|
> A *declaration group* is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order. The order of declarations in `where`/`let` constructs is irrelevant.
|
|
|
|
|
|
|
|
|
Notes:
|
|
|
|
|
|
- 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.
|
|
|
- defining dependencies between bindings is a little simpler than dependencies between variables.
|
|
|
- the dependency analysis transformation formerly listed in this section is no longer always possible.
|
|
|
|
|
|
|
|
|
Replace the first paragraph of [ section 4.5.2](http://haskell.org/onlinereport/decls.html#sect4.5.2)**Generalization**:
|
|
|
|
|
|
>
|
|
|
> The Hindley-Milner type system assigns types to a `let`-expression in two stages. First, the right-hand side of the declaration is typed, giving a type with no universal quantification. Second, all type variables that occur in this type are universally quantified unless they are associated with bound variables in the type environment; this is called *generalization*. Finally, the body of the `let`-expression is typed.
|
|
|
|
|
|
|
|
|
with
|
|
|
|
|
|
>
|
|
|
> The Hindley-Milner type system assigns types to a `let`-expression in two stages:
|
|
|
>
|
|
|
> >
|
|
|
> > 1) The declaration groups are considered in dependency order. For each group, a type with no universal quantification is inferred for each variable bound in the group. Then, all type variables that occur in these types are universally quantified unless they are associated with bound variables in the type environment; this is called *generalization*.
|
|
|
|
|
|
> >
|
|
|
> > 2) Finally, the body of the `let`-expression is typed.
|
|
|
|
|
|
|
|
|
Notes:
|
|
|
|
|
|
- The original 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.
|
|
|
- The original does not deal with functions, non-trivial patterns or recursion.
|
|
|
Dependency groups are smaller, and more programs type-check.
|
|
|
|
|
|
## Terminology issues
|
|
|
|
|
|
- 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. |