Composition of the VS function Function Application

Question

• Can anyone give an example of function composition?

• Is this the definition of a function composition operator?

  (.) :: (b -> c) -> (a -> b) -> a -> c f . g = \x -> f (gx) 

This shows that it takes two functions and returns a function, but I remember someone expressed logic in English, for example

man-boy → ali is boy → ali is human

• What is this logic related to the composition of functions?
• What is the meaning of strong binding of a functional application and composition, and what is a stronger binding than another?

Please, help.

Thanks.

Answer 1

( Edit 1: I skipped a couple of components of your question for the first time, see the bottom of my answer.)

The way to think about this type of statement is to look at the types. The form of the argument you have is called a syllogism; however, I think you remember something wrong. There are many different types of syllogisms, and yours, as far as I can tell, does not correspond to the composition of functions. Let's look at the kind of syllogism that does:

• If it's sunny, I'll be hot.
• If I feel hot, I’ll go swimming.
• Therefore, if it is sunny, I will go swimming.

This is called a hypothetical syllogism . In logical terms, we will write this as follows: let S stand for the sentence “sunny”, let H stand for the sentence “I will be hot”, and let W stand for the sentence “I will go swimming”, Writing α → β for “α implies β "and the record ∴ for" therefore ", we can translate above:

• S → H
• H → W
• ∴ S → W

Of course, this works if we replace S, H, and W with any any α, β, and γ. It should now look familiar. If we change the implication arrow → to the arrow -> function, it becomes

• a -> b
• b -> c
• ∴ a -> c

And now, we have three components of the composition operator type! To think of it as a logical syllogism, you might think of the following:

• If I have a value of type a , I can create a value of type b .
• If I have a value of type b , I can create a value of type c .
• Therefore , if I have a value of type a , I can create a value of type c .

This should make sense: in f . g f . g existence of the function g :: a -> b tells you that premise 1 is true, and f :: b -> c tells you that premise 2 is true. So you can conclude the final statement for which the function f . g :: a -> c f . g :: a -> c is a witness.

I'm not quite sure what your syllogism means. It is almost an instance of modus ponens , but not quite. The arguments of modus ponens are as follows:

• If it rains, then I can.
• Rain.
• Therefore, I can.

Writing R for "it is raining" and W for "I will be wet", it gives us a logical form

• R → W
• R
• ∴ W

Replacing the implication arrow with the function arrow gives us the following:

• a -> b
• a
• ∴ b

And this is just a function application, as we see from the type ($) :: (a -> b) -> a -> b . If you want to think of it as a logical argument, it can be of the form

• If I have a value of type a , I can create a value of type b .
• I have a value of type a .
• Therefore, I can create a value of type b .

Here we consider the expression fx . The function f :: a -> b witnesses the truth of sentence 1; the value x :: a is a witness to the truth of sentence 2; and therefore the result can be of type b , which proves the conclusion. This is exactly what we found from the evidence.

Now your original syllogism takes the following form:

• All boys are human.
• Ali is a boy.
• Therefore, Ali is a man.

Translate it to characters. Bx will mean that x is a boy; Hx will mean that x is human; a will mean Ali; and ∀x. φ says that φ is true for all values ​​of x. Then we have

• ∀x. Bx → Hx
• IN
• ∴ Ha

It is almost modus ponens, but this requires an instance of forall. Although logically correct, I'm not sure how to interpret it at the type system level; if anyone wants to help, I'm all ears. It was supposed to be a rank 2 type of type (forall x. B x -> H x) -> B a -> H a , but I am pretty sure that this is wrong. Another assumption would be a simpler type like (B x -> H x) -> B Int -> H Int , where Int means Ali, but again, I'm pretty sure that this is wrong. Again: if you know, please let me know too!

And the last note. Looking at things this way - after the connection between evidence and programs - ultimately leads to a deep magic style without dots ; that is, the resulting function has no explicit variables.

You also asked about "strong binding." I think you mean operator precedence . and $ (and possibly also application features). In Haskell, as in arithmetic, some operators have a higher priority than others, and thus bind more tightly. For example, in the expression 1 + 2 * 3 this is parsed as 1 + (2 * 3) . This is because Haskell has the following declarations:

 infixl 6 + infixl 7 * 

The higher the number (priority level), the faster this operator is called and, therefore, the operator is more closely related. A functional application effectively has infinite priority, therefore it is most closely related: the expression fx % gy will be parsed as (fx) % (gy) for any % operator. The operators . (composition) and $ (applications) have the following parity declarations:

 infixr 9 . infixr 0 $ 

Priority levels range from zero to nine, so this suggests that the operator . binds more tightly than any other (except for the function), and $ binds less tightly. Thus, the expression f . g $ h f . g $ h will be parsed as (f . g) $ h ; and for most operators f . g % h f . g % h will be (f . g) % h , and f % g $ h will be f % (g $ h) . (The only exceptions are the rare few other operators with zero or ninth priority.)