search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.41k stars 642 forks source link

HAMT based datastructures support #2881

Open ryepesg opened 8 years ago

ryepesg commented 8 years ago

Languages like Scala and Clojure uses HAMT for implementing very fast arrays (the call it vector), hash-maps and hash-sets. Some people are using Idris in programming contest competitions, but for me it is very hard without those data structures, specially the array one.

jfdm commented 8 years ago

@ryepesg Thanks for the feature request. If you feel up to the task of providing such HAMTs then feel free to do so. If not and you have ideas of how it should be done, then adding a feature proposal to the wiki would also be grand.

ryepesg commented 8 years ago

Thanks @jfdm. I'm not capable enough to contribute, but the datastructues in Idris could be modeled after Haskell Vector.

Other datastructures are HashSet and HashMap.

clayrat commented 7 years ago

There's actually a newer alternative for HAMT called CHAMP, which is supposedly superior in terms of both speed and memory utilization. It's described in Steindorfer, Vinju, "Optimizing Hash-Array Mapped Tries for Fast and Lean Immutable JVM Collections" https://michael.steindorfer.name/publications/oopsla15.pdf and has Java implementations at

ahmadsalim commented 7 years ago

@clayrat Are you potentially interested in implementing CHAMP?

bamboo commented 7 years ago

FTR, the dotnet backend includes a HAMT implementation by relying on a backend specific native array API modelled after Haskell's Data.Vector.

So more importantly than HAMT or CHAMP, Idris needs to provide array primitives that all backends can implement, the rest can be built on top as libraries.

clayrat commented 7 years ago

@ahmadsalim I actually started drafting up an implementation, and came to the same conclusion as @bamboo - some sort of underlying (unsafe) array manipulation API is needed.

ahmadsalim commented 7 years ago

@bamboo @clayrat As far as I remember one only needed a fixed size array. This could be simulated by e.g.:

data Array32 : (a : Type) -> Type where
   MkArray32 : (c1 : a) -> ... -> (c32 : a) -> Array32 a
ahmadsalim commented 7 years ago

Of course a native array API would be great as well. I think one could use the FFI to design an API, but this might require a bit more work.

bamboo commented 7 years ago

@ahmadsalim in the case of HAMT, yes, the Array32 trick might be enough although not as convenient and performant (my guess) as a true native array. Nice trick anyway and I'll try it eventually on idris-hamt.