drop and negative indexes

[RyanGlScott]

In Haskell, calling drop n xs with a negative integer n is equivalent to calling drop 0 xs, i.e., returning the original list xs unchanged:

λ> drop (-1) [1, 2, 3]
[1,2,3]
λ> drop 0 [1, 2, 3]
[1,2,3]

In Copilot, however, the drop function over streams is a bit more inconsistent. There are times where calling drop with a negative index works, e.g.,

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop (-1) true
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

$ runghc Main.hs
example:
(true)
(true)
(true)
(true)
(true)

On the other hand, there are other streams for which calling drop (-1) will cause Copilot to crash:

{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

spec :: Spec
spec = do
  let s :: Stream Bool
      s = drop (-1) ([False] ++ true)
  trigger "example" s [arg s]

main :: IO ()
main = interpret 5 spec

$ runghc Main.hs
Main.hs: Prelude.!!: index too large
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/List.hs:1368:14 in base:GHC.List
  tooLarge, called at libraries/base/GHC/List.hs:1378:50 in base:GHC.List
  !!, called at src/Copilot/Interpret/Eval.hs:147:18 in copilot-interpreter-4.6.1-inplace:Copilot.Interpret.Eval

Moreover, if you try to compile this specification to C99 or Bluespec, then -1 will underflow and result in generated code that looks like this:

static bool example_0_guard(void) {
  return (s0_get)((4294967295));
}

We should figure out a coherent story for what Copilot's drop function should do with negative indexes. Personally, I would propose making drop (-1) equal to drop 0, just like it is in Haskell, as this seems like the least surprising choice. Implementation-wise, this would only require a very small change to drop's implementation to achieve.

[ivanperez-keera]

I like this.

Also relevant: #601

[ivanperez-keera]

Also annoying is that drop doesn't cross function application boundaries.

For example, in principle, it should be that:

drop n (f + g) = drop n f + drop n g

However, that's not the case in Copilot.

Drops don't cross OP<n> boundaries.

I wonder whether this is just a different problem, or whether there's a more elegant variant of drop we could potentially come up with.

[RyanGlScott]

I don't think it's the exact same problem, but it's conceptually similar: drop n (f + g) not being equal to drop n f + drop n g is another instance of drop not having enough special cases. In this example, drop isn't doing enough to enforce the Drop invariant, i.e., that Drop should always be applied directly to an Append. We could rectify this by adding the following special cases to drop's definition:

diff --git a/copilot-language/src/Copilot/Language/Operators/Temporal.hs b/copilot-language/src/Copilot/Language/Operators/Temporal.hs
index 37b0d9a2..79b72aa8 100644
--- a/copilot-language/src/Copilot/Language/Operators/Temporal.hs
+++ b/copilot-language/src/Copilot/Language/Operators/Temporal.hs
@@ -36,4 +36,10 @@ drop :: Typed a => Int -> Stream a -> Stream a
 drop 0 s             = s
 drop _ ( Const j )   = Const j
 drop i ( Drop  j s ) = Drop (fromIntegral i + j) s
+drop i ( Op1 op s ) =
+  Op1 op (drop i s)
+drop i ( Op2 op s1 s2 ) =
+  Op2 op (drop i s1) (drop i s2)
+drop i ( Op3 op s1 s2 s3 ) =
+  Op3 op (drop i s1) (drop i s2) (drop i s3)
 drop i s             = Drop (fromIntegral i)     s

This would be a pretty nice improvement, and with no downsides that I can think of.

[ivanperez-keera]

Should we also add a case for Append along the following lines?

drop i (Append y Nothing s) | if length y >= i = Append (drop i y) Nothing s else ???

[RyanGlScott]

I'm not sure if we'd want the condition to be length y >= i, because if length y == i, then we'd end up with a situation where we Append an empty list to a stream, and I think that copilot-language's internals currently expect this list to be non-empty. For length y > i, however, then I think that optimization would be plausible.

Actually, if we maintain the Drop invariant (i.e., that Drop always appears applied directly to an Append), then it seems like we could almost always optimize away uses of Drop before they get to copilot-language's analysis step. That's an interesting thought... I'm not sure what ramifications that would have on the overall design. Perhaps Drop could be eliminated in favor of putting all of the logic inside of the drop function? (I might be overlooking something that makes this impossible.)

[ivanperez-keera]

because if length y == i, then we'd end up with a situation where we Append an empty list to a stream

You're right. We'd have something like:

drop i (Append y Nothing s) | length y > i  = Append (drop i y) Nothing s
                            | length y == i = s
                            | otherwise     = ???

[ivanperez-keera]

Going back to what drop (-1) s would do, the other sensible alternative would be to give our an error message.

Putting the fact that Copilot is an EDSL in Haskell, is there a reason why silent behavior might be better than a static error?

To put it another way: are there scenarios where drop (-1) s is not indicative of a conceptual error?

[RyanGlScott]

In Haskell at least, the reason for making drop well-defined (even for negative values) is to make the property take n xs ++ drop n xs == xs hold for all n. Copilot doesn't have a take function for streams, however, so this argument is less convincing. I suppose making drop n emit a proper error message for negative n would also be reasonable—I don't have that strong of an opinion one way or the other.

[ivanperez-keera]

Tagging @fdedden .

I wonder if there's a good mathematical justification for what Ryan is saying that would suggest that a drop that doesn't error is somehow better based on the work we did in https://dl.acm.org/doi/10.1145/3609026.3609727, even if we don't have an actual take function in Copilot.