bodil / purescript-sized-vectors

Idris style sized vectors in PureScript
18 stars 12 forks source link

Reconsider `range` and `range'` #22

Closed m-bock closed 4 years ago

m-bock commented 4 years ago

Vec.range vs Unfoldable.range

It's obvious that we cannot have an Unfoldable instance. However, I found it confusing once that Vec.range and Vec.range' behave differently from Unfoldable.range and e.g. Array.range.

Couldn't we express the existing range just with fill (as its implementation) and thus maybe drop it?

A different range

and here's a suggestion of how a range could be closer to the 'real' one:

rangeNew ::
  forall n1 n2 n3 max min diff.
  Nat n1 =>
  Nat n2 =>
  Max n1 n2 max =>
  Min n1 n2 min =>
  Sub max min diff =>
  Pos diff =>
  Succ diff n3 =>
  n1 -> n2 -> Vec n3 Int
rangeNew _ _ = Vec $ Array.range (toInt (undefined :: n1)) (toInt (undefined :: n2))

This follows the same laws as the known range, it only adds a typelevel restriction: No negative endpoints, and they cannot be equal.

rangeNew d2 d2 -- compile error
rangeNew d4 d2 -- 4 +> 3 +> 2 +> empty
rangeNew d2 d4 -- 2 +> 3 +> 4 +> empty
artemisSystem commented 4 years ago

Good idea. The range function confused me as well when i first saw it

artemisSystem commented 4 years ago

Why should rangeNew d2 d2 error? Why not just remove the Pos diff constraint and allow it to create empty vecs?

Also, i believe it's more common to format type signatures with operators first on the line, like this:

rangeNew
  :: forall n1 n2 n3 max min diff
   . Nat n1
  => Nat n2
  => Max n1 n2 max
  => Min n1 n2 min
  => Sub max min diff
  => Succ diff n3
  => n1 -> n2 -> Vec n3 Int
m-bock commented 4 years ago

Yes true, we can omit the Pos. That's better. It will not create empty vecs, but singleton ones. rangeNew d2 d2 -- 2 +> empty

Regarding the formatting. I use purty. It's not perfect but pretty good. https://github.com/bodil/purescript-sized-vectors/issues/25

artemisSystem commented 4 years ago

right, i misthought

athanclark commented 4 years ago

Wow this is a really good idea, good work!