I would guess that the truncation of the ordinary zip is not because it is useful in that context, but because it makes the zip function total.

If you wanted truncation and had no type-level knowledge about a relationship between the list lengths, you would explicitly compose list truncation of the longer list with the zipping.

But if you have some sort of known relationship between the lengths of the lists, not just equality of the lengths (as specified above), you can avoid the check.

For example:

  zipTruncate :: List (1+ N) a -> List N b -> List N (a, b)
  zipTruncate _ [] = []
  zipTruncate (x:xs) (y:ys) = (x, y) : zipTruncate xs ys

This also has just one check, and is verified safe by the compiler, and truncates the single extra element from the first given list.

With dependent types, you can even say something like:

  zipTruncate :: List (someFunc N) a -> List N -> List N (a, b)

But I am no expert on dependent types, and do not know what can/cannot be done with application of functions at the type-level.

I would guess that the truncation of the ordinary zip is not because it is useful in that context, but because it makes the zip function total.

I used to think the same way, but then I ran into a couple of cases where it was actually useful (it was in Python, where zip has the same behavior).

If you wanted truncation and had no type-level knowledge about a relationship between the list lengths, you would explicitly compose list truncation of the longer list with the zipping.

Yes, but I guess that would be less efficient than the standard version of zip. You would at least have to check which list is longer, no?

But if you have some sort of known relationship between the lengths of the lists...

Special cases often enable better optimizations, but I'm asking about the general case.

So I guess the answer is that one can't use these types to implement the standard zip. On the other hand, if you assume the lists are of equal lengths then you can avoid the extra check in standard Haskell:

    zip' :: [a] -> [b] ->[(a,b)]
    zip' [] [] = [] 
    zip' (x:xs) (y:ys) = (x,y) : zip' xs ys

If the lengths are different this will give an error, although it's a runtime error so it's not as good as your version.

> I used to think the same way, but then I ran into a couple of cases where it was actually useful (it was in Python, where zip has the same behavior).

Then there's little reason not to explicitly truncate...

> Yes, but I guess that would be less efficient than the standard version of zip. You would at least have to check which list is longer, no?

A simple function like:

  truncate :: List N a -> List M a -> (List (min N M) a,
                                       List (min N M) a)

composed with zip, can be fused into the same original function as truncating zip -- there is no reason for it to be more expensive.

> Special cases often enable better optimizations, but I'm asking about the general case.

Note these same special cases will not yield any optimizations if you cannot encode that special case into the type.

> If the lengths are different this will give an error, although it's a runtime error so it's not as good as your version.

Actually, not having the pattern match for the empty/non-empty and non-empty/empty cases does not mean there is no runtime check.

You pay both with partiality (some inputs will fail at runtime) and speed (failed pattern matches still get checked at runtime). Dependant-typed zip gives you both of these back.