Seems like back peddling. If part of the input data you have is there to reference input data in an array in C++ you would check the input data ahead of time so that you don't have to check the range in the middle of a loop.
Then you can have performance that is compared to everything else instead of just other programs written in the same language.
I think the main confusion is that, "Scrap your Bounds Checks with Liquid Haskell" presented a toy example/implementation which scales to real implementations, for the task of high-performance parsing of UDP packets (used by Awake Security, I guess).
The toy example/implementation is chosen to teach Liquid Types/Haskell, and therefore, covers the simple case of parsing UDP headers, which is a simple bounds check of "indexing an array of length 8". In this case, there is no need to use Liquid Types in any language.
But in the real use case (not shown in the talk), when you want to dig deeper into the content of UDP packets and such, you will need more than "check the input data (length) ahead of time so that you don't have to check the range in the middle of a loop". This is the case where Liquid Types help, tremendously. But such complicated cases, where Liquid Types shines, may not fit into a talk.
Again, it is not fair to think this is a complication specific to Haskell.
Again, it is not fair to think this is a complication specific to Haskell.
It is fair, because other languages have a single keyword or setting instead of a whole 'type system' with fancy labels that introduces lots of complexity for something simple.
It is not fair to think this is a complication specific to Haskell, because you can opt-out of runtime bounds checks as easily as C++, Rust, and Julia, with functions such as unsafeTake and unsafeDrop.
It is unfair to not respond to these points, while calling "this is a complication specific to Haskell." Because Haskell can do what others can do, but more.
> lots of complexity for something simple.
"indexing an array of length 8" for parsing UDP headers is simple, agreed. And Haskell can handle that simply with unsafe functions.
Keeping track of properties with complicated dependencies to parse arbitrary content (perhaps application-logic-aware contents, not "just checking for array length before indexing in a loop") is simple, strong disagree. See the section "Beyond Bounds Checking" of "Why Liquid Haskell matters" for example [1]. This might be used to implement the kinds of static analysis needed for Mojo or Swift, for instance [2].
And this cannot be solved in the languages you mentioned, either. Unless you are claiming that all parsing checks are "just checking for array length before indexing in a loop".
We are still working on completely different scales.
The talk is using a toy example to show what is possible, and you are using that example too literally, without realizing that the example scales to handle much more complex problems that people need to deal with in the real world.
It is unfair to lump together different scales and call them the same thing.
Your reaction is like criticizing a talk which shows sorting 5 numbers with programs, with "it is simple to sort 5 numbers by hand, why bother learning how to program with all those complexity for something this simple?". And then calling this fair, without realizing that in the real world, sometimes people need to sort way more than 5 numbers.
C++ doesn't have bounds checks in the std library in release builds by default, so you can't get better than that.
Your reaction is like criticizing a talk which shows sorting 5 numbers with programs,
It is not, because this idea that loops and bounds checks are complex in the first place isn't true. No other language invests so much complexity in a simple problem that is barely an issue in modern languages in the first place.
> C++ doesn't have bounds checks in the std library in release builds by default, so you can't get better than that.
In Haskell you can provide your own prelude, which uses unsafe functions without bounds checks by default. With CPP or cabal tricks, you can easily have bounds checks only for debug builds, but no bounds checks for release builds. No Liquid Types needed either, though this is only testing in development but not compile time verification. Less safe, but same effort and result as in C++.
> loops and bounds checks are complex in the first place isn't true.
Liquid Types people are not thinking about only loops and bounds checks. They think about any properties, for example:
Sorting 5 numbers is complex in the first place isn't true. No other technology invests so much complexity as programming and this is barely an issue in modern problem solving in the first place.
My previous comments already said loops and bounds checks are not complex in the first place, and they are only used as a demo in a talk, as Liquid Types scale to handle any properties.
I am pretty certain that a reasonable reader can judge the merits of our arguments and make up their mind. Thanks for raising a possible misconception about Haskell and Liquid Types, and this forced me to strengthen the arguments to clear the misconception for other reasonable readers. This is my last comment on this issue.
> So your solution is to rewrite the haskell standard library yourself?
No need--the simplest solution is to pass flags correctly to the dependent library (set all flags BoundsChecks, UnsafeChecks, and InternalChecks to false for the vector package) for release builds.
Explanation after the one-line rebuttal:
This exactly matches the C++ behavior: no bound checks for release builds, but with bounds checks for debug builds. This shows that Haskell can do what C++ can do, very easily, just by passing compiler/cabal/stack flags correctly.
With this rebuttal, I think the issue is completely settled, at least for reasonable readers.
No need--the simplest solution is to pass flags correctly to the dependent library (set all flags BoundsChecks, UnsafeChecks, and InternalChecks to false for the vector package) for release builds.
If performance is an issue, why not just do this instead of dealing with "Liquid Types".
And with this rebuttal, the issue is now settled for all readers and even those differently abled that are using voice readers.
But why have a separate type system instead of just building it into the language. C++ could build in pointer checks and it would be in the same type system.
And with this rebuttal, the issue is now double settled.
> But why have a separate type system instead of just building it into the language.
Excellent question. The existing "mainstream" languages (C++, Rust, Julia, or even Haskell) are not designed to support such applications as bound checks or pointer checks in their type systems, where certain runtime values/checks can affect/refine the types (as in dependent types, or refinement types which Liquid Types are based on).
It could be done (in some newer languages: Idris, Agda, Lean), but people have not figured out an ergonomic way to do so in more "mainstream" languages (e.g., not hurting type inference, light and maintainable proof burdens). Liquid Haskell is an attempt to bring refinement type to Haskell, as an extrinsic type system.
> C++ could build in pointer checks and it would be in the same type system.
People have not figured out how to do so (and I doubt if it is possible at all). Suffice to say:
* Rust is an attempt to build in lifetime-and-ownership-checks into the type system of C++, and Rust is a new language,
* Liquid Rust is an attempt to add pointer checks (refinement types) to Rust, and even then it is not built into Rust.
> And with _this_ rebuttal, the issue is now double settled.
People are still researching solutions (see Rust and Liquid Rust over C++) to this problem (building in pointer checks in the type system of C++), and they would love it if you can settle their problems.
Seems like back peddling. If part of the input data you have is there to reference input data in an array in C++ you would check the input data ahead of time so that you don't have to check the range in the middle of a loop.
Then you can have performance that is compared to everything else instead of just other programs written in the same language.