[Haskell-cafe] Function Type Calculation (Take 2)
Miguel Mitrofanov
miguelimo38 at yandex.ru
Sun Apr 27 16:39:22 EDT 2008
> [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
More information about the Haskell-Cafe
mailing list