[clean-list] a local function typing question in function composition

[Edsko de Vries]

Hi,

> >Then when it checks the body of f ("y"), it must check that y has
> >type "a", where "a" is the type of the argument passed in (x). This
> >is indeed  a different a, BUT "y" has type "a" *for every a*, so that
> >doesn't matter!
> 
> This is the part that I do not understand. "y" has type "a, for every
> a" but it seems to me that this type is too general. I would have
> thought that "y" needs to have the exact same type as "x".

But it does! In this example, y has every type, and therefore it also
has the same type as x :) See example below.

> Indeed, if you look at the program as a whole, it doesn't make sense,
> because "undefined" could return anything, and thus the actual value
> that "y" gets could  be anything.  I would argue that this example
> actually shows up a problem in the  Clean type system, because the
> caller of "f" wants a value back which is of the same  type as the
> value passed in.

Actually, the point is that undefined won't return anything at all, and
therefore it is safe to assume it has every type. 

> The only reason this "works" (and here I am  using "works" very very
> loosely) is that the function "f" never terminates when called, so it
> is impossible to  actually inspect the returned value. If "f" actually
> returned a value, then this would  clearly be a bug.

No, not really. I am sorry that my use of "undefined" muddled the
waters. Here is a similar example that doesn't use undefined, and does
in fact return a value:

module t

f :: [a] -> [a]
f x = y
    where
        y :: [a]
        y = []

Start = f [1,2,3]

The empty list [] has type "[a]" (list of a) for every a (the empty list is a
list of integers, a list of bools, etc.). Now exactly the same argument holds:
y has type [a] for every a. The signature of f says that the result must have
the type type as the input, but since y has type [a] for every a, that's not a
problem. This program is type-correct and runs (and returns []).

> Never-the-less, from a practical prospective, I have learned the
> following:
> 
>     The type variables used in inner type declarations are ALWAYS
>     different from the type variables in outer type declarations.
> 
> If I remember this rule, I think I can understand and avoid typing
> errors.

Yes, if you find yourself using a type variable in an inner function which you
have also used in an outer function, chances are you are trying to do something
that won't work.

> It would be helpful if the error message
> 
>     Type error [t.icl,6,y]:type variable of type of lifted argument a
>     appears in the specified type
> 
> could be changed to be a little bit more comprehensible. 

I agree, but that's not up to me I'm afraid :)

Edsko