7 Jun 2012 14:44

```I'm trying to figure out how to deal with this:

fun join[T, N, M] (x:array[T, N]) (y:array[T, M]):array[T, _flatten(N + M)] = {

This doesn't work at the moment. Here's the model:

Flx_btype.t =
...
| BTYP_sum of t list
| BTYP_unitsum of int
| BTYP_array of t * t
| BTYP_type_var of bid_t * t

noting:

BTYP_tuple [] is the type unit of value ().

BTYP_unitsum n is () + () + () + () ... n times, the BTYP_sum of n units.

BTYP_array (T,N) is an array, but Felix only allows N to be a BTYP_unitsum.

The type 2 is an example of a unit sum, this one is named "bool", it just
means "2 cases".

Finally we must not that type summation is NOT associative.

1 + 2 is NOT 3

although they're isomorphic. This is just the dual of the more familiar fact that

```

8 Jun 2012 14:14

```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:

```