From: Mike Fourman <mikef@uk.ac.ed.lfcs>
Date: Fri, 22 Mar 91 16:45:16 GMT
Message-Id: <4563.9103221645@subnode.lfcs.ed.ac.uk>
To: guttman@org.mitre.linus
Subject: Re: semantics of polymorphic operators
Cc: info-hol@edu.uidaho.cs.ted

>From guttman@org.mitre.linus Thu Mar 21 19:46:36 1991
>I'm looking for a citation (or else an off-the-cuff explanation) for the
>semantics of HOL polymorphism.  I know that lots has been written about the
>syntax of polymorphism (typing algorithms etc.), but I'm in the dark about the
>(formal) meaning of them.
>
>[Note:  I'm asking about the polymorphic operators in the HOL formal logic
>rather than those in ML.]  
>
>That is to say, given a model for the polymorphism-free part of an HOL-theory,
>can we find objects that are the denotations of polymorphic constants such as
>cons, pair, composition (of functions), etc.?
>
>There are of course two main lines of response (namely yes and no).  The "yes"
>response would assert that we can construct denotations for the polymorphic
>operators "above" the given model. 

The answer is, 'Yes'.

Simply-typed classical logic can be modelled in any Boolean Topos, B,
with Natural Number Object. 

The theory 'Boolean Topos with Natural Number Object' is essentially
algebraic, so we can form algebraic extensions of models of the theory
by adjoining indeterminates. In particular, we can adjoin an object
freely to obtain an 'extension', B[X]. There is a unique morphism from the
original topos to the extension, morphisms from B[X] to B correspond to
objects in B (and correspond to substituting for the formal object, X).

The appropriate morphisms of topoi, logical morphisms 'under B',
preserve the interpretation of type theory.

Terms whose types have one type variable, 'a, can be interpreted in 
B[X]. To deal with more variables, we make successive extensions;
morphisms between these (and between these and B) correspond to type 
substitutions.

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.

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.


We can use the same ideas to represent the type of parameterisation
provided by SML modules (by adjoining an indeterminate structure of a
given signature these may be viewed algebraically as _generators_), and
by ExtendedML modules (by adding axioms, viewed algebraically as
relations).


Note that the full SML type system cannot be so easily modelled, as
many ML datatypes are inconsistent with classical logic.

-------------------------------------------------------------------------------
Prof. Michael P. Fourman                     email        mikef@lfcs.ed.ac.uk
Dept. of Computer Science                    'PHONE (+44) (0)31-650 5198 (sec)
JCMB, King's Buildings, Mayfield Road,              (+44) (0)31-650 5197
Edinburgh EH9 3JZ, Scotland, UK                 FAX (+44) (0)31 667 7209
-------------------------------------------------------------------------------