On 21/06/2012, at 1:25 AM, john skaller wrote:
> I'm in the throws of trying to get multi-dimensional arrays working.
>
The problem here is that array access is implement in the library
bi a C binding. The combinator "EXPR_get_n" is only generated by
pattern matching.
So now the theory says, given
T ^ N ^ M
we can use a new operator
index_to_product (T ^ N ^ M ) => T ^ (M * M)
on types. On values the same operator can be defined: it is a reinterpret
cast that just changes the type. The big thing is that an array type translates:
BTYP_index_to_product (
BTYP_array (
BTYP_array (T, BTYP_unitsum N),
BTYP_unitsum M
)
)
reduces to
BTYP_array (T,
BTYP_type_tuple (
BTYP_unitsum N,
BTYP_unitsum M
)
)
which is a linear array with a tuple index. Of course, this operation can be
encoded
in the library with a type function and typematch:
typedef fun index_to_product t = typematch t with
| ?T ^ ?N ^ ?M => T ^ (N * M)
endmatch
The problem is that the library can't generalise this. The general form "a la
FISh" is
array [n,m,r] [a,b] [c,d,e] ....
i.e. an arbitrary length list of arbitrary lists of dimensions .. in Felix
notation this is:
T ^ (n * m * r) ^ (a * b) ^ (c * d * e) ....
The reshaping isomorphism is easy to understand, you can move the ^ and *
operators around how you like as long as the "list" of integers doesn't change.
This has no impact on the layout of the array. It has no impact on where the
columns and rows are. The only impact is on how it is indexed, in other words,
where the actual data functors "array" lie. In turn this determines what higher
order functions like map and fold mean. The "reshaping" operator is used
to change "what is considered an element".
In category theory terms we're saying array is a data functor, but here's a new
data functior: array of array. Alternatively we can undo that and make an
array of array (aka matrix) into a an array (with data the happens to be
an array).
This matters because a functor is a structure preserving map. Thus means
that
given a function f: T -> U for the functor ARRAY we can define
f (ARRAY) by f (ARRAY T) -> ARRAY (f T)
in other words the function "f" and the functor ARRAY commute.
Of course the name of the operator above is "map". It's part of the
"structure preservation". Folds also, and other stuff.
Anyhow the problem is that the Felix type system has no way to define
the general form or reshaping above in the library. We can do a simple
binary case. We can do the several ternary cases, but after that it gets
nasty. Of course in Ocaml, in the compiler, it's trivial to check two lists
of lists of ints conform to the reshaping rule!
Interestingly there's no problem with ^, the problem is with *.
Felix can handle ^ because it's a left associative binary operator
so any number of these can be handled by recursion (Felix type
functions can be recursive). But operator * is not binary but
n-ary.
--
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
