> 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 th

> 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.