Accept a more generic Accumulate about idris HOT 4 CLOSED

We should use idris-testing or, better yet, Specdris (#43).

from idris.

Edit: I should've mentioned this right away. Thanks for starting this discussion!

That's not the real issue here though. Let me try to elaborate.

Altering the bespoke assertEq to be more specific is not the correct approach here.

assertEq : Eq a => String -> (given : a) -> (expected : a) -> IO ()

It specifies that assertEq means to compare two values of type a, under the constraint that a has an implementation of Eq. The implementation you linked does not satisfy that invariant, because the type checker cannot be sure that b has an implementation of Eq. The solution to your generic implementation then is to add the constraint:

accumulate : Eq b => (a -> b) -> List a -> List b

What all that said, the tests expect the solution to have the following signature, as per the stub.

accumulate : (Int -> Int) -> List Int -> List Int

Notably, the following test fails to type check when you alter the signature of accumulate, as in the linked solution.

testDecrementFunctionAddsOneToAllInput : IO ()
testDecrementFunctionAddsOneToAllInput = assertEq "decrement function subtracts 1 from input" (accumulate (\x => x - 1) [1,2,3]) [0,1,2]

When checking right hand side of testDecrementFunctionAddsOneToAllInput with expected type
        IO ()

When checking argument smaller to function Prelude.Nat.-:
        Can't find a value of type
                LTE 1 x

So if we want to support a more generic accumulate (I can see arguments both ways), the necessary changes are more broad in scope than just assertEq.

Hot take re: making accumulate generic

• Pros: more traditional FP, good learning exercise, intro to type constraints
• Cons: could be too much too soon (intro to type constraints), need to change most/all of test (not a big deal, obviously)

I've had a long day/week. Does this blathering make any sense?

from idris.

It does make sense.

I still believe generalising the signature should be accepted by tests, even if the stub stays the same.

The type errors you've cited stem from the compiler either not specialising b (the empty list case), or selecting a wrong type for numbers (the LTE 1 x case). Both cases could be solved by specifying the type of lists used in tests. That's what my proposition really does, by specialising the assertEq helper.

from idris.

Ok, I’d be happy to review/merge a PR.

from idris.