Why is this function type-correct

[Jon Fairbairn]

"Rijk J. C. van Haaften" <rjchaaft@cs.uu.nl>
wrote:
> Recently, I wrote a function similar to
> =

> x :: a
> x =3D x 42
> =

> which is type-correct (Hugs, Ghc, THIH).
> Still, from the expression it is clear
> that the type shoud have a function type.
> The definition
> =

> x :: a -> b
> x =3D x 42
> =

> is equally well accepted, though I can't
> see why this type would be correct. (I'd
> expect it to be too general.)
> =

> For what reasons are these types considered
> correct?

When you say

x :: a

you are asking that the compiler check that everything you
say about x is consistent with x being acceptable where
/any/ type is required.

In the application x 42, it requires that x be a function,
which is fine, because x has any type, and this includes
functions. When you say x =3D x 42, this requires that the
type returned from x 42 is the same as the type of x, again
fine because if x::a, then x:: Integer -> a also, so x 42:: a.

It works out in practise because x =3D x 42 gives x the value
bottom, and bottom::a for all a.
 =


  J=F3n

-- =

J=F3n Fairbairn                                 Jon.Fairbairn@cl.cam.ac.u=
k
31 Chalmers Road                                         jf@cl.cam.ac.uk
Cambridge CB1 3SZ            +44 1223 570179 (after 14:00 only, please!)