Excessive explanation, part fifteen

All right, we are getting through section four of this paper. Today: what is an "environment"?

Now let Env = Id a' V be the domain of environments I. 

Just to be clear, this is not a function in the Exp language. This is a formal description of part of the runtime engine of the Exp language. Basically we are saying here that an "environment" is simply the part of the runtime of an implementation of the language that takes identifiers and maps them onto their values. And that just as we'll use If for type schemes and I for type variables, we'll use I for environments.

You're so accustomed to using environments that they are like the air you breathe; you don't even think about it. When you're writing a program in some language and you say x = y + z;, you're saying "obtain the values associated with identifiers y and z from the environment, add them, and modify the environment so that next time we ask, x has that value". We can characterize the accesses to y and z as the environment being a function that takes "y" or "z" and returns their values. We can characterize the assignment to x as being the construction of a new environment based on the previous environment.

The semantic function I : Exp a' Env a' V is given in [5]. 

Again this is not an function in the Exp language; this is again a formalization of the runtime engine.

Remember that in our notation, a function of two arguments is notated as a function of one argument that returns a function of one argument. So what we're saying here is that the "semantic function" is a function that takes an expression and an environment and produces a value.

Again, this is making formal the basic operation of a runtime. The runtime has a bunch of expressions and the values of all the variables, and it evaluates the expressions in the context of the environment.

Using it, we wish to attach meaning to assertions of the form A a e:Ifwhere e a Exp and A is a set of assumptions of the form x:If, xaId.

This right here is the mission statement of this paper.

The double-turnstile means "the thing on the right is a logical consequence of the thing on the left".

What we're saying here is: we have (on the left) a set of judgments (called "assumptions" here) where all the expressions are identifiers. Say:

x:intsquare:int a' intidentity:aI^2(I^2 a' I^2)

We have on the right an arbitrary expression with a typing judgement, say

Iy.identity (square x) : aI^2(I^2 a' int)

I hope you agree that if we assume that x is an int, square is a function from int to int, and identity is an identity function, that the lambda given is a function that takes any type and returns an int. The assumptions on the left are sufficient to deduce that the judgment on the right is correct (if the assumptions are correct, of course).

The goal of this paper is to provide an algorithm which, given the facts on the left and the expression on the right, deduces the type schema on the right in a manner that allows us to confidently say that yes, we have sufficient evidence on the left to make this judgment on the right.

(Aside: is it possible to have a function with type scheme aI^2(I^2 a' I^2) that is not an identity function? Ponder this!)

If the assertion is closed, i.e. if A and If contain no free typevariables, then the sentence is said to hold iff, for every environment I, whenever I axa:If', for each member x:If' of A,it follows that I aea I:If. 

OK, we've got some jargon and some notation here used without introduction.

First of all, "the assertion" and "the sentence" are being used interchangeably here. We are "asserting" that the assumptions about typed identifiers on the left are sufficient evidence to deduce the type of the expression on the right.

Second, remember when we abused the Exp function notation to say that an environment was a function Id a' V? You would think then that we would continue to abuse that notation and say that given an environment I and an identifier x we would say that the value of x was I x. And is what we do, but to call out that x is being used here as an identifier rather than standing in for a value, we "quote" it with funny brackets. So the value of identifier x in environment I is notated I axa.

Similarly for the semantic function I. It takes two things: an expression e and an environment I, and to emphasize that the expression is an expression of the Exp language, we bracket it as well. So I aea I is "the value of expression e when evaluated in environment I".

So what the heck is this jargon-filled paragraph actually saying? We have a bunch of identifiers with types on one side, and the statement that this implies that expression on the other side has a particular type. The paragraph is saying that this means: choose any possible environment that has those identifiers having some values of the given types. No matter what environment you chose, evaluating the expression in that environment gives a value that matches the expression's type.

That might be too abstract still. In our example:

x:int, square:int a' int, identity:aI^2(I^2 a' I^2) a Iy.identity (square x) : aI^2(I^2 a' int)

We're saying that no matter what integer we choose for x, no matter what function from int to int "square" really is, and no matter what function matching its type scheme "identity" really is, we know that evaluating the expression on the right will produce a function from something to int. There is never any combination of values for the environment that would cause that expression to evaluate to something else.

Further, an assertion holds iff all its closed instances hold.

That's maybe not so clear but fortunately there is an example in the paper:

Thus, to verify the assertion x:I, f: aI^2(I^2 a' I^2) a (f x): Iit is enough to verify it for every monotype I1/4 in place of I.This example illustrates that free type variables in an assertionare implicitly quantified over the whole assertion, while explicitquantification in a type scheme has restricted scope.

What we're getting at here is that this is not the same as saying

 x:aI I, f: aI^2(I^2 a' I^2) a (f x): I

Because that scopes the alpha to just the type of x, but we want that alpha to be still "in scope" on the right hand side of the double turnstile. Basically it is saying that the assertion is logically:

 aI ( x:I, f: aI^2(I^2 a' I^2) a (f x): I )

All right, that gets us through section four! The last paragraph in section four lays out what is going to happen in the rest of the paper:

The remainder of this paper proceeds as follows. First we presentan inference system for inferring valid assertions. Next we present an algorithm W for computing a type scheme for any expression, underassumptions A. We then show that W is sound, in the sense that any type-scheme it derives is derivable in the inference system. Finallywe show that W is complete, in the sense that any derivable type-scheme is an instance of that computed by W.

Next time: A notation for making chains of logical inferences, and another kind of turnstile.