archives

Unsoundness

Hi, I wonder if someone can help resolve the conflict described below.

My system is an Algol like language which supports both functional and procedural code.
Now, I hate the way C handles lvalues, it doesn't extend well, one has to make horrible rules
and list all possible l-contexts, and attempts to do this in C++ are an abysmal failure.
My solution is elegant! Consider a record:

(x=1,y=42.1)

which has type

(x:int, y:double)

then this is a first class value, and the field names are projections:

x (x=1,y=42.1)

Since I have overloading there's no conflict with the same field name in some other record,
the field name is just an overloaded function name.
To make it look nicer you can use reverse application:

(x=1,y=42.1) . x

Now, to get rid of lvalues we introduce pointer types and variables so that in

var xy = (x=1,y=42.1);
&xy <- (x=2,y=43.1);

This is really cool because & is not an operator,
just a way to write the value which is the address of a variable.
We use a procedure written as infix left arrow which takes a pointer to T
as the first argument and a T as the second, and stores the value at the specified address. So its all values.

To assign to a component, we introduce a second overload for each projection that takes a pointer argument and returns a pointer:

&xy . x <- 3;

This works for other products as well (tuples, arrays and structs).
So, we have a purely value based semantics and a sane type system.
In particular we have a very nice rule that relates values and objects.

So far so good, but now I have another feature called "compact linear types"
which are packed encodings of any type defined by the rule:
unit is compact linear, and sum, product, or exponential of a compact linear type is compact linear.
A small compact linear types is one that fits in a 64 bit machine word.
So for example the type 3 * 4 is a single 64 bit value which is a subrange of integer 0 thru 11.
Compact linear types with integer coercions used as array indices give polyadic arrays
(rank independent array programming).

The problem is .. compact linear type components are not addressable.
Projections functions work fine, but there are no overloads for pointer projections.

And so the conflict: polymorphic pointer projections are unsound:

proc f[T,U] (r: &(T,U)) (v:T)) { r.0 <-v; }

will not work if r is a pointer to a compact linear object. I can think of three solutions:

(1) invent a new pointer type (destroys uniform pointer representation property)
(2) have distinct product, sum, and exponential operators for compact linear types
(3) use the same operators but introduce pack and unpack operations