So I'm struggling with some stuff now. Consider
T^N * T^M === T^ (N+M)
This is an isomorphism, but is it an equality? What does it mean?
Basically the first expression is the type of this example with N=2, M=3:
val x = ( (1,2,3), (4,5) )
In other words it's a pair of arrays. To index this you'd do
x.0.0, x.0.1, x.1.0, x.1.1. x.1.2
to get 1, 2, 3, 4, 5 in turn. However, the top level thing is NOT an array!
It's a tuple, because the two components have different types.
Now, Felix current "kludges" the type of an array index. The correct type
of an array
int ^ 3
is 3, not int. Just to make it plainer, the correct type of
int ^ 2
is 2, not int. The type 2 is just the type used to express two alternatives
and it has a "common name" you all know "bool". Look in the Felix library
and you will see:
typedef bool = 2;
2 is syntactic sugar for
1 + 1
where 1 is syntactic sugar for the type of (), the empty tuple,
which is also called "unit",
The values of two are
case 0 of 2
case 1 of 2
Yes, that works. Ugly zero origin notation, blame C.
These also have a "common name":
false
true
[These names are also in the library, they're macros for the canonical
names]
I need you to see that for an array of length two the CORRECT index
type is bool not int. Because bool is just 2. So the correct index values
are false and true.
When you access an array with an int there's an "implicit conversion"
from int to the correct index type. This conversion isn't transparent:
the conversion generates code, namely an array bounds check.
The representation of "case N of M" where N is an integer literal
and M is a unit sum type is just int. So the same data representation
is used.
The point no is: the correct index for the array
T^N * T^M === T^ (N+M)
is 2 to select which tuple component, then either N or M
depending on which is selected. The general form is
roughly:
case 0 of (N+M) (case k of N)
case 1 of (N+M) (case k of M)
Or something. My brain is bent! But these are just nested cases.
It's easier to consider an encoding:
if index in 0 to 1 then firstarray . index
else secondarray. (index -2)
But we can CHEAT as follows. We know a tuple stores elements in order
as does an array so the representation in C++ of these two arrays is layout
compatible with an array of 5 elements. So the encoding of the index 0 .. 4
can be used directly provided we cast the tuple of the two arrays to a
tuple of a single array length 5.
Now the point here seems to be that the isomorphism is indeed an equality
in Felix. That is, the type of the array index is really
N + M
where N, N are unitsums. Although
2 + 3 is NOT equal to 5
our chosen encoding of unitsums as ints, and tuples and arrays as successive
fields of a structure, naturally allow the isomorphism to be implicit. In other
words
the *integers" 0 thru 4 are a perfectly good encodings of 2 + 3.
BTW: why am i going on with all this?? Because of this:
/*
fun join[T, N, M] (x:array[T, N]) (y:array[T, M]):array[T, _flatten(N + M)] =
{
....
*/
It's commented out. It doesn't work. Because we can't flatten type variables.
So I'm just going to make arrays with index type
* sum of ints, or
* sum of any valid array index type
valid index types. The implementation is of course .. just to add up
the all the unitsum counters.
--
john skaller
skal...@users.sourceforge.net
http://felix-lang.org
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
