Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Fri, 5 Feb 1993 10:57:56 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15245;
          Fri, 5 Feb 93 02:45:14 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15240;
          Fri, 5 Feb 93 02:45:08 -0800
Received: from guillemot.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Fri, 5 Feb 1993 10:44:15 +0000
To: Victor "A." Carreno <vac@gov.nasa.larc.air16>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: sticky types
In-Reply-To: Your message of Tue, 02 Feb 93 10:38:47 -0500. <9302021538.AA23594@air52.larc.nasa.gov>
Date: Fri, 05 Feb 93 10:44:10 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.861:05.02.93.10.44.19"@cl.cam.ac.uk>


> I have never used sticky types. I thought it was not elegant. After writing
> types over and over again, I thought I'll give it a go. But it appears the
> sticky does not want to stick. 
> 
> Any hints on what I am doing wrong?

See page 204 of DESCRIPTION:

      The quotation type checker normally requires that there be
      enough information in a quotation to fully determine the
      types of all subterms of the term being type checked. This
      information comes from two sources:
      
        * the generic types of constants, and 
        * explicit type information given after a colon.
      
      If sticky types are activated (by setting the flag sticky to
      true) then the last type a variable had in a session is
      remembered, and this is used as a default type during type
      checking.  THE STICKY TYPE IS ONLY USED, HOWEVER, IF THE
      VARIABLE IN QUESTION IS COMPLETELY UNCONSTRAINED BY ITS
      CONTEXT IN THE QUOTATION.  If the context partially
      determines the type of a variable, then sticky types are not
      used.  For example, in the term "f 1" the variable f is
      constrained to have a function type, but the range type is
      not determined.  In the quotation "(f,1)" the variable f is
      completely unconstrained.  In the latter case an
      (appropriate) sticky type would resolve the typing, but in
      the former it would not.  Sticky types can never cause the
      type checking of a quotation to fail when it would succeed
      without them.

Tom