Mutually recursive bindings
Tom Pledger
Tom.Pledger@peace.com
Mon, 6 Nov 2000 19:06:01 +1300 (NZDT)
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
> catch22 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 lambdabound,
and FLETV = free variables which will be letbound, 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 lambdabound,
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 letbound, 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 letbound variables until after quantification.
Worth using?
Regards,
Tom