On 17/05/2011, at 12:08 AM, Chris Double wrote:
> On Tue, May 17, 2011 at 1:35 AM, john skaller
> <[email protected]> wrote:
>>
>> Felix provides arrays which include the length in the type and actually
>> allows *some* algorithms to be written with these but other, clearly
>> sensible, useful, and correct algorithms, cannot be written.
>> For example in Felix you can't concatenate two arrays because the lengths
>> can't be added by the type system.
>
> Have you considered adding some form of dependent types to Felix to
> allow expressing this sort of thing?
Sure, but I don't know how :) I would need a type theorist or three on the team
to help design this properly. As it is Felix is pretty much dead because of
lack of developers and users (which is why I'm here at the moment evaluating
Rust).
This is a bit off topic but: in Felix, an array has the type
T ^ N
where ^ is an exponential and N is a unit sum:
3 = 1 + 1 + 1
for example. In particular this kind of array is "free" in the sense that
it is precisely a tuple:
int ^ 3 = int * int * int
var x = 1,2,3;
is a tuple of three ints and also an array of 3 ints .. there's no difference,
they're not just isomorphic they're *equal*.
The problem is that
3 + 2 != 5
because, expanded:
(1+1+1) + (1 + 1) != 1 + 1 + 1 + 1 + 1
because summation is not associative.
In fact, the typing here has no need of dependent (run time) types.
Its entirely static. Its just that I do not see a general isomorphism
to do the calculation.
One should note from this scheme that array indicies SHOULD be sum types
and NOT integers, and such values cannot possibly be "out of bounds".
>
> Can you give an example of how making functions take tuples improves
> certain types of code or makes things possible that weren't before?
Sure just look at "binder1" and "binder2" in the C++ standard library and
wonder where "binder3" and "binder4" have gone. They haven't gone,
they're not defined. You need an infinite number of them. If you have only
one argument functions .. you only need one of them for completeness.
--
john skaller
[email protected]
_______________________________________________
Rust-dev mailing list
[email protected]
https://mail.mozilla.org/listinfo/rust-dev
