Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: type inference
Message-Id: <93Jan13.023957met.8121@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 13 Jan 1993 02:39:50 +0100


Ching Tsun writes

> HOL88 apparently assumes the first i and j are of type :num
> because the second i and j are.  However,

>     "(\i' j'. (\i j. i > j))"

> does not parse.  Yet another peculiarity of HOL88.

Yuk. No doubt it works though.

Victor writes, by way of explanation

> ... since the type checker uses the heuristics that all variables in a term
> with the same name have the same type." **

> If this heuristic was not used then the term "\x.x+1" could be
> i) \x:num.x+1
> ii) \x:bool.x+1
> iii) \x:*.x+1 
> etc.
> making it a real pain to write any term.


Not so. In `\x.x+1` the two occurrences of "x" must have the same type
because they are in the same scope. No constraints are necessary, since
the presence of the non-polymorphic constant "+" allows a ground type
for "x" to be computed.

This is not the case for

    \i j i j. i > j

in which the first "i" and "j" have no information on which to give them
a type. At this point hol88 says, "Well, let's at least give them
something", and hol90 says "uncle".

This difference does not manifest itself in any term in any proof ever
ported from hol88 to hol90.

The heuristic that *ought* to be used is that all free variables sharing
a name in a term must have the same type, and all free variables
occurring in the scope of a binding occurrence with the same name have
the same type as the binding occurrence. Or something like that.

Konrad.