Why isn't (b) of (a -> (b -> c)) the first parameter in the function definition but the s-CodePudding

If first parameter is taken by the function first as function application is left-associative, for example:

drop 2 [1,2,3,4]

result: [3,4]

is equivalent to

(drop 2) [1,2,3,4]

same result: [3,4]

Here my question is, if the type signature is right-associative, which means, things in right side evaluate first, in this case, it's gonna be as follows, as the first parameter is first taken by the function:

drop :: [1,2,3,4] -> (2 -> [3,4])

It shouldn't have been as follows, right?

drop :: Int -> ([a] -> [a])
drop :: 2 -> ([1,2,3,4] -> [3,4])

So, why does it take the second parameter first in type signature of the function instead of the first parameter?

In addition, if the second parameter is evaluated prior to first parameter, then why is the following usage invalid?

(drop [1,2,3,4]) 2

CodePudding user response：

It's nonsensical to write things like drop :: [1,2,3,4] -> (2 -> [3,4]) or 2 -> ([1,2,3,4] -> [3,4]) – you're mixing type-level and value-level notations there. What you should instead do is look at local types of subexpressions:

drop                  2    [1,2,3,4]
└─┬┘                  ┊    └──┬────┘
┌─┴───────────────┐ ┌─┴─┐  ┌──┴──┐
│Int->[Int]->[Int]│ │Int│  │[Int]│
└─────────────────┘ └───┘  └─────┘

Add the implied parentheses

(drop                   2)    [1,2,3,4]
 └┬─┘                   ┊     └──┬────┘
┌─┴─────────────────┐ ┌─┴─┐   ┌──┴──┐
│Int->([Int]->[Int])│ │Int│   │[Int]│
└───────────────────┘ └───┘   └─────┘

Now the subexpression drop 2 means you're applying the argument 2 as the first argument of the function drop, i.e. as the Int in its signature. For the whole drop 2 expression, this argument has therefore vanished:

(           drop           2   )  [1,2,3,4]
┊  ┌──────────┴────────┐ ┌─┴─┐ ┊  └──┬────┘
┊  │Int->([Int]->[Int])│ │Int│ ┊     ┊
┊  └───────────────────┘ └───┘ ┊     ┊
└────────────┬─────────────────┘  ┌──┴──┐
        ┌────┴───────┐            │[Int]│
        │[Int]->[Int]│            └─────┘
        └────────────┘

This is analogous to applying the single-argument function length :: [Bool] -> Int to the single argument [False,True] :: [Bool] to get the result length [False,True] ≡ (2::Int). The fact that for drop the result has type ([Int]->[Int]) instead of something “atomic” like Int is irrelevant at this stage.

Then on the outer level, you're applying the function of type [Int]->[Int] to the argument of type [Int], which is perfectly sensible. The whole thing then has simply result type [Int].

( (           drop           2   )  [1,2,3,4] )
┊ ┊  ┌──────────┴────────┐ ┌─┴─┐ ┊  └──┬────┘ ┊
┊ ┊  │Int->([Int]->[Int])│ │Int│ ┊     ┊      ┊
┊ ┊  └───────────────────┘ └───┘ ┊     ┊      ┊
┊ └────────────┬─────────────────┘     ┊      ┊
┊         ┌────┴───────┐            ┌──┴──┐   ┊
┊         │[Int]->[Int]│            │[Int]│   ┊
┊         └────────────┘            └─────┘   ┊
└────────────────────────┬────────────────────┘
                      ┌──┴──┐
                      │[Int]│
                      └─────┘

CodePudding user response：

I think you misunderstand what right associative means. It indeed means that:

drop :: Int -> [a] -> [a]

is equivalent to:

drop :: Int -> ([a] -> [a])

This thus means that drop is a function that takes a parameter of type Int, and then returns a function of type [a] -> [a].

But function application itself is left-associative. Indeed:

drop 2 [1,2,3,4]

is short for:

(drop 2) [1,2,3,4]

Here drop 2 will thus return a function of type [a] -> [a] that will drop the first two items of the list. We then apply [1,2,3,4] to that function, and thus obtain [3,4].

CodePudding user response：

I guess I've understood the puzzle now:

In a function application, the function will always take parameters from left to right, one by one, as it's left-associative.

Now, when it comes to type signature of the function, it's right-associative indeed, but it doesn't mean the function will be applicated by taking the last argument, then the second last argument, and so forth.

Nope, the function will still take the first argument and generate the second function that takes the second argument and so forth.

For example:

Original lambda version

  (λa.a(λb.b)) (1,2)
= (a(λb.b)[a:=1]) (2)
= (1(λb.b)) (2)
= 1(b)[b:=2]
= 1(2)

Curried lambda version

  λab.ab (1,2)
= λb.ab[a:=1] (2)
= λb.1b (2)
= 1b[b:=2]
= 1(2)

After the substitutions of the bound variables with parameters are complete, it starts the actual evaluation process:

(1(2)) = 3

The evaluation will start from the last generated function(Inner most generated function), as what arithmetic does. Otherwise, the final result is incorrect as if the evaluation starts conversely. As the order of type signature actually means arithmetic or evaluation order but not the function application.

The job of function application is to replace the bound variables with their parameters, as it's unrelated from the evaluation order from type signature.

Note: Terms or logic of this post may be incorrect, I'll correctly this very soon, as I'm tired and need to go to sleep. sorry I should post this tomorrow. If you are able to and wish, you could edit my post to correct it. :)