(untitled)

This technology needs a thread. It is pure magic. Liquid types seem to be the real deal for verifying the correctness of programs. Dependent types have gotten lots of hypes for ages, but this seems to be a much more practical way to get good safety guarantees without paying a huge price in verbosity.

uhhh any explanation of what a liquid type is?

>>5620 It's a subset of dependent types that doesn't break type inference. Basically, it lets you annotate regular types with conditions that must evaluate to true for any value of that type. Done correctly, this does not break type inference, so you can statically verify a program with very little effort since the compiler does all the mundane work for you. See: https://ucsd-progsys.github.io/liquidhaskell-blog/

>>5623 So basically the same thing as "Concepts" from C++?

>>5631 No, that's basically just typeclasses, which are orthogonal to this. This allows you to make refinement types, which basically specify a condition that will evaluate to true if you evaluate it on a value of that type. For example, you can make a type for integers in a given range. They will be subtypes of the base type, so that you can use this restricted integer type in any place that expects an integer, but not vice-versa. More importantly, the compiler can propagate these properties. For example, if x is known to be greater than 0, then the compiler will also know that x + 3 is greater than 3. The two liquid Haskell examples in the OP show how the compiler will give you a type error if you incorrectly implement a fibonacci function, or if you incorrectly implement insertion sort.

>>5616 So this is like a trait for haskell fiends?

>>5623 >Basically, it lets you annotate regular types with conditions that must evaluate to true for any value of that type. Sounds like Refinement Types in Typed Racket. Do they use the same concept?

>>5623 sounds exactly like the "types" from racket.

>>5645 Yes, liquid types are indeed (inferrable) refinement types. I don't know much about typed racket, but the nice thing in Liquid Haskell is that the type inference almost completely automates away most proofs of correctness. You can often prove an existing library correct (or incorrect) by just adding a few annotations to its functions, and it will either compile or find possible sources of bugs in the library source. Racket just got them a couple months ago right? Then they are probably the same. Liquid Haskell is probably the implementation with the most spread as it has been around for a couple years. As I understand it, In its early stages the idea has mostly been pushed by researchers at Microsoft research and at INRIA, and their research language F* has them as a core part of the language (it has full dependent types but empathizes the subset that doesn't break type inference, unlike Idris and Agda that require you to write out a function's type signature before implementing it).

If you like inferrable refinement types, then Microsoft research/INRIA's F* language is probably a really interesting language to look at: https://www.fstar-lang.org/ https://www.fstar-lang.org/tutorial/ It's a dependently typed language that heavily empathizes the subset of the language that doesn't break type inference. Afaik, it is the only dependently typed language with a self-hosting compiler. The compiler can prove itself to be correct!

Also, some cool statistics from Liquid Haskell projects: http://goto.ucsd.edu/~nvazou/real_world_liquid.pdf Apparently, averaged over 11 thousand LOC from various real-world libraries that were formally checked by liquid Haskell (with bugs fixed when needed), formally verifying all of it took 2k LOC of specifications and annotations. That compares VERY favorably with unit tests, which often require a 50-50 ratio to give good coverage, and 90% unit tests for applications that absolutely have to be safe no matter what. Formal checking when applicable gives an even stronger guarentee than the latter with less effort than the former. Refinement types essentially make unit tests obsolete in a large number of situations, especially if you are aiming for full coverage. It takes a number of safety-related software patterns (such as the gatekeeper pattern) and makes them "just code" with the safety enforced directly by the compiler instead of by the programmer.

I think that these are popping up everywhere nowadays mainly because the Z3 SMT solver is now free and available under an MIT licence. All the new implementations of refinement types seem to use it as the backend during the type inference/type checking step.

Could Rust get these?

>>5733 Probably. Even C# had an experimental extension called spec# which allowed formal checking. I remember writing a formally checked binary sort in it, and it wasn't verbose at all. I'd love to see Rust get than kind of safety features. Right now it has memory safety, and some inherent safety by encouraging immutability and single ownership, but formal checking of unsafe (and safe) code would be really nice to have.

>>5736 Found the spec# online demo: This binary search compiles if you flip the two inequalities: https://rise4fun.com/SpecSharp/BinarySearch

I read the papers and it makes sense but I can't even begin to imagine what the code actually looks like. How do people actually implement this stuff? What's the actual algorithm that the compilers use?

Why does haskell get all the good stuff, as ocaml zealot i'm envious. Anyway after going through Chlipala's book, i'm a bit more proficient at coq and this doesn't really seem that good in comparison.

>>5741 I guess it has something to do with Abstract Interpretation : https://en.wikipedia.org/wiki/Abstract_interpretation

>>5782 Ocaml has the F* language which can compile to OCaml and is mostly compatible with it.

>>5782 >Anyway after going through Chlipala's book, i'm a bit more proficient at coq If you have the book as a PDF, could you share it here? I can't wrap my head around coq, I'm terrible at it even though I've been following a course about it.

Coq fills a different niche to liquid types though. Proving something in Coq takes MUCH more effort than using refinement types when the latter are an option. But it can capture some things that the latter can't do.

>>5820 Not him and not that book, but these seem pretty cool https://softwarefoundations.cis.upenn.edu/

>>5616 >>5623 That looks pretty cool, but there must be a reason why "basic/official" Haskell doesn't include this, isn't it ? Seems a little bit too obvious. If that isn't the case, well, it definitely deserve inclusion in the language.

>>5915 Refinement types are much younger than Haskell, and efficient implementations were expensive proprietary solutions until just a couple years ago. Now that Microsoft's Z3 SMT solver is open source (happened in 2015), you're starting to see a bunch of good implementations in different languages that use it as a backend. As for GHC Haskell, it's currently undergoing another really major change in its type system, as DependentHaskell is reaching the point where it is being implemented and will be released in the next two years. Some form of refinement types might make it in.