I would like to discuss how Dependent Haskell could compare to Idris2.
Haskell is a language with a few features that could make dependent types difficult, such as pervasive type inference. GHC, the only serious compiler, was initially not suited for dependent types — System F, the heart of the compiler, wasn’t. But it has long since diverged in practice. GHC is no longer based around System F; the Core is significantly different now. Whether it is as good as the Idris2 core, I don’t know.
On the other hand, Idris2 has a self-hosting compiler, with lessons learned from Idris1, and pervasive totality checking — which I don’t know whether Dependent Haskell will attempt.
But the type system is not sound. There are a few small errors here and there, and the Type : Type issue hasn’t been dealt with. Idris2 is fully victim to the type-in-type problem; it implements no kind of universe levels. This leads to Girard’s paradox, where Type : Type introduces inconsistency
That said, I gather this problem could be solved. It just takes enough manpower that Idris2 compiler devs don’t want to divert, because for practical problems, Girard’s paradox basically never comes up.
I would like to know if Dependent Haskell could implement a fully sound type system. And whether it could implement totality checking. Both are required for theorem checking — but again, Girard’s paradox doesn’t come up often, even in many common types of proofs.
Holy guacamole, it sounds like you and Seroquell wants to turn GHC into the idris2 compiler. Am i wrong or is totality checking the only major feature missing ( compared to that language ) from the blog post?
Idris2 implements QTT, so it’s likely a good idea to draw inspiration from it when figuring out how to combine linear types and dependent types, given that the former are already in GHC.
Totality checking is indeed not planned at the moment. Regarding other major features, I’d have to brush up my Idris2 to properly answer that. Perhaps, if you listed them, I could tell you whether something similar is in the DH plan.
Quantitative Type Theory is useful because it provides a system for writing programs with linearity restrictions and proofs that won’t show up at runtime. I believe the name refers both to the general idea of using 0/1 (linear) annotations, and also to one of the core IRs used in the Idris2 compiler. The surface language desugars to TTImp, which then lowers to QTT.
In your blog post, you mentioned wanting to explore ways to modify GHC Core for better support of dependent types and linear types. In that context, QTT (the IR) is probably the most relevant prior work. (Note that QTT has been in flux and may still receive changes, including to its name. So if this is something you want to look into, I’d recommend reaching out to the Idris2 developers about ongoing work.)
One thing I’m wondering: is totality checking not planned because it wouldn’t be practical in Dependent Haskell, or because it would require too much effort? Or merely because it’s not strictly needed to implement dependent types?
It would be really exciting if Dependent Haskell could eventually support verified invariants or even abstract proofs within the language. But that often (or always?) requires totality checking to prevent unsoundness.
In addition to that, Dependent Haskell would likely need to address issues like Girard’s paradox and related inconsistencies. Do you think soundness — in the sense of supporting logically consistent proofs — is something Dependent Haskell could eventually aim for?
Girard’s paradox has come up before in this context e.g. this thread, where Richard Eisenberg claims it doesn’t really matter:
But I claim we have rock-solid safety (ignoring unsafeCoerce and friends). Divergence in types, whether caused by looping type families or by Girard’s paradox, cannot create a proof of Int ~ Bool. We can know this because the language of erased proofs (that is, coercions) is very limited and has no opportunity for recursion. It is clearly “terminating” because it has no evaluation whatsoever. Yes, we must carefully prove that it’s impossible to get Int ~ Bool during the proof of type safety, but we’ve done that. (And in more painstaking detail than any proof I’ve come across for any of those other dependently typed languages. Do point me to links if I’m wrong.)
Bottom line: we’re as safe as you want to be, where “safe” means that we don’t launch the rockets. (“Safe” does not mean “terminating”!)
I don’t think there is any apetite for changing Type : Type in Haskell, so it will probably always be “unsound”, in that sense.
As for totality, I don’t think anyone has said “definitely not”, and indeed I would really like having the option. But it’s a lot of work, and probably deemed less important, due to Haskell being aggressively partial, and LiquidHaskell already existing.
Thank you very much — you reminded me of something important I was forgetting.
In Idris2, values can be one of three kinds:
Strict (the default) — evaluated immediately
Lazy — evaluated on demand (but cannot be infinite)
Codata — potentially infinite and must be lazy
Idris2’s totality checker essentially verifies that functions return output structurally smaller than their input. This guarantees termination over any finite data structure. It does not guarantee termination for codata — which is expected, since codata can be infinite.
In Haskell, the default is codata, with strict data as an opt-in. Reading through the proposal you linked, I wonder: would that proposal be like adding lazy ?
Termination would already be guaranteed for strict data, but it’s still important to include totality checking — because one might want finite data generated lazily. ( Note: with totality checking , strict data can always be evaluated lazily with no change to program behavior, but including codata still has usability advantages, such being explicit )
That said, I don’t know how Liquid Haskell guarantees totality. Would be interesting to understand how it handles this.
As a side note, some Idris2 users have talked about adding optional universe levels in the next major revision — similar to how totality checking is currently optional. They think this could be something that’s easy to opt into when needed…
Substructural recursion—where a function’s output is structurally smaller than its input—can still be manually justified using dependent types, even in the absence of a totality checker.
I’m not sure whether the Girard Paradox can be mitigated manually, but since universe levels (like totality checks) are typically erasable after type checking, it might be feasible to implement both mechanisms as a GHC plugin that exploit dependent Haskell features.
I’d be interested in exploring an implementation, assuming this approach is actually viable and would allow sound proofs
I believe LiquidHaskell’s termination checker is also based on verifying structural recursion on data. Unlike Idris, however, LiquidHaskell does not verify productivity, so you are out of luck for codata, though see this paper: https://dl.acm.org/doi/pdf/10.1145/3546189.3549922.
I am surprised to learn that Idris has Type : Type, as I was under the impression that it had cumulative universes. I see now that it is a TODO: 1, 2.