Full-Name: Joshua D. Guttman
Posted-Date: Mon, 1 Apr 91 15:53:06 -0500
Date: Mon, 1 Apr 91 15:53:06 -0500
From: guttman@org.mitre.linus
Message-Id: <9104012053.AA01011@malabar.mitre.org>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: guttman's message of Thu, 21 Mar 91 12:33:30 EST
Subject: Re: semantics of polymorphic operators

Thanks for the replies about the semantics of HOL polymorphism.  I find it
gratifying that, when I ask a question on this mailing list, I get replies
indicating that people have already recognized and thought through the issues,
and have written down their thoughts.  Moreover, it's available by ftp.

The set-theoretic semantics developed by Andy Pitts is (in my opinion) clever
and attractive.  If I may summarize, the heart of the matter is that
expressions (in their "real, canonical" form) have type indicators attached to
them (and their subexpressions).  Thus a polymorphic constant such as cons is
not a closed expression, but rather contains the free type variable 'a
representing the putative type of the list elements.

For this reason, it is natural that the denotation of cons be not a function of
its two arguments (i.e. the car and cdr), but rather a function which takes an
assignment of closed denotations to its free (type and normal) variables.  Only
after values have been assigned to the free variables (of the two kinds) do we
get a function which applies to the car and cdr to construct the list.

If cons had been a *closed* expression, then one would have wanted its
denotation to be a function that takes the car and cdr to construct the
(enlarged) list.  And in this case there would have been trouble, as a
syntactically well formed (and apparently closed) expression like

 cons(cons, nil)                (*)

would indicate that the denotation of cons must be a function that should be
defined when given itself as an argument.

Of course approaches to semantics in which this is possible are well worked
out.  BUT they are unappealingly far from the normal semantics for simple type
theory, and it would strike me as a bad idea to introduce all that complex and
alien machinery just to graft a syntax for polymorphism onto simple type
theory.

However, because type variable appear free in polymorphic expressions, this is
unnecessary.  The two occurrences of the word "cons" in (*) do not denote the
same value, as the outer occurrence is `one type up' from the inner occurrence.
Thus for any selection of a set of values for the free type variable 'a, the
two occurrences, denote different functions.  Nothing special need be done to
allow the outer one to apply meaningfully to the inner one.

I suppose I should add that this approach to the semantics of polymorphism
seems to me not so radically contrary to Russell's "typical ambiguity" idea.  I
would expect the connection to go like this, when we focus for simplicity just
on a formula F with no free ordinary (non-type) variables.  Then the
Pitts-style denotation of F is just a function that parametrizes the values
that F takes when the ambiguous types are filled in.  So in particular, when
the Pitts-style denotation of F is a constantly True function, then F is a
typically ambiguous theorem.  Does this seem plausible?

        Josh