Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 27 Jun 1995 14:34:35 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA133907801;
          Tue, 27 Jun 1995 06:56:41 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA133857749;
          Tue, 27 Jun 1995 06:55:49 -0600
Received: from ira.uka.de (actually i80s35) by irafs1 with SMTP (PP);
          Tue, 27 Jun 1995 14:55:19 +0200
To: info-hol@leopard.cs.byu.edu
Cc: slind@informatik.tu-muenchen.de
Subject: Semantics of HOL
Date: Tue, 27 Jun 1995 14:53:15 +0200
From: schneide <schneide@ira.uka.de>
Message-Id: <"irafs1.ira.164:27.06.95.12.55.22"@ira.uka.de>


Konrad answers:
|> Sure, but you will have to give up some kind of type 
|> inference, since that is undecidable in the "2nd order" 
|> lambda calculus.

Yes, that will be true if we would allow type abstractions
to appear everywhere. But if we restrict them only to 
appear at the top of the term (except for type applications)
then we obtain a predicative polymorphism which is 
in a sense weaker than 2nd order lambda calculus which
uses impredicative polymorphism. In particular, the type 
inference for predicative polymorphism is (however I am
not sure at the moment) decidable.


Klaus.