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

[Philip Matthews]

Edsko:

Thanks for the long message.
See my detailed comment inline.

- Philip

On 12-Apr-07, at 10:54 , Edsko de Vries wrote:

> Hi Philip,
>
>> So, going back to the  original example
>>      f :: a -> a
>>      f x = y
>>          where
>>              y :: a
>>              y = x
>>
>>      Start = f 5
>>
>> Here the error really is that the compiler cannot unify the type of
>> "y" in the expression "f x = y" with the type of "y" from the type
>> declaration "y :: a", because the "a"s are actually different type
>> variables. They are different type variables, but they need to be the
>> same in order to type check the function.
>>
>> Am I correct?
>
> No, not quite, but close :-) Let me illustrate with a slightly  
> modified
> example:
>
> module t
>
> undefined :: z
> undefined = undefined
>
> f :: a -> a
> f x = y
>     where
>         y :: a
>         y = undefined
>
> Start = f 5
>
> I'm declaring a term "undefined", which is simply defined to be  
> itself. The
> point is that "undefined" has every type. That's what the type  
> annotation says
> for undefined: the type of undefined is "z" *for every z*.
>
> This definition of f (which is identical to the previous, except  
> that I defined
> y to be "undefined" rather than "x") is accepted by the compiler. Why?
>
> The annotation of "y" says that y has type a *for every a*. It checks
> the definition of y, and finds that it is defined to be  
> "undefined"; it
> looks up the type of undefined, finds that undefined has type x *for
> every x* and thus accepts the type annotation.
>
> 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".

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.

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.



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.


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. Before this   
conversation,
I had no idea what this message meant, and even now I can only  
vaguely interpret it.


> We could just as well have written:
>
> f :: a -> a
> f x = y
>     where
>         y :: b
>         y = undefined
>
> and nothing would change. Now when we go back to the original example,
>
> f :: a -> a
> f x = y
>     where
>         y :: a
>         y = x
>
> the type error is *not* in the body of, but in the body of y. The  
> body of y
> says that y must have type a *for every a*, but in fact, y only has  
> one type,
> that is, the type of the argument passed in (x). Unfortunately,  
> since Clean
> doesn't have scoped type variables, we cannot write that down, but  
> internally
> the typechecker will have assigned a type variable "T" to  
> correspond to the
> type of x. Because y is defined to be x, Y will also have type "T".  
> The type
> annotation of "y" says that y has every type you want it to have,  
> but that's
> not the case (it has type T, and only type T).
>
> Again, this program is *exactly* the same program as
>
> f :: a -> a
> f x = y
>     where
>         y :: b
>         y = x
>
> which is rejected for the same reason (now y has type b *for every  
> b*, but that
> is of course the same type as type a *for every a* -- although  
> perhaps it is
> easier to see that this program is wrong).
>
> Does that help?
>
> Edsko