5 ms·

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]

by Peaker 15y ago

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: lists that have 2 type parameters or "indexes" instead of 1. The 1 is usually the type of element inside the list, the extra 1 is a natural number indicating the length of the list. So the function zip becomes something like: zip :: List N a -> List N b -> List N (a, b) zip [] [] = [] zip (x:xs) (y:ys) = (x,y) : zip xs ys The compiler checks the code and verifies, at compile-time, that both the input lists and the resulting list are all of the same length. This also means that you only need one runtime emptiness check instead of 2. If the N is concretely known at compile-time, you may need 0 (though that case might be caught by inlining/loop unrolling optimizations anyway).

cwzwarich 15y ago
In an unsafe language like C or C++, you would just assert that the two containers are the same length and use parallel iterators. The type system here lets you optimize away some of the overhead of using a safe language, but it doesn't let you write code that is more optimized than the obvious unsafe code, at least in this example. Also, in this example you're using a singly linked list, which is usually a performance loss compared to a more appropriate data structure. CPUs are designed to favor contiguous arrays.
- Peaker 15y ago
  > In an unsafe language like C or C++, you would just assert that the two containers are the same length and use parallel iterators. The type system here lets you optimize away some of the overhead of using a safe language, but it doesn't let you write code that is more optimized than the obvious unsafe code, at least in this example. 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. Also note that runtime checks, in many cases, do not give you safety. For example, normally, you have an array indexing operation like: readArray :: Array a -> Int -> IO a Ignore the "IO" if you are unfamiliar with Haskell's IO type. This is unsafe whether or not you have index bounds checking. A runtime check will only convert one kind of error (corruption/segfault) to another (runtime exception). In these (common cases), your only option of getting safety is advanced type hackery. Something like: index :: (size:N) -> Array size a -> Fin size -> a where Fin N is the type of integer ranged between 0 and (N-1). > Also, in this example you're using a singly linked list, which is usually a performance loss compared to a more appropriate data structure. CPUs are designed to favor contiguous arrays Nothing about this type hackery is specific to singly linked lists, and advanced type hackary is applicable for pretty much any data structure. Also note that the singly linked lists used in zip may not actually be represented by pointer-chasing singly-linked lists. They may be "fused" together into efficient loops that process the input directly.
  - cwzwarich 15y ago
    > 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 correctness, so the ability to formalize a proof that they are correct and encoding it into a type system doesn't surprise me at all. If it is possible to do it on a large program without maintenance or scalability problems, then I will be more impressed. You also present a false trichotomy. 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. > Nothing about this type hackery is specific to singly linked lists, and advanced type hackary is applicable for pretty much any data structure. Also note that the singly linked lists used in zip may not actually be represented by pointer-chasing singly-linked lists. They may be "fused" together into efficient loops that process the input directly. As the data structures get further away from algebraic data types, the type hackery gets more and more involved. If you start working with arbitrary mutable data structures that arise in practice, the type hackery becomes a topic for a PhD thesis rather than something usable in practical programming today. I don't know of any compiler that actually does a reasonable job converting uses of data structures like lists and association lists into arrays and hash tables in general. There are compilers (like GHC) that handle special cases but fall over beyond that. I think this falls into the territory of the "sufficiently smart compiler" fallacy. Also, making data contiguous is just the simplest of a common set of data representation optimizations. Does any compiler automatically convert a list into an intrusive doubly linked list or eliminate the use of a visited stack for DFS by stealing a bit from vertices or reversing pointers?
    - deleted 15y ago
      [deleted]
    - Peaker 15y ago
      > 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 point against Haskell (as length-indexed lists are not yet actually in use in the Haskell eco-system). Haskell can encode low-level programs that are almost C-level, and in that (ugly) style can probably reach the performance you can with lower-level languages (excluding hand-optimized assembly, perhaps). > As the data structures get further away from algebraic data types, the type hackery gets more and more involved. If you start working with arbitrary mutable data structures that arise in practice, the type hackery becomes a topic for a PhD thesis rather than something usable in practical programming today. Mutable data structures do not have to "arise in practice". You can have pure semantics with mutable performance (e.g: Clean's uniqueness types, or Haskell's ST). Lots of people's PhD thesis are in actual use in practical programming today. A PhD thesis often discovers a technique and makes it accessible for real world programs today. > I don't know of any compiler that actually does a reasonable job converting uses of data structures like lists and association lists into arrays and hash tables in general. I think this falls into the territory of the "sufficiently smart compiler" fallacy. Converting these is not a good idea because you would change the complexities of the code (which is, IMO, the heart of the fallacy). A prepend of an a-list or a list is O(1), but to a list or hash table, it is (in the worst-case) worse. But what Haskell's primary compiler, GHC, does do, is fuse together list processing such that lists can disappear altogether into efficient loops. As for arrays and hash tables, these are not amenable to efficient "pure" modification (unless you use uniqueness types as in Clean), but they have reasonable alternatives that are pure and persistent: Sequence allows O(logN) indexing, O(1) amortized (O(logN) worst-case) prepend/append. Tries and search trees allow for quick lookups and quick pure modification. These are easy to reason about. > Also, making data contiguous is just the simplest of a common set of data representation optimizations. This conflicts with O(1) prepend. If you want contiguous allocation, you can use different data structures. > Does any compiler automatically convert a list into an intrusive doubly linked list or eliminate the use of a visited stack for DFS by stealing a bit from vertices or reversing pointers? If you need to remove/insert items in the middle of a list, you would probably not use a linked list. So a doubly linked is not a good optimization to apply automatically. If your point is that code with simpler mathematical semantics that is easy to reason about might cause a constant hit on performance in some cases -- then I agree. You cannot always have simplicity, verifiability, and speed. But often you can. Also note that purity affords many optimizations that are unavailable in non-pure languages (e.g: rewrite rules like: map f . map g --> map (f . g)).
guygurari 15y ago
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?
- Peaker 15y ago
  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.
  - guygurari 15y ago
    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.

by Peaker 15y ago

cwzwarich 15y ago

In an unsafe language like C or C++, you would just assert that the two containers are the same length and use parallel iterators. The type system here lets you optimize away some of the overhead of using a safe language, but it doesn't let you write code that is more optimized than the obvious unsafe code, at least in this example. Also, in this example you're using a singly linked list, which is usually a performance loss compared to a more appropriate data structure. CPUs are designed to favor contiguous arrays.

Peaker 15y ago
> In an unsafe language like C or C++, you would just assert that the two containers are the same length and use parallel iterators. The type system here lets you optimize away some of the overhead of using a safe language, but it doesn't let you write code that is more optimized than the obvious unsafe code, at least in this example. 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. Also note that runtime checks, in many cases, do not give you safety. For example, normally, you have an array indexing operation like: readArray :: Array a -> Int -> IO a Ignore the "IO" if you are unfamiliar with Haskell's IO type. This is unsafe whether or not you have index bounds checking. A runtime check will only convert one kind of error (corruption/segfault) to another (runtime exception). In these (common cases), your only option of getting safety is advanced type hackery. Something like: index :: (size:N) -> Array size a -> Fin size -> a where Fin N is the type of integer ranged between 0 and (N-1). > Also, in this example you're using a singly linked list, which is usually a performance loss compared to a more appropriate data structure. CPUs are designed to favor contiguous arrays Nothing about this type hackery is specific to singly linked lists, and advanced type hackary is applicable for pretty much any data structure. Also note that the singly linked lists used in zip may not actually be represented by pointer-chasing singly-linked lists. They may be "fused" together into efficient loops that process the input directly.
- cwzwarich 15y ago
  > 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 correctness, so the ability to formalize a proof that they are correct and encoding it into a type system doesn't surprise me at all. If it is possible to do it on a large program without maintenance or scalability problems, then I will be more impressed. You also present a false trichotomy. 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. > Nothing about this type hackery is specific to singly linked lists, and advanced type hackary is applicable for pretty much any data structure. Also note that the singly linked lists used in zip may not actually be represented by pointer-chasing singly-linked lists. They may be "fused" together into efficient loops that process the input directly. As the data structures get further away from algebraic data types, the type hackery gets more and more involved. If you start working with arbitrary mutable data structures that arise in practice, the type hackery becomes a topic for a PhD thesis rather than something usable in practical programming today. I don't know of any compiler that actually does a reasonable job converting uses of data structures like lists and association lists into arrays and hash tables in general. There are compilers (like GHC) that handle special cases but fall over beyond that. I think this falls into the territory of the "sufficiently smart compiler" fallacy. Also, making data contiguous is just the simplest of a common set of data representation optimizations. Does any compiler automatically convert a list into an intrusive doubly linked list or eliminate the use of a visited stack for DFS by stealing a bit from vertices or reversing pointers?
  - deleted 15y ago
    [deleted]
  - Peaker 15y ago
    > 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 point against Haskell (as length-indexed lists are not yet actually in use in the Haskell eco-system). Haskell can encode low-level programs that are almost C-level, and in that (ugly) style can probably reach the performance you can with lower-level languages (excluding hand-optimized assembly, perhaps). > As the data structures get further away from algebraic data types, the type hackery gets more and more involved. If you start working with arbitrary mutable data structures that arise in practice, the type hackery becomes a topic for a PhD thesis rather than something usable in practical programming today. Mutable data structures do not have to "arise in practice". You can have pure semantics with mutable performance (e.g: Clean's uniqueness types, or Haskell's ST). Lots of people's PhD thesis are in actual use in practical programming today. A PhD thesis often discovers a technique and makes it accessible for real world programs today. > I don't know of any compiler that actually does a reasonable job converting uses of data structures like lists and association lists into arrays and hash tables in general. I think this falls into the territory of the "sufficiently smart compiler" fallacy. Converting these is not a good idea because you would change the complexities of the code (which is, IMO, the heart of the fallacy). A prepend of an a-list or a list is O(1), but to a list or hash table, it is (in the worst-case) worse. But what Haskell's primary compiler, GHC, does do, is fuse together list processing such that lists can disappear altogether into efficient loops. As for arrays and hash tables, these are not amenable to efficient "pure" modification (unless you use uniqueness types as in Clean), but they have reasonable alternatives that are pure and persistent: Sequence allows O(logN) indexing, O(1) amortized (O(logN) worst-case) prepend/append. Tries and search trees allow for quick lookups and quick pure modification. These are easy to reason about. > Also, making data contiguous is just the simplest of a common set of data representation optimizations. This conflicts with O(1) prepend. If you want contiguous allocation, you can use different data structures. > Does any compiler automatically convert a list into an intrusive doubly linked list or eliminate the use of a visited stack for DFS by stealing a bit from vertices or reversing pointers? If you need to remove/insert items in the middle of a list, you would probably not use a linked list. So a doubly linked is not a good optimization to apply automatically. If your point is that code with simpler mathematical semantics that is easy to reason about might cause a constant hit on performance in some cases -- then I agree. You cannot always have simplicity, verifiability, and speed. But often you can. Also note that purity affords many optimizations that are unavailable in non-pure languages (e.g: rewrite rules like: map f . map g --> map (f . g)).

guygurari 15y ago

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?

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