Context
A while ago, I implemented an immutable Array-based Zipper. I’m now adding instances for the Extend and Comonad type class instances. However, when I use quickcheck-laws to verify that these instances are correct, the Comonad check fails:
Checking 'Associativity' law for Extend
1000/1000 test(s) passed.
✓︎ Extend
Checking 'Left identity' law for Comonad
1000/1000 test(s) passed.
Checking 'Right identity' law for Comonad
491/1000 test(s) passed.
✗ Comonad:
Test 3 (seed 1808572881) failed:
Test returned false
Overview of Problem
Comonad’s extract is pretty easy to implement, and after further debugging I can prove that the issue is with my Extend implementation. The below implementation fails because I always set the focusIndex to 0 (so that a valid element is always focused regardless of which index I use). This implementation works fine when the first element is focused, but fails when any other element is focused.
So, if I have an array [0, 1, 2], and I focus the third element (i.e. 2), then this equation should be true:
extract (extend (fold $ map Additive) zipper) == (fold $ map Additive) zipper
It’s not because the first iteration of mapWithIndex below will “copy” the zipper into the first element slot in the array. In reality, it should be copied into the third element slot in the array.
While I could use a custom case to force that to occur, I’m guessing my understanding of what this instance should be doing is likely just incorrect in the first place.
Could someone clarify how the Extend instance should be implemented?
Current Implementation
I based my implementation on the Array instance. For a runnable example, I put a gist together via Try PureScript. You’ll need to open the console to see the result.
-- | An immutable Zipper for an Array.
-- | Modifications to the focused element are `O(n)` due to creating
-- | a new array rather than mutating the underlying array.
-- | Navigating to a new focus element is `O(1)` regardless of how far
-- | away from the current focus that element is. This
-- | is in contrast to a `List`-based zipper where modifications
-- | are `O(1)` and navigation is `O(n)`.
-- |
-- | In other words, this zipper works well in read-heavy code
-- | but might not work well in write-heavy code
-- |
-- | [0, 1, 2, 3, 4, 5]
-- | ^ ^
-- | | -- maxIndex
-- | -- focusIndex
newtype ArrayZipper a =
ArrayZipper { array :: Array a, focusIndex :: Int, maxIndex :: Int }
derive instance eqArrayZipper :: Eq a => Eq (ArrayZipper a)
derive instance functorArrayZipper :: Functor ArrayZipper
instance extendArrayZipper :: Extend ArrayZipper where
extend
:: forall b a
. (ArrayZipper a -> b)
-> ArrayZipper a
-> ArrayZipper b
extend f (ArrayZipper rec) =
let
sliceArray idx _ =
f (ArrayZipper
{ array: slice idx (rec.maxIndex + 1) rec.array
, focusIndex: 0
, maxIndex: rec.maxIndex - idx
})
in ArrayZipper (rec { array = mapWithIndex sliceArray rec.array})
instance comonadArrayZipper :: Comonad ArrayZipper where
extract :: forall a. ArrayZipper a -> a
extract (ArrayZipper r) = unsafePartial (unsafeIndex r.array r.focusIndex)
Other Extend implementations I’ve tried
This implementation fails to pass the same law above. It duplicates the zipper n times, so that each copy is focusing a different element within it:
instance extendArrayZipper :: Extend ArrayZipper where
extend
:: forall b a
. (ArrayZipper a -> b)
-> ArrayZipper a
-> ArrayZipper b
extend f (ArrayZipper rec) =
let
sliceZipper idx _ =
f (ArrayZipper rec { focusIndex = idx })
in ArrayZipper (rec { array = mapWithIndex sliceZipper rec.array})