Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Wed, 13 Jan 1993 10:47:22 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25651; Wed, 13 Jan 93 02:34:03 -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 AA25596; Wed, 13 Jan 93 02:33:53 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Wed, 13 Jan 1993 10:33:09 +0000 To: KIKUCHI Yutaka Cc: info-hol@edu.uidaho.cs.ted Subject: Re: APPLY function on HOL In-Reply-To: Your message of Wed, 13 Jan 93 04:17:00 +0200. <9301121917.AA05632@jevex.cs.titech.ac.jp> Date: Wed, 13 Jan 93 10:33:05 +0000 From: John Harrison Message-Id: <"swan.cl.ca.680:13.01.93.10.33.12"@cl.cam.ac.uk> Yu writes: . Dr. John Harrison said: . > The type system of HOL won't let you define such functions with quite . > the abandon of LISP. . . I was so disappointed to hear that. . Our aim is to make a function that can apply [1;2;3] to + . and also can apply [2;3;4] to `\x y z.x+y*z'. . You mean that we cannot write such `apply' function, don't you? Indeed, I don't think HOL polymorphism stretches that far. It may be possible to produce some hack which would be sufficient for your purposes (I'm not clear what use you anticipate for this function), but there is no provision for what amounts to functions with variable numbers of arguments. Sorry, John.