Apologies for the delay in responding:
| Mark Jones wrote:
| >
| > Your comment about giving smaller strongly connected components is
| > interesting. I noticed the same thing a couple of years ago, and the
| > Hugs type checker uses this observation to type check some programs
| > that might otherwise be rejected.
|
| Would you mind giving an example of this? Thanks.
Here's a pathological example:
f x = g [x]
g x = f [x]
These two functions are mutually recursive, so their types must be
inferred at the same time. However, a typical computation will
proceed as follows:
f x = g [x] = f [[x]] = g [[[x]]] = f [[[[x]]]] = ...
Thus we can see that f and g are being used in recursive calls at
different types; this conflicts with the requirement of Hindle-Milner
type inference that all recursive uses are at the same type, and hence
a type error occurs.
In Haskell, we can fix this problem by adding a pair of type signatures:
f, g :: a -> Bool
The point I was making is that we can actually get away with less than
this. More precisely, Hugs will allow you to type check this program
given only one type signature declaration. For example, here is the
complete program:
f :: a -> Bool
f x = g [x]
g x = f [x]
Why is this possible? The explicit type signature breaks the dependency
graph as far as type inference is concerned because it means that we don't
need to infer types for f and g at the same time. Instead, we can *assume*
the declared type for f; use that to type check g; *infer* the most general
type shown above for g; and then type check f, ensuring that we really do
get something that has the original declared type for f.
I think this is pretty subtle, but I hope this answers your question.
All the best,
Mark
