How can we obtain the composition of two functions for use with `List.map`

? Do we always have to use `compose`

or can we use function application with parenthesis?

I was trying to apply the `List.map`

function to a list of tuples (2 nats each) like

```
Definition lst := [(1,10); (2,20); (3,30)].
Definition bar (n : nat) := n + 100.
```

I wanted to take the second element of each tuple and apply the `bar`

function on it to produce a new list.

I tried

```
Compute List.map (bar snd) lst.
(*
The term "snd" has type "?A0 * ?B0 -> ?B0" while it is expected to have type
"nat".
*)
```

Type of `snd`

is `(?A * ?B) -> ?B`

which in the case of `lst`

would become `(nat * nat) -> nat`

.

And type of `bar`

is `nat -> nat`

.

It worked when I tried using `compose`

from `Coq.Program.Basics`

.

```
Compute List.map (compose bar snd) lst.
(*
= [110; 120; 130]
: list nat
*)
```

Is function composition not possible by simply writing them together? Do we always need `compose`

?

Indeed, function composition is compose and not application; the type signature of compose describes exactly the job of composition.

`compose`

exists for proof search. i.e. for typeclass search to be able to recognise a specific composition and find instances that way. You can also write `fun x => bar (snd x))`

for that function.

Last updated: Sep 30 2023 at 05:01 UTC