I guess I better lay out why I'm skeptical of dependent types being all that great for Haskell, so here's a thread https://twitter.com/mattoflambda/status/1356620065114886144

Haskell is *absurdly good* for developer productivity.

Sure, we don't have an IDE, but the cost of maintaining a codebase grows way slower than the actual codebase, whereas other languages have like quadratic maintenance costs

This is true of Haskell2010

Add in the GHC2021 suite of extensions and it's Even Better, but there's a bit of extra complexity cost, but it's worth it!

Then you throw in type-level computation and suddenly the trade-off isn't so good.

You're adding a *lot* of complexity, so the cost is very high.

Paying back that complexity cost requires a lot of taste and care - you gotta make a lot of mistakes to know what's worth it

Dependent Types makes an offer:

"I'll dramatically simplify the type/term language, so type-level programming isn't as complicated, and then it's easy, and the cost-benefit analysis for type-level programming is fine!"

I'm very skeptical on this offer.

For credentialing purposes:

I've worked through "Type Driven Development in Idris," I know about the Lambda Cube, I've implemented a toy dependently typed lambda calculus, and I've played with my fair share of Haskell type-level programming.

Dependent Types are inherently hard

Even in Idris, a language designed primarily with dependent types in mind, it's hard! There's no getting around it. You have to start worrying about formally proving properties and carrying those proofs around.

Proofs are structural, so implementation details leak.

I don't doubt that a dependently typed language would be better than the nightmare that is TypeFamilies, but it has a Use

it serves as a Warning that you're entering Bizarre territory

The syntactic accessibility of a technique should correspond with the conceptual/UX difficulty

Dependent Types don't solve the problems that Haskellers commonly report, and I bet they'd make them worse.

- Reasoning about performance
- Debugging type-level computation
- Finding Haskell jobs
- Structuring Large Applications
- Long compile times https://taylor.fausak.me/2020/11/22/haskell-survey-results/#s6q17

You think reasoning about performance is hard? Just wait 'til you have to pass runtime proofs around!

Type class constraints can have odd performance characteristics, preventing memoization/inlining/other optimizations

Proofs will make this *much worse*

Now, to compute the runtime of a function, you need to also consider the runtime of the *type signature*.

Good luck! Haskell is fast, but it's easy to make it slow.

I can't wait for the first bugs to come around because `sum` at the type-level is too lazy.

Debugging type class instance resolution or type family evaluation is a nightmare.

GHC has no visibility in how or why certain choices are made

The error can easily propagate pretty far from the source, giving you a message that seems totally unrelated

With experience and a bit of that Arrakis spice, I've been able to mind-meld with GHC and I can kinda trace these errors now

I don't know if I'm capable of tracing them with full dependent types.

But maybe we'll get `Debug.trace` at the type level, so it's fine.

Finding jobs (esp. for juniors) is very hard, and I've diagnosed the problem as "we write code that's way too complex"

Dependent types will make this worse, not better.

https://www.parsonsmatt.org/2019/12/26/write_junior_code.html

No one has written a large application with Dependent Types.

No one knows how to do it!

At some point, that knowledge will percolate out, but we're in 2021 and pragmatic Haskell books are still very rare (ahem @prodhaskell).

I doubt DT will be any faster.

Dependent Types will make existing application architecture patterns more complex, not less.

Between mtl, ReaderT, and effects-systems, we're not sure how to pass *runtime parameters* around.

So good luck on figuring out how to pass proofs around.

Alright so let's hit that last bullet - compile times.

GHC is a remarkable compiler. It can do a *lot* of work for us, and that work takes time.

TypeFamilies are one of the slowest parts of GHC. Next up is `DeriveGeneric` and other straightforward derivations.

Dependently Typed programs are going to be unimaginably slow at first.

The toy examples will be fine, but then someone will program an extensible record with 40 fields to model a database table, and it'll come crashing to a halt.

Faster compile-times lead to a faster development feedback cycle, which is critical for productivity.

Anything that slows that down better pay a *huge* benefit, or the time costs of waiting on GHC to recompile will be overwhelming in the long run.

The real problem - and I touched on this in the @haskellweekly podcast - is that "software productivity" is improved so much with Haskell already that improving it any further *doesn't actually help productivity*. https://twitter.com/haskellweekly/status/1356226620479184900

Haskell projects tend to be exceptionally high quality and robust.

They also tend to be poorly documented, have bad observability, and are difficult to learn.

Dependent Types will double-down on this difference. That's going to make things worse, not better.