Dependent-typed multidimentional arrays

[suhr]

Related (QUBE language):

• http://www.cs.ru.nl/dtp11/slides/trojahner.pdf
• http://www.students.informatik.uni-luebeck.de/zhb/ediss1099.pdf

[edwinb]

What's the issue here with Idris?

If this is something you'd like to see implemented, it might be better suggested on the mailing list.

[nicolabotta]

Related (QUBE language) to what ?

[suhr]

Related (QUBE language) to what ?

To the subject.

If this is something you'd like to see implemented, it might be better suggested on the mailing list.

Yes, I probably should suggest it there (just used to suggest features on Github).

What's the issue here with Idris?

Well, I can't find even one-dimension arrays. Also Matrix is represented now as Vect n (Vect m a) and I'm not sure about its performance.

[edwinb]

I'd suggest asking on the mailing list if anyone has done anything like this, or if anyone is interested in helping to make something like this, in that case.

There's lots of interesting things can be done in Idris, and we can't do all of them ourselves. If there are features or libraries which can reasonably considered core, that's a different matter, but I think requesting an entirely new library is out of the scope of what we're trying to track on the issue tracker here.

[nicolabotta]

Сухарик notifications@github.com wrote:

Related (QUBE language) to what ?

To the subject.

I see, thanks ! Multidimensional arrays are an interesting subject and
there have been a number of attempts at implementing efficient
operations on them. I remember

http://acts.nersc.gov/formertools/pooma/

from the time I was working on PDEs but there are certainly more recent
examples. I think it would be interesting to start by trying to
understand the difference between vectors as they are currently
implemented in Idris and "arrays" as they are meant in QUBE or other
languages or libraries.

Maybe finite functions (functions taking values in |Fin m|, |(Fin m, Fin
n)|, etc.) of numerical types could be a starting point to get to a
notion of array (maybe as computationally efficient representation of
finite functions ?).

Best,
Nicola

[suhr]

I'm actually more interested in declarative array programming. Such languages as APL or J provide expressive and generalized operations on arrays, so programs can be short, clear and without any [explicit] loops. QUBE seems to provide it with gen-with (array creation) and loop-with (folding) constructions and pattern matching on dependent types.

[saulshanabrook]

I am working on a similar solution for compiling array expressions efficiently using ideas from APL, but in Python. If anyone has any links to the Qube language implementation or Idris implementations of similar work, they would be much appreciated.