Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 28 Sep 1995 17:13:00 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA259402914; Thu, 28 Sep 1995 09:41:54 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from crl.dec.com by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA259372911; Thu, 28 Sep 1995 09:41:51 -0600 Received: by crl.dec.com; id AA02531; Thu, 28 Sep 95 11:30:37 -0400 Received: by easynet.crl.dec.com; id AA21535; Thu, 28 Sep 95 11:29:59 -0400 Message-Id: <9509281529.AA21535@easynet.crl.dec.com> Received: from ricks.enet; by crl.enet; Thu, 28 Sep 95 11:30:29 EDT Date: Thu, 28 Sep 95 11:30:29 EDT From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" To: info-hol@leopard.cs.byu.edu Cc: leonard@ricks.enet.dec.com Apparently-To: info-hol@leopard.cs.byu.edu Subject: Synonymous types Has it ever occurred to you to try to merge two implementations of the same type, by proving that they're equivalent? I was thinking the other day about how unfortunate it is that one must choose between alternative implementations of things like integers, when each implementation's supporting library has advantages, and the two types are actually describing the same objects. I wondered if it would be possible to prove that the two types were the same, and thereafter be able to treat them as synonyms. I couldn't see how to make that work, but the next best thing, automated conversion between the two, seems workable and potentially useful. Given two types defined by specification, and proofs that the two specs are equivalent, it seems to me it should be possible to automatically derive mapping theorems for rewriting theorems about objects of one type into theorems about objects of the other, and it should be easy to wrap shells around derived rules (and theorem-tactics, etc.) from one theory to create equivalent rules for the other theory. (All this is assuming the two theories avoid name conflicts, which I recognize is a bad assumption, but that seems an uninteresting issue.) Since I didn't know that anyone else has already thought about it, I thought I'd bring it up. Do you see a way of making two existing types synonyms? If not, do you think mechanisms for converting between equivalent types would be useful?