Mark P Jones writes:
[...]
In general, I think you need to know the types to determine what transformation is required ... but you need to know the transformation before you get the types. Unless you break this loop (for example, by supplying explicit type signatures, in which case the transformation isn't needed), then I think you'll be in a catch-22 situation.
Why do you need the type to determine the transformation? Here's another example to illustrate the point:
h x = (x==x) || h True || h "hello"
Before looking at this example, I was gearing up to protest that the transformation was cued simply by scope, but now I see that it was cued by scope *and* not foiled by type. So, I withdraw the transformation idea, but instead suggest that a similar improvement in inferred polymorphism can be achieved by making the type checker more circumspect (lazy?) about when it performs some unification. For example, with FLAMV = free variables which will be lambda-bound, and FLETV = free variables which will be let-bound, and ! marking the alleged innovations: h = \x -> (x==x) || h True || h "hello" - a; FLAMV: x::a -- Eq b => b -> b -> Bool --- (Substitute b for a) Eq b => (b -> Bool; FLAMV: x::b) - ! (Because x will be lambda-bound, go ahead and unify the types of its uses now) Eq b => (b; FLAMV: x::b) ---- Eq b => (Bool; FLAMV: x::b) -- Bool -> Bool -> Bool -------- Eq b => (Bool -> Bool; FLAMV: x::b) _ c; FLETV: h_1st::c ---- Bool ------ (Substitute Bool -> d for c) d; FLETV: h_1st::Bool -> d -- Bool -> Bool -> Bool --------- (Substitute Bool for d) Bool -> Bool; FLETV: h_1st::Bool -> Bool - ! (Because h is let-bound, do not attempt ! to unify the types of h_1st and h_2nd) e; FLETV: h_2nd::e ------- [Char] --------- (Substitute [Char] -> f for e) f; FLETV: h_2nd::[Char] -> f ------------------- (Substitute Bool for f) Bool; FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool ---------------------------- Eq b => (Bool; FLAMV: x::b; FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool) ----------------------------------- Eq b => (b -> Bool; FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool) --------------------------------------- (Tentatively give h its quantified type) h :: forall b . Eq b => b -> Bool ! (Discharge the h_1st requirement, by unifying Bool -> Bool ! with a fresh instance of forall b . Eq b => b -> Bool) ! (Discharge the h_2nd requirement, by unifying [Char] -> Bool ! with another fresh instance of forall b . Eq b => b -> Bool)
[...] This also throws up another issue; with polymorphic recursion, you might need an *infinite* family of specialized functions. Consider the following example:
r x = (x==x) && r [x]
This also yields to the above technique of deferring unification for uses of let-bound variables until after quantification. Worth using? Regards, Tom