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:

enter image description here

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).

enter image description here

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.

Thank you!


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.