change internals

[artemisSystem]

I’m not entirely sure about this, but it might be possible to change the internals in a way that makes it possible to pattern match on Vecs (like this: a +> b +> c +> Empty). This would be very practical, and it would be possible to easily pattern match on each value without any unsafeCrashWith mess. This might be impossible without GADTs though? I’m not certain.

[artemisSystem]

I can try implementing this later today or tomorrow

[artemisSystem]

Something like this? Maybe? data Vec s a = forall s1. Succ s1 s => a +> Vec s1 a | Empty. This might work, but i'm not sure (might try it out later today). One thing is that there are constraints in the declaration (generally looked upon as a bad idea), which is to prevent you from constructing a Vec D2 a with three elements for example. Not super familiar with this though, and the final implementation might differ from this (or might not even be possible, we'll see). A great bonus (in my opinion) though, is that there will be no clash or confusion between Data.Vec.empty and Control.Plus.empty anymore (because the former won't exist, it will be Empty, which is a constructor for Vec).

[artemisSystem]

Silly me, this isn't haskell. It would have to be something like VecCons a (Vec s1 a) instead of a +> Vec s1 a, then with a infixr 6 VecCons as +> after. (Same fixity as Data.List.(:))

[artemisSystem]

As most things will have to be rewritten, i can try fixing #22 and #23 (#26) while i'm at it

[athanclark]

You might be able to get away with it in the type theoretic sense, because if I recall correctly, Exists is made with an existential type variable. However, I do not think you can add any constraints on that data constructor, like in Haskell's GADTs as you just mentioned. Ideally, it would look something like a heterogeneous list:

data Vec (size :: Nat) a where
  Nil :: Vec D0 a
  Cons :: forall child. Succ child size => Vec child a -> a -> Vec size a

But I don't think it's possible.

Furthermore, and I think this is a very important feature, is that Vec's are just newtypes over Arrays, meaning they (for the most part) have the same runtime complexity as them, and can be used in place if need be. I think that's a very necessary feature, especially in terms of purescript being a simple wrapper around javascript, which isn't stellar in terms of compilation enhancements or anything. From what I understand, javascript engines treat arrays a bit better than nested objects, which is what the data constructors would compile to.

[artemisSystem]

i think it really depends on a case to case basis what’s better between arrays and linked lists, i could be wrong though. and in most of the use cares i’ve seen or thought of, the differences between arrays and lists are negligible. i think you’d have to have a list of at least a thousand elements, and then you’d see the list come out on top actually, i think. might be that arrays are better before that, but as i said, it’s not by much and i don’t think it’s very important. I’m trying something with classes, not sure if it’s gonna work though, will update you tomorrow.

[athanclark]

Yeah I agree. I think it might belong in its own package then, because it would be less of a "random access" vector per se, and more of a linked list, as you mentioned.

[artemisSystem]

I don't really think it makes that much of a difference honestly, and if it's possible to implement, i think it should be here. But maybe we'll see if we get there

[artemisSystem]

This doesn't seem possible for now. An alternative is to use uncons to chip away at each element in a type-safe way.