Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9212111502.AA08489@easynet.crl.dec.com>
Date: Fri, 11 Dec 92 10:25:13 EST
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" <leonard@com.dec.enet.ricks>
To: info-hol@edu.uidaho.cs.ted
Cc: leonard@com.dec.enet.ricks
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: Cartesian sums for alternative representations

I've been working on the formal spec of the Alpha AXP architecture.  Alpha is
a 64-bit architecture, and I've been unhappy with all the representations I've
considered for 64-bit words.  No matter what I pick --- 64-element lists, or
64-tuples, or num, or whatever --- some operations are a real pain, and require
converting to and from a more tractable representation.  To do a floating-point
operation, for example, I have to convert each word into a real, perform the
operation, and convert back. 

Yesterday it occurred to me that I could use a Cartesian sum:
  (bool list) + (num) + (int) + (real) + ...

I'll have to write functions to convert from any of the choices into any of the
others (and had better prove that the conversions don't change the meaning),
but I probably won't actually convert very often at all.  Almost always, if
a value is operated on as one data type, the next operation will consider it
the same data type.  If all my operations first convert their operands to the
most convenient representation, and return their results in that same
representation, all operations can be defined in terms of their own most
convenient representations, and yet conversions will still be rare.

Have you seen this done before in other contexts?  Are there difficulties with
it that I've overlooked?

Tim