[Haskell-cafe] WG:

[Massimo Zaniboni]

Il 15/08/2018 23:06, Stefan Chacko ha scritto:

>  3. Why do we use clinches in such definitions. I concluded  you need
>     clinches if a function is not associative 
> 
> such as (a-b)+c  . (Int->Int)->Int->Int
> 
> But also if a higher order function needs more than one argument. 
> (a->b)->c .
> 
> Can you please explain it ?

   funXYZ :: Int -> Int -> Int -> Int
   funXYZ x y z = (x - y) + z

if you rewrite in pure lamdda-calculus, without any syntax-sugars it became

   fun_XYZ :: (Int -> (Int -> (Int -> Int)))
   fun_XYZ = \x -> \y -> \z -> (x - y) + z

so fun_XYZ is a function `\x -> ...` that accepts x, and return a 
function, that accepts a parameter y, and return a function, etc...

You can also rewrite as:

   funX_YZ :: Int -> (Int -> (Int -> Int))
   funX_YZ x = \y -> \z -> (x - y) + z

or

   funXY_Z :: Int -> Int -> (Int -> Int)
   funXY_Z x y = \z -> (x - y) + z

and finally again in the original

   funXYZ_ :: Int -> Int -> Int -> Int
   funXYZ_ x y z = (x - y) + z

I used different names only for clarity, but they are the same exact 
function in Haskell.

In lambda-calculus the form

   \x y z -> (x - y) + z

is syntax sugar for

   \x -> \y -> \z -> (x - y) + z

On the contrary (as Francesco said)

   (Int -> Int) -> Int -> Int

is a completely different type respect

   Int -> Int -> Int -> Int

In particular a function like

   gHX :: (Int -> Int) -> Int -> Int
   gHX h x = h x

has 2 parameters, and not 3. The first parameter has type (Int -> Int), 
the second type Int, and then it returns an Int. Equivalent forms are:

   g_HX :: (Int -> (Int -> Int))
   g_HX = \h -> \x -> h x

   gH_X :: (Int -> Int) -> (Int -> Int)
   gH_X h = \x -> h x

   gHX :: (Int -> Int) -> Int -> Int
   gHX_ h x = h x


IMHO it is similar to logic: intuitively it seems easy and natural, but 
if you reflect too much, it is not easy anymore... but after you 
internalize some rules, it is easy and natural again.

Regards,
Massimo