I'm not sure if this is the correct place to ask this kind of a question, but here goes:
I'm doing my own reading of the Principles of Program Analysis book, and i'm having trouble understanding some priciples from Chapter 5 - Type and Effect Systems.
In the book (page 286) there is an example:
I can not understand, why do they start with the expression funF f x => ... Is this maybe guessing the values of the types of the bound variables f and x, we just assume that f is of type function that takes a function and returns a function, and that x is of type function (because it seems about right)?
After that we have to determine the type of the function body, so we move to f (fnY y => y). From the assumed types, we infer the type f (the top bottom rule in the image), and then we move to: fnY y => y, and it is streightforward that the type of that expression is t -> t (a function that returns the same type that it was given).
Now that we know this, we can determine the type of the function application f (fnY y => y) as t -> t.
Then again we move up to determine the type of funF ... which accoring to the rules for recursive functions is streight-forward (the same type as for f in the assumed typed enviroment)..
Then we move to the in body: g (fnZ => z). g's type has already been determined immediatly above, so we move to fnZ => z which is the same as for fnY. And in the end we get that the whole expression has the type: t -> t.
What i'm asking is: is this the correct trail of thought? Or i'm i missing the point somewhere?
I'm not sure about the guessing part, why did we start where we did, why not more simply with variable y or somewhere else? The rest of the chapter heavily depends on the proper understanding of these concepts, and i would like to understand this.
In general, I would be grateful if somebody could point me out to a book or something that, in more details explains type systems.