[wyager]

The liquid Haskell constraint approach is very interesting. I have not tried it yet, but it looks like it might be quite usable.

Of course, the other popular approach is to use dependent types. I've recently run up against the limits of Haskell's type system in a number of projects, so I've been playing around with Idris. It's very cool to be able to promote arbitrary functions to the type level (and higher). The potential applications for static analysis are awesome.

I recommend everyone play around with cutting-edge type systems. Doing so has really influenced the way I program and do math. Haskell is pretty far up there, especially with standard GHC extensions (DataKinds etc.). Liquid Haskell, idris, agda, etc. are even more powerful. If you're coming from a C/Python/Java/etc. background like I did, you'll be totally blown away.

[jonsterling]

There's a perspective that unifies both the Liquid Haskell-style approach and dependent types, which is "behavioral type theory". Nuprl (the longest-lived implementation of dependent type theory, starting in the early 80s and still going strong today) is an example of a behavioral type theory, for instance; it's a trivial example, though, since the behavioral types refine a unityped structural framework, but you can generalize it to get something along the lines of Liquid Haskell, but without being tied to a solver. This is what we are currently working on with the JonPRL project; we have so far implemented a Nuprl-style type theory, and the next version of JonPRL will have a structural type theory underneath it.

[kmicklas]

This is something I've been wanting for a long time. Liquid Haskell and these solver-based systems should just be a special tactic library with some syntactic sugar on top of a standard dependently typed language.

[jonsterling]

One option is to treat the solver as a trusted "black box" rule if the user wants to—so theoretically, you could get all the benefits of something like Liquid Haskell simultaneously with the unbounded expressivity of full Nuprl.

[repetae]

NuPRL hasn't been actively developed in 30 years and was only ever of interest to small group of people working on proof assistants and pure type theory, not industrial users. LiquidHaskell is actively developed and can be used in production today for real life industrial use cases.

[jonsterling]

Nuprl is absolutely still actively developed, in fact; I am constantly in touch with the PRL group. But the code-base is very crufty. In the past two years, though, numerous features have been added (including nominal abstraction, exceptions, bar induction, and a number of other interesting things), which you'd be aware of if you spent more time paying attention and less time snarking.

I am not at all telling people, "Switch from Liquid Haskell to Nuprl!". I'm providing perspective on the design space.

[Kutta]

Is there any reason to single out Nuprl for this though? We could slap SMT onto a wide range of elaborators (as it has been a stated goal for the Lean prover, and there has been attempts in Isabelle, Coq and Agda too if I recall correctly). Practical elaboration already involves a large amount of machinery that isn't reflected in kernel type theory, so I don't see why Nuprl would be better in this regard.

[jonsterling]

It's a matter of behavioral type theory vs structural type theory; each can benefit from "slapping a solver on", but behavioral type theory allows you to reason directly about the code from a partial and effectful language, whereas structural type theory does not (in a direct way, at least).

Lean, Coq and Agda all implement structural type theory.