[notfashion]

> This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it.

It's more accurate to say that Idris can guess an implementation of the function, but it's not the only possible implementation with that type. There's nothing in the type to stop the function from reversing one or both of the lists before the zipping stage, for example. More generally, it could randomize the order of elements in one or both of the supplied lists.

[chongli]

That's true, though it has no reason to do those other things. In general it tries to do the least amount of work possible to accomplish the goal.

It's interactive, though, and it's extremely fun to use. It gives you the feeling that you're solving a puzzle, and like a good puzzle game, it can do the obvious bits for you.

[notfashion]

Yes, but the "least amount of work", as far as Idris is concerned, has no necessary relationship to what the programmer intended when they defined the type. It guesses the simplest thing that fits, but that's far from a guarantee of correctness.

It is a serious shortcoming that even when you pay the complexity cost of dependent types, you still can't specify the intent in this case. I mean, the semantics of "zip" can't be specified with a type. You can define a "sorted list" or "ordered list" type, but you cannot enforce maintainance of the natural, arbitrary order of list elements. In this sense dependent types are both too complex to reason about and simultaneously not powerful enough to fully specify the function.

[mrgriffin]

One solution to ensuring that the order is preserved (that I've actually used in production Haskell code where this was a real risk) is to use a heterogeneous list instead of a Vec.

  rzipWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as

With this type I don't think you'd be able to rearrange the elements, but you do have to pay the cost of using Const everywhere, as in you can specialize approximately my function as follows (handwavy, won't compile):

  zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
  zipWith f as bs = recToVec (rzipWith f' as' bs') where
    as' = vecToRec (fmap Const as)
    bs' = vecToRec (fmap Const bs)
    f' (Const a) (Const b) = Const (f a b)

  vecToRec :: Vec n (f a) -> Rec f (Replicate n a)
  recToVec :: Rec (Const a) as -> Vec (Length as) a

Rec is defined in Vinyl: https://hackage.haskell.org/package/vinyl-0.11.0/docs/Data-V...

[dllthomas]

> has no necessary relationship to what the programmer intended when they defined the type

Right, for instance I wouldn't be surprised if "the least amount of work" here amounted to reversing both lists as you zip.