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.
Compute List.map (bar snd) lst. (* The term "snd" has type "?A0 * ?B0 -> ?B0" while it is expected to have type "nat". *)
(?A * ?B) -> ?B which in the case of
lst would become
(nat * nat) -> nat.
And type of
nat -> nat.
It worked when I tried using
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
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: Jan 29 2023 at 05:03 UTC