Stream: Coq users

Topic: Composition of 2 functions


view this post on Zulip Julin S (Dec 07 2021 at 03:45):

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?

view this post on Zulip Paolo Giarrusso (Dec 07 2021 at 06:08):

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

view this post on Zulip Ali Caglayan (Dec 08 2021 at 10:35):

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: Jan 29 2023 at 05:03 UTC