Paul aquagnu at gmail.com
Thu Aug 16 04:53:30 UTC 2018

```Hmm, very interesting question, really: what is the "->" in functions
signatures: type-level operator or syntax only?

16.08.2018 01:20, Massimo Zaniboni wrote:
> 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
>
> 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
> _______________________________________________