[Haskell-cafe] Function Type Calculation (Take 2)

[Miguel Mitrofanov]

> 			[1]
> funk f x = f (funk f) x
>
> 	f :: a
> 	x :: b
> 	funk f x :: c
> therefore funk :: a -> b -> c
>
> 		RHS
> 	f (funk f) x :: c
>
> 	f (funk f) :: d -> c
> 	x :: d
>
> 	f :: e -> d -> c
>
> 	funk :: h -> e
> 	f :: h
>
> 		unification
> 	f :: a = h = (e -> d -> c)
> 	x b = d

No. x :: b = d (a typo?)

Don't forget also that

funk :: a -> b -> c = h -> e,

which means that e = b -> c

> therefore funk :: ((h -> e) -> b -> c) -> b -> c

No. I don't understand where you've got this expression from. It's

funk :: a -> b -> c = (e -> d -> c) -> b -> c = ((b -> c) -> b -> c) - 
 > b -> c

According to GHCi:

Prelude> let funk f x = f (funk f) x
Prelude> :t funk
funk :: ((t1 -> t) -> t1 -> t) -> t1 -> t

which is about the same.

> 			[2]
> w f = f f

Can't be typed in Haskell.

> Assigning Types
> 	f :: a
> 	w f :: b
> therefore w :: a -> b
>
> 		RHS
> 	f f :: b
>
> 	f :: c -> b
> 	f :: c
>
> 	f :: a = b = c = (c -> b)

And that's why. It can't happen that c = c -> b. Ever.

Prelude> let w f = f f
<interactive>:1:10:
     Occurs check: cannot construct the infinite type: t = t -> t1