Re: Question about notation

To: jr hindley <majrh@uk.ac.swan.pyr>
Subject: Re: Question about notation
From: Andrew Pitts <Andrew.Pitts@uk.ac.cam.cl>
Date: Tue, 03 Nov 92 09:05:03 +0000
Approved: types@dcs.gla.ac.uk

[The previous message from Andy Pitts was truncated by mistake.  Here is the
correct message.  Apologies for the error.  -- Phil Wadler, Moderator]

>A question on notation: Is there a standard or near-
>standard notation for a set of type-statements of form
>
>  x1 has type tau-1, x2 has type tau-2,...,xn has type tau-n ?
>
>I have heard these sets sometimes called a BASIS, sometimes an
>ENVIRONMENT, sometimes a CONTEXT, etc. Any consensus?

Personally, I tend to use the word "context", as I think do many
others. However in the context (!) of programming language semantics,
this usage clashes inconveniently with the use of the word "context"
to mean an "expression with holes".  Consequently, in courses I've
taught on types and semantics, I've tried using the expression "type
assignment" (quite logical, since one is assigning types to
identifiers), which I believe I picked up from John Mitchell. I guess
if \Gamma is such a type assignment, then

\Gamma |- M has type tau

should be called a "typing assertion", or to be more Swedish, a "typing
judgement".

Andy Pitts