bodil / purescript-sized-vectors

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

Apply instance is wrong? #14

Closed chrismshelton closed 4 years ago

chrismshelton commented 5 years ago

I think the Apply instance for Vec is wrong...

> import Data.Vec
> fns = cons (_ * 2) (cons (_ * 3) empty)
> nums = cons 2 (cons 3 empty)
> :t fns 
Vec D2 (Int -> Int)

> :t nums
Vec D2 Int

> :t (apply fns nums)
Vec D2 Int

> (apply fns nums)
[4,6,6,9]

Going by the type, apply fns nums should produce a Vec D2 but the array it produces actually has 4 elements in it

paluh commented 5 years ago

@chrismshelton I think that the instance provided by this library is consistent with default instance of an Array and allows us to provide Applicative instance for the Vector too. Here is a quick demo of Array apply in action:

> [(*) 2, (*) 3, (*) 4] <*> [1,2]
> [2,4,3,6,4,8]

Your apply proposition is also potentialy laws preserving implementation for that method in the spirit of the ZipList. Such an implementation requires from a given data type to be lazy in order to provide Applicative instance. That is because pure should return infinite... array in our case.

artemisSystem commented 4 years ago

It would not require a lazy list, because it will not have to be infinite. The amount of elements to be included when using pure is available in the type, and each length of array has its own instance. The Applicative instance even already works this way, making the instance unlawful for every vector with size not equal to one. (Breaks at least the identity law, the composition law, and the homomorphism law. Not sure about interchange because i just looked at them quickly but it's not very important, as it already breaks the three other laws) Here's repilcate: https://github.com/bodil/purescript-sized-vectors/blob/b31f49310931886706bb366cfc6c945ee9fcf7d7/src/Data/Vec.purs#L106-L111 ...Which is used in the definition of pure: https://github.com/bodil/purescript-sized-vectors/blob/b31f49310931886706bb366cfc6c945ee9fcf7d7/src/Data/Vec.purs#L269-L270 I can throw together a pull request fixing this right now

paluh commented 4 years ago

@3ddyy You are absolutely right! Sorry for my previous mindless and mechanical comment - I had completely missed the point. Thanks for explanation - this is really cool instance.