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
(1, (2, 3)) is NOT ((1,2),3) is NOT (1,2,3)
even though they're isomorphic.
OK, so in the representation of arrays, there is no way to "add" two units sums
1 (+) 2 = 3
but we need to do this. Certainly we can add the integers:
BTYP_array (T, BTYP_unitsum 43) ((++)) BTYP_array (T, BTYP_unitsum 57)
=>
BTYP_array (T, BTYP_unitsum 100)
where ((++)) is joining two arrays, but this is only possible because 43 and 57
and
fixed bounds. We cannot say
BTYP_array (T, BTYP_unitsum N) ((++)) BTYP_array (T,BTYP_unitsum M) =>
BTYP_array (T, BTYP_unitsum (N + M))
because the argument of BTYP_unitsum is an integer, it can't be a type variable
because the argument isn't a type. We can write this:
BTYP_array (T, BTYP_sum (BTYP_unitsum N, BTYP_unitsum M))
but this is NOT the same as
BTYP_array (T, BTYP_unitsum (N + M))
which is what we want. There is a __flatten operator in Felix, but it cannot be
reduced
until after the variables become constants, and consequently unification fails,
in
other words
_flatten(N + M)]
does not unify with
BTYP_unitsum _
In case you're confused ..
fun join[T, N, M] (x:array[T, N]) (y:array[T, M]):array[T, _flatten(N + M)] =
{
remember
BTYP_array (double, string)
unifies just fine with BTYP_array (T,N) by setting N->string. Which is just
T ^ string
which .. is the type of a strdict if we wanted! An array of T indexed by
strings is just as sane
as one indexed by integers.
The point is the notation first allows for any kind of index, and later barfs
when the index
isn't a unitsum ("Felix doesn't know how to implement this ytet").
There are any number of possible fixes.. not sure what to do though!
BTW: we could implement this easily:
BTYP_array (T, BTYP_type_tuple [BTYP_unitsum 3; BTYP_unisum 4])
what's that you say? It's just this:
Array [T, (3 , 4)]
Commonly known as a Matrix.
--
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
