4 ms·

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

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.

Peaker 15y ago
> 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.

Peaker 15y ago

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