The UCSD programming systems group writes about LiquidHaskell, refinement types and verifying Haskell programs.
HN commenters point to it as a good example of refinement types, with an interactive tutorial they find amazing for proving properties about code.
This is actually a very good comment. Haskell has had these features since early ~2000s and it was a major competitive advantage in the language space, but today I would argue that if you're using a modern language then they don't stand out as much. Nevertheless, not all popular languages provide all the above mentioned features and in case they implement them it's usually in a compromised fashion. For example, nullable types are still an open issue in Java, while C# and Typescript provide easy ways to circumvent them, a lot of times by accident (the main issue is that they're mostly annotations, not runtime checks).
On the other hand, you mention several features which Haskell provides, usually through libraries that can only be implemented due to the features provided by the base language:
- Refinement types [1] allow to add runtime invariants to existing types in an ergonomic fashion, or you can go even further and use something like LiquidHaskell[2] to enforce properties at compile time.
- For multithreaded programs, the existence of STM[3] allows to to write mutable variables which are safe to use across threads. Very few languages offer something like this.
- For structural dependencies, you can apply the techniques of "ghost of departed proofs"[4]. Personally I don't like to go that route since programming becomes an act of "proving" rather than "doing" but I appreciate the fact that you can encode it if you want/need to.
- Metaprogramming in Haskell is not as…
If you're talking about the restricted/smart constructor approach that I think is exemplified by this library, i.e. the approach that hides the construction of a type behind a mandatory verification function, it's a pattern that's been around for a long time. OOP constructors are perhaps the best known example, although they often through an exception on invalid input rather than represent this at the type level with an Option/Maybe type or Either type.
I personally think that this approach (with the type level tracking) is indeed woefully underused (and is an easy-to-understand-and-implement win in most codebases) and would usually chalk it up to lack of familiarity in the community.
That being said, there are definitely domains that can make this approach (without the help of general dependent types) cumbersome to the point that I would consider scrapping it. One example of this is doing statistics and collection types. Most statistical operations operate over a collection of values. This is easily supplied by a standard collection type such as List or Vector. A significant chunk require a non-empty collection of values (think aggregate statistics such as mean). A type such as NonEmptyList or NonEmptyVector comes in handy here along with the corresponding verification function. A smaller chunk require collections of at least two elements (e.g. a sample estimate of standard deviation). Now you need a separate AtLeast2ElemList with a separate verification function.…
This kind of type becomes really tedious to use unless there is some sort of viable "subtyping"—you certainly want to be able to use a non-zero number where any number works and, ideally, you want to be able to recover a non-zero number when you write a function that takes in a normal number and always returns a positive value. If you're forced to use a bunch of explicit conversion functions to achieve this you add a lot of noise to your code and, generally, the most common function is going to be along the lines of "I know this is positive, so throw an error if it's 0"—which is exactly what we get anyway.
Explicit might be better than implicit most of the times, but it is possible to be too explicit.
That said, we can achieve this, although it's probably a bit trickier than you'd think at first. The best option I know is called "refinement typing", which basically allows you to specify types as subsets (ie "the set of integers which are not 0") and automatically verifies whether your functions actually return a value in the subset.
Liquid Haskell[1] is an example of a system you can use today to play with the idea. It uses an automatic logic solver (Z3) under the hood to automatically prove that your refinements hold. (For example, I believe it should be able to automatically verify that the function f x = abs x + 1 will never be 0.)
[1]: https://ucsd-progsys.github.io/liquidhaskell-blog/
From what I gather, this happens at runtime, which makes me feel it's a bit unfortunate to call it dependent types, or at least my view of dependent types is of it being a compile-time guarantee.
Take for example Liquid Haskell[0] where you can, at compile time, make guarantees about your code. For example, here's a function that makes division safe, by never allowing the second value, y, to be 0,
{-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y
The second annotation is plain Haskell meaning it takes 2 `Int`s and returns an `Int`, with the third line being the function body. The first {-@ .. -} annotation is the one Liquid Haskell reads, stating it takes an `Int` as the first argument, another `Int`, which we now refer to as v, that is not 0, and finally returns an `Int`.
Another practical language with dependent types is Idris[1], which supports full dependent types with dependent pattern matching.
Finally, for the "why would I use this", I recommend checking out Gabriel Gonsalez's keynote, from Haskell eXchange 2017, "Scrap your Bounds Checks with Liquid Haskell"[2]
[0] https://ucsd-progsys.github.io/liquidhaskell-blog/
[1] https://www.idris-lang.org
[2] https://skillsmatter.com/skillscasts/10690-keynote-scrap-your-bounds-checks-with-liquid-haskell
Conflating types in binary operations hasn't been an issue for me since I started using TS in 2016. Even before that, it was just the result of domain modeling done badly, and I think software engineers got burned enough for using dynamic type systems at scale... but that's a discussion to be had 10 years ago. We all moved on from that, or at least I hope we did.
> Now we all should be looking towards fail-safe systems, formal verification and domain modeling.
We were looking forward to these things since the term distributed computing has been coined, haven't we? Building fail-safe systems has always been the goal since long-running processes were a thing.
Despite any "past riddles", the more expressive the type system the better the domain modeling experience, and I'd guess formal methods would benefit immensely from a good type system. Is there any formal language that is usable as general-purpose programming language I don't know of? I only ever see formal methods used for the verification of distributed algorithms or permission logic, on the theorem proving side of things, but I have yet to see a single application written only in something like Lean[0] or LiquidHaskell[1]...
[0]: https://lean-lang.org/
[1]: https://ucsd-progsys.github.io/liquidhaskell/
As was already mentioned in another reply, what you are describing are refinement types. A refinement type system actually exists for Haskell: it’s called LiquidHaskell,[1] and though I have not used it for anything serious, it seems to work well for certain kinds of problems.
The main challenge of refinement types is that arbitrary properties are very difficult to check in general. (If that weren’t the case, software verification would be easy!) I wrote about this at length in my previous blog post,[2] and Hillel Wayne wrote about it earlier this year from another perspective.[3]
[1]: https://ucsd-progsys.github.io/liquidhaskell-blog/
[2]: https://lexi-lambda.github.io/blog/2020/08/13/types-as-axioms-or-playing-god-with-static-types/
[3]: https://www.hillelwayne.com/post/constructive/