From: Mike Fourman <mikef@uk.ac.ed.lfcs>
Date: Mon, 25 Mar 91 10:28:06 GMT
Message-Id: <8201.9103251028@subnode.lfcs.ed.ac.uk>
To: guttman@org.mitre.linus
Subject: Re: semantics of polymorphic operators
Cc: cbj@uk.ac.ed.lfcs, dts@uk.ac.ed.lfcs, info-hol@edu.uidaho.cs.ted, 
    jhm@uk.ac.ed.lfcs, simon@uk.co.ahl

>From mikef@edinburgh.lfcs Sat Mar 23 01:04:44 1991
>To formalise all this a little more; for each term whose type has type
>variables a_0 ... a_{n-1}, we define an interpretation in any Boolean
>Topos with NNO equipped with an interpretation of the type variables
>(as objects of the topos). These interpretations commute with change
>of interpretation of the type variables along logical morphisms.

Sorry, this was written off-the-cuff and too hastily; I should have
written, 'for each term involving type variables' (rather than '... whose
type has type variables'). The point is that when we quantify a logical
variable - and possibly remove type variables from the type, we should
still insist that the term be interpreted only relative to
interpretations that also cover these 'hidden' type variables. Types
should thus be decorated with lists of type variables, these include, but
must sometimes exceed, the variables explicit in the type.

Consider, for example,

\forall x: 'a . x = x

this is a term (of type bool) whose interpretation depends on the 
interpretation of the type 'a.

>
>In particular, any term has a generic interpretation in a (chosen, but
>--because of the coherence indicated in the previous sentence--
>arbitrary) topos obtained by adjoining indeterminate objects to
>represent the necessary type variables. I believe these are the
>denotations you seek.

The important point is to notice that _proofs_ don't need to be
decorated (with yet more lists of type variables), because change of
interpretation to include new type variables reflects truth. If \tau
has a proof (that may involve terms involving type variables other than
those involved in \tau) then the interpretation of \tau must be true:
first, by induction on the proof, in a topos with sufficient generic
types to interpret each step in the proof; second, by reflection, in
any topos with sufficient generic types to interpret the term.

Mike