Fwd: [Haskell-cafe] Point-free style

[shiqi cao]

---------- Forwarded message ----------
From: shiqi cao <shiqicaoml at gmail.com>
Date: Sun, 13 Feb 2005 21:25:56 -0500
Subject: Re: [Haskell-cafe] Point-free style
To: Tim Docker <timd at macquarie.com.au>


On Mon, 14 Feb 2005 11:24:12 +1100, Tim Docker <timd at macquarie.com.au> wrote:
> Ketil Malde wrote:
>
>   >        (.) . (.) .(.)
>   >
>   > I entered it into GHCi, and got
>   >
>   >         :: forall a a b c a.
>   >               (b -> c) -> (a -> a -> a -> b) -> a -> a -> a -> c
>
> I spent a minute or so attempting to intuit the type signature of this,
> before cheating and entering it into ghci also.
>
> Is there a straightforward technique by which type signatures can be
> "hand calculated", or does one end up needing to run the whole inference
> algorithm in one's head?

Hi Ketil,

I think the type signatures can be derived by hand.

First let us take a look the type of (.)

(.) :: forall c a b. (b -> c) -> (a -> b) -> a -> c

one thing need to be taken into account is  (.) is left associative,
but composition of two functions , like f(g(x)),  brings the inner
function into our mind first intuitively.

Since we know the type of (.) calculating the (.).(.) is algebra
manipulation, but be careful.

The left hand (.) and right hand (.) are not identical in terms of
type. Let us call the left one (.)_1, right one (.)_2 and the middle
one (.)_3. Let us type (.)_2 first since the type of (.)_1 is based on
(.)_2

(.)_2 :: (b -> c) -> (a->b) -> (a -> c)
             ----X----       ---------Y----------

Let X =  (b -> c) and Y = (a->b) -> (a -> c)

(.)_2 :: X -> Y

Then (.)_3 must be (Y -> Z) -> (X -> Y) -> (X -> Z)

Then (.)_2 must be (Y -> Z)

Since (.)_3 is derived (.).(.) has type (X->Z), we need to find out what Z is.

        (.)_2 :: (Y -> Z)
=>  (.)_2 :: ((a->b) -> (a -> c)) -> Z   [1]

        (.) :: forall C A B. (B -> C) -> (A -> B) -> (A -> C)
=>  (.)_2 :: ((a->b) -> (a -> c)) -> (d -> (a -> b)) -> (d -> (a -> c))   [2]
There d is an arbitrary type.

        [1] and [2]
=>  Z = (d -> (a -> b)) -> (d -> (a -> c))
=>  (.).(.) :: (X -> Z) = (b -> c)  ->  (d -> (a -> b)) -> (d -> (a -> c))

GHCi result is
(.).(.) :: forall a b c a1.
           (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c


Shiqi Cao