So your solution is to rewrite the haskell standard library yourself?
With CPP or cabal tricks
I don't know what cabal tricks is supposed to mean here.
> I don't know what cabal tricks is supposed to mean here.
It means conditional compilation, i.e. what the C preprocessor also gives you (but somewhat more principled).
> 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.
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.
For pointer checks.
And with this rebuttal, the issue is now double settled.
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.
In Haskell you can provide your own prelude, which uses unsafe functions without bounds checks by default.
> 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:
* pointer checks, see [1] or https://news.ycombinator.com/item?id=37376946.
* valid expression checks [2], see https://news.ycombinator.com/item?id=37440896.
[1]: https://arxiv.org/abs/2207.04034 "Flux: Liquid Types for Rust"
[2]: https://www.tweag.io/blog/2022-01-19-why-liquid-haskell/ "Why Liquid Haskell matters"
"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.
This is my last comment on this issue.