Arrays in Idris

[bro...@dnanexus.com]

This has been asked before I think, but what's the status of random access in O(1) time type arrays in Idris?

I've looked at the libraries and the examples in the Manning book's MEAP, but from what I can see Vect is a linked list
and Matrix is built on top of it. If that's true, and if the compiler doesn't compile this down to 'C like' arrays, it would make
Idris unsuitable for certain applications.

[David Raymond Christiansen]

Hello,

> This has been asked before I think, but what's the status of random
> access in O(1) time type arrays in Idris?

We don't have it as a built-in primitive. Depending on exactly what you
want, it's not stupendously difficult to implement in a backend-specific
manner using the FFI, especially if the arrays you need only contain
primitive types like Int, Bits8, or Double.

> I've looked at the libraries and the examples in the Manning book's
> MEAP, but from what I can see Vect is a linked list
> and Matrix is built on top of it. If that's true, and if the compiler
> doesn't compile this down to 'C like' arrays, it would make
> Idris unsuitable for certain applications.

Right. Those aren't the right tools for every job, and O(1)-readable
arrays are useful. It would be nice to have better support for them.

/David

[bro...@dnanexus.com]

On Wednesday, February 24, 2016 at 10:31:58 AM UTC-8, David Christiansen wrote:

Hello,

> This has been asked before I think, but what's the status of random
> access in O(1) time type arrays in Idris?

We don't have it as a built-in primitive. Depending on exactly what you
want, it's not stupendously difficult to implement in a backend-specific
manner using the FFI, especially if the arrays you need only contain
primitive types like Int, Bits8, or Double.

Hi David,

    Thanks, that's what I was thinking of doing, using the SQLite binding as a model.

> I've looked at the libraries and the examples in the Manning book's
> MEAP, but from what I can see Vect is a linked list
> and Matrix is built on top of it. If that's true, and if the compiler
> doesn't compile this down to 'C like' arrays, it would make
> Idris unsuitable for certain applications.

Right. Those aren't the right tools for every job, and O(1)-readable
arrays are useful. It would be nice to have better support for them.

I guess I'm now pestering you (and Edwin) about a timeline for a better solution ;-).

I thought that with uniqueness types, that better solution would be forthcoming. The now

moribund Clean language used to have decent arrays IIRC, and they also had array backed

strings, unlike Haskell. Please steal ideas from Clean.

-- Brian

[David Raymond Christiansen]

Hi Brian

> I guess I'm now pestering you (and Edwin) about a timeline for a better
> solution ;-).
> I thought that with uniqueness types, that better solution would be
> forthcoming. The now
> moribund Clean language used to have decent arrays IIRC, and they also
> had array backed
> strings, unlike Haskell. Please steal ideas from Clean.

It would be nice to get this, but it's not on my todo list right now.

/David

[Niklas Larsson]

I have been playing around with arrays of primitive types as in here https://github.com/idris-lang/Idris-dev/pull/2972.

Arrays of Idris would need a different mechanism. I've looked at it a bit, but not done anything. The primitives would be simple enough, making a fancy dependently typed array class looks like real work :-)

Niklas

---

Från: bro...@dnanexus.com
Skickat: ‎2016-‎02-‎25 01:20
Till: Idris Programming Language
Ämne: Re: [Idris] Arrays in Idris

---

The contents of this e-mail and any attachments are confidential and only for use by the intended recipient. Any unauthorized use, distribution or copying of this message is strictly prohibited. If you are not the intended recipient please inform the sender immediately by reply e-mail and delete this message from your system. Thank you for your co-operation.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[bro...@dnanexus.com]

Great, that looks like a good first start. I like that you added the missing types for systems programming. Hopefully this or something like it will get merged soon, at least as a stopgap until said fancy dependently typed array appears. Thanks!

-- Brian

[Ahmad Salim Al-Sibahi]

It would be nice if we could get something like bitmapped vector-tries (http://hypirion.com/musings/understanding-persistent-vector-pt-1) for efficient pure arrays :).

Unfortunately, they would take some time to develop on top what there is now, and it requires a native implementation of immutable arrays in each backend if it has to be portable (and not require excessive IO).

-- AS

[Apostolis Xekoukoulotakis]

Any algebraic data type that has only one self recursion should be transformed into an array. Let me explain why.

First of all, each such type would consume the same amount of memory, that is the union of its the memory of each constructor except its self-recursion.

An array of n elements means that we have a self-recursion for n-1 elements and not for the last one.

The fact that we have only one self-recursion allows us to have only one path that would generate an n-array, thus the variable n determines 1-1 the path that was taken, helping in performing pattern matching.

[William ML Leslie]

On 29 February 2016 at 20:24, Apostolis Xekoukoulotakis

<apostolis.xe...@gmail.com> wrote:
> Any algebraic data type that has only one self recursion should be
> transformed into an array. Let me explain why.
> First of all, each such type would consume the same amount of memory, that
> is the union of its the memory of each constructor except its
> self-recursion.
> An array of n elements means that we have a self-recursion for n-1 elements
> and not for the last one.
>
> The fact that we have only one self-recursion allows us to have only one
> path that would generate an n-array, thus the variable n determines 1-1 the
> path that was taken, helping in performing pattern matching.

While this might make sense for unique lists, it's not an optimisation
in general, because it makes it harder for lists to share tails.

--
William Leslie

Notice:
Likely much of this email is, by the nature of copyright, covered
under copyright law. You absolutely MAY reproduce any part of it in
accordance with the copyright law of the nation you are reading this
in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without
prior contractual agreement.

[Markus Pfeiffer]

Hi Apostolis,

On Mon, Feb 29, 2016 at 11:24:11AM +0200, Apostolis Xekoukoulotakis wrote:
> Any algebraic data type that has only one self recursion should be transformed
> into an array. Let me explain why.
> First of all, each such type would consume the same amount of memory, that is
> the union of its the memory of each constructor except its self-recursion.
> An array of n elements means that we have a self-recursion for n-1 elements and
> not for the last one.
>
> The fact that we have only one self-recursion allows us to have only one path
> that would generate an n-array, thus the variable n determines 1-1 the path
> that was taken, helping in performing pattern matching.

Have you tried implementing this? Have you benchmarked it?

Cheers,
Markus

[Apostolis Xekoukoulotakis]

No I haven't implemented it. The previous email are mostly my thoughts on how it should be done.

William makes a good point which I cannot answer in a definite manner. So here are some more thoughts.

If an algebraic data type implements an interface with the function 

at: a -> Int -> Maybe a  ,and that function is a simple recursion to the type a k times, 

then the compiler will treat that algebraic data type as an Array assuming all the conditions are met.

Changing the size of the array wil most probably require to copy all the data to the same position or to another one.

This proposal allows the programmer to make a conscious decision about how he wants his data type to behave based on his needs without at the same time polluting the idris language that much.

[Ahmad Salim Al-Sibahi]

Actually, optimization wise the best thing is to have a hybrid between a list and an array, https://en.wikipedia.org/wiki/Unrolled_linked_list (I got this from people who had done heavy benchmarking). 

In any case, my idea of having a bitmapped vector trie was to allow for an unbounded datastructure with good performance for random access, updates and appending for users, and not as an internal optimization.

Regards,AS