Earlier quoted context omitted.
> Well, you can choose any two of: 1. Fast (less run-time), 2. Safe (cannot crash), 3. Simple types (None of the advanced type hackery). Many choose 1+3 or 2+3, but advanced types let you choose 1+2 which in many cases is remarkable and somewhat surprising that it is even possible. I don't think it's really that surprising that it's possible. Most programs don't rely on any deep mathematical properties for their corr…
> Haskell is not actually a completely 'safe' language; it still has exceptions that can cause a program to "go wrong" and terminate unexpectedly. You can write 'fast' code with it, but it isn't as fast as what I could write in a lower-level language. I never meant to imply Haskell was a "completely safe" language. That is an impossibility, even totality does not imply complete safety. My zip example is actually a po…
What Every C Programmer Should Know About Undefined Behavior #2/3
41–45 of 45 posts
Re: What Every C Programmer Should Know About Undefined Behavior #2/3
#42Kind of off topic, but I am curious: is this one of the advantages of functional programming - the notion that you can prove or disprove certain things about the code and therefore optimize the compiler, based on such proofs, to your heart's content?
The more advanced of a type system you have, the more you can optimize indeed. A nice example of this is the zip function. In Haskell: zip :: [a] -> [b] -> [(a, b)] zip [] _ = [] zip _ [] = [] zip (x:xs) (y:ys) = (x,y) : zip xs ys Note how each iteration needs to check both lists for emptiness. In a more advanced type system (or using more advanced type hackery in Haskell) you can have length-indexed lists. That is:…
Re: What Every C Programmer Should Know About Undefined Behavior #2/3
#43Earlier quoted context omitted.
The more advanced of a type system you have, the more you can optimize indeed. A nice example of this is the zip function. In Haskell: zip :: [a] -> [b] -> [(a, b)] zip [] _ = [] zip _ [] = [] zip (x:xs) (y:ys) = (x,y) : zip xs ys Note how each iteration needs to check both lists for emptiness. In a more advanced type system (or using more advanced type hackery in Haskell) you can have length-indexed lists. That is:…
This is interesting, but the two versions of zip you present are not equivalent. The standard version can handle lists of different lengths; it effectively truncates the longer list to the shorter one's length. Can you get this behavior in the second version and still have just one emptiness check?
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.Re: What Every C Programmer Should Know About Undefined Behavior #2/3
#44Earlier quoted context omitted.
This is interesting, but the two versions of zip you present are not equivalent. The standard version can handle lists of different lengths; it effectively truncates the longer list to the shorter one's length. Can you get this behavior in the second version and still have just one emptiness check?
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…
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.Re: What Every C Programmer Should Know About Undefined Behavior #2/3
#45Earlier quoted context omitted.
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…
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 c…
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.