Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Mon, 26 Oct 1992 14:47:40 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28544; Mon, 26 Oct 92 06:29:33 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28539; Mon, 26 Oct 92 06:29:10 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Mon, 26 Oct 92 14:17:49 GMT From: David Shepherd Message-Id: <11551.9210261417@frogland.inmos.co.uk> Subject: Re: Type checking loophole? To: gavan@za.ac.uct.mth.elc (Gavan Tredoux) Date: Mon, 26 Oct 1992 14:17:22 +0000 (GMT) Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: <9210252155.AA06936@elc.mth.uct.ac.za> from "Gavan Tredoux" at Oct 25, 92 11:55:28 pm X-Mailer: ELM [version 2.4 PL3] Content-Type: text Content-Length: 1501 Gavan Tredoux has said: > I've defined a new type ":lnum" and a constant "holds" but some typos > revealed the following phenomenon. Transcript follows from hol2.0 > > -------------------------------------------------------------- > > type_of "WHOLE";; > ":num -> lnum" : type > > type_of "holds";; > ":exseq -> (lnum -> (wff -> bool))" : type > > "!e i fmla. holds e(WHOLE i)((ALL fmla) imp fmla)";; > > "!e i fmla. holds e(WHOLE i)((ALL fmla) imp fmla)" : term > > "!e i fmla. holds e (i) ((ALL fmla) imp fmla)";; > > "!e i fmla. holds e i((ALL fmla) imp fmla)" : term > > -------------------------------------------------------------- > > This shouldn't be allowed, the second term with "holds" > having an ":int" rather than an ":lnum" for the second argument. > Yet the parser okays both. Hmm. there's no problem there .. in the second example you've just got a univerally quantified variable "i" of type ":lnum" instead of type ":num" as in the first example. in both cases the type checker is able to infer the type of "i" from context. what would have been erroneous would be "! e (i:lnum) fmla. holds e (i) ((ALL fmla) imp fmla)";; and the type checker would have complained -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq 1992: celebrate the quincentenary of columbus getting lost