headers
john skaller | 7 Jun 2012 14:44
Picon

adding array bounds

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
(Continue reading)

Permalink | Reply |
headers
john skaller | 8 Jun 2012 14:14
Picon

Re: adding array bounds

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:
(Continue reading)

Permalink | Reply |

Gmane