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

[Philip Matthews]

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

> On Thu, Apr 12, 2007 at 10:07:05AM -0400, Philip Matthews wrote:
>>
>> On 12-Apr-07, at 09:57 , Edsko de Vries wrote:
>>
>>> Hey,
>>>
>>>> Does this mean that it is illegal in Clean to use type variables
>>>> from an outer function definition in an inner function  definition?
>>>
>>> No, not really. It's just that all type variables are implicitly
>>> quantified by a "forall" (just like in Haskell, I might add). So,  
>>> for
>>> example, the following code is perfectly fine, albeit a bit  
>>> contrived:
>>>
>>> module t
>>>
>>> f :: [a] -> [a]
>>> f xs = ys
>>>    where
>>>        ys :: [a]
>>>        ys = []
>>>
>>> Start = f [1,2,3]
>>>
>>> Again, the type annotation on "ys" says that "ys" has type "[a]"
>>> for all a (and
>>> it does, because the empty list has that type).
>>
>> Would I be correct in saying that type variable "a" in "f:[a]->{a]"
>> is completely distinct
>> from type variable "a" in "ys::[a]", even though they have the same
>> name?
>
> Yes, that is correct, because they are both bound by a forall. What  
> that
> definition really says is
>
> f :: forall a. [a] -> [a]
> f xs = ys
>     where
>         ys :: forall a. [a]
>         ys = []
>
> Edsko

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?

- Philip