Hacker News Reader

Comment by Mythroat | Hacker News Reader

Is there a reason dependent types are not more common?

They've been historically hard to implement in a way that is both efficient, sound, integrates with effectful code, promotes code reuse (like in Haskell), and has good developer UX (good error messages and IDE support). I believe we are getting to a point where it is feasible, hence I'm messing around with it myself [0], but it can be challenging to navigate the terrain of papers and theory as a language designer. While DTs themselves are quite simple, the integration with other features users expect is tricky, and producing a production-grade compiler is definitly not as straightforward as making a regular Hindley-Milner style language.

[0]: https://github.com/pikelet-lang/pikelet/

They can make libraries a pain. Like imagine if someone write a library in C#2025 with dependent types where functions took parameters like [i: i%2 == 0] or whatever. And your big project has no existing dependent types. There's no way to adopt this library unless you pull dependent types all the way in.

Or even if you did, but your types were [i: i%4 == 0] or [i: (i+1)%2 == 1] or whatever, you'd have to write proofs that they types were compatible. Even some simple things are just not worth it.

Maybe some form of gradual typing like TypeScript is somehow possible? And also like TypeScript, a repository for declarations for popular libraries.

If the project had no existing dependent types at all, couldn't you just perform a runtime check before calling the library? The check would return evidence that [i: i%2 == 0] for the particular i, or fail at runtime. If it succeeded, then you could invoke the library using the new evidence.

One appealing aspect of dependent types is that they let you decouple validation of inputs from the function calls themselves, while still disallowing passing wrong inputs to the function by mistake.

Yup, lots of people are under the impression that you need to prove everything when it comes to DTs. That's not true - you can indeed push these checks to runtime, and just have the compiler make ensure you do it.

You could just assert that i%2 == 0 via some postulate - as long as the proof is irrelevant for the code that is. Doing so is similar to converting from any in a gradual type system: if the assertion is correct you get correct code with little work and if you're uncorrect you're no worse off than if you had no types at all.

There are difficulties with dependent types, but having to go all in can be avoided via a shift in culture.

Wondered that myself. It’s surprising there’s not more languages with dependent types (and the associated requisite libraries).

I suspect it’s taken a while for the theory behind dependent types to become widespread enough for some enterprising hacker or grad student to make a useable language for them (e.g. Idris). Even if a new theory comes along it takes time for appropriate metaphors and methods of using them to be created and disseminated.

Though does computing the dependent types at compile time take more process.

Imagine having to prove a Coq theorem for every function call.

No, it's not really that bad. But almost. I really suggest you play with Idris some; what you can do with it is brilliant, for simple tasks. For complicated tasks, like the fully general propositions you need for library functions, it can get much more complicated than the code itself.

Try to write the classic Haskell Quicksort in Idris:

    qsort :: Ord a => [a] -> [a]
    qsort [] = []
    qsort (p:xs) = qsort (filter (< p) xs) ++ [p] ++ qsort (filter (>= p) xs)

and let me know how it goes, if you will. That's when I gave up on Idris.

This one liner isn't really quicksort anyway.

They're very difficult to use and they make code more complicated.

Reply on news.ycombinator.com