# 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
> 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

```