Differences between `shiftInAt0` and `shiftInAtN`

[kleinreact]

I noticed some unexpected differences between shiftInAt0 and shiftInAtN:

• I'd expect them to share an equivalent type signature, but
  • shiftInAt0 requires KnownNat n, while
  • shiftInAtN requires KnownNat m.
• Probably as a consequence of the above
  • shiftInAt0 is implicitly quantified via forall n a m, while
  • shiftInAtN is implicitly quantified via forall m n a.
• Finally, if we'd for example redefine rotateLeftS and rotateRightS via shiftInAt0 and shiftInAtN utilizing their duality (see some example code below), then
  • the resulting rotateLeftS' definition returns on some input in the REPL, while
  • rotateRightS' does not.

We either should give both operations some symmetric behavior or we should explain, why we like them to be different on purpose.

---

rotateLeftS' :: forall d n a. KnownNat n => Vec n a -> SNat d -> Vec n a
rotateLeftS' input SNat = output
 where
  (output, feedback) = shiftInAtN @d @n @_ input feedback

rotateRightS' :: forall d n a. KnownNat n => Vec n a -> SNat d -> Vec n a
rotateRightS' input SNat = output
 where
  (output, feedback) = shiftInAt0 @n @_ @d input feedback

someInput :: Vec 10 Bit
someInput = unpack 0b1110011000

returns :: Vec 10 Bit
returns = rotateLeftS' someInput d2

diverges :: Vec 10 Bit
diverges = rotateRightS' someInput d2

[christiaanb]

Right, currently,	Function	Argument 1	Argument 2
shiftInAt0	lazy	strict
shiftInAtN	strict	lazy

Which is why:

rotateRightS' :: forall d n a. KnownNat n => Vec n a -> SNat d -> Vec n a
rotateRightS' input SNat = output
 where
  (output, feedback) = shiftInAt0 @n @_ @d input feedback

diverges, as it uses its recursive result in the strict argument position. To make it not diverge you have to do:

rotateRightS' :: forall d n a. KnownNat n => Vec n a -> SNat d -> Vec n a
rotateRightS' input SNat = output
 where
  (output, feedback) = shiftInAt0 @n @_ @d input (lazyV feedback)

The reason for all of this is my/our desire to built functions within the Vector module out of existing functions in the Vector module; as opposed to adding a new recursive function. Though this is mostly coming from a position where:

1. In the past, we would have to add a new primitive for every recursive function (this is no longer the case).
2. In the present, in order to have fast compiles, it's better to have a primitive for a recursive function; but I want to avoid adding more primitives.

We can make the type arguments have the same order, so n m a. But otherwise I wouldn't want to make any changes in order to achieve symmetry. I would probably update the documentation to highlight the strictness of the arguments. I could be convinced otherwise though.

[kleinreact]

I'm fine with keeping the operations asymmetric with respect to their argument strictness, as long as this is clear to the user. It's just something that might be overseen easily otherwise.

We can make the type arguments have the same order, so n m a. But otherwise I wouldn't want to make any changes in order to achieve symmetry. I would probably update the documentation to highlight the strictness of the arguments.

:+1: