4 ms·

Is there a reason dependent types are not more common?

daxfohl 8y ago
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.
- 21 8y ago
  Maybe some form of gradual typing like TypeScript is somehow possible? And also like TypeScript, a repository for declarations for popular libraries.
- danidiaz 8y ago
  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.
  - bjz_ 8y ago
    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.
- Zalastax 8y ago
  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.
elcritch 8y ago
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.
mcguire 8y ago
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.
- deleted 8y ago
  [deleted]
tree_of_item 8y ago
They're very difficult to use and they make code more complicated.
bjz_ 8y ago
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/ https://github.com/pikelet-lang/pikelet/
etatoby 8y ago
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.
- AzzieElbab 8y ago
  This one liner isn't really quicksort anyway.

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.

21 8y ago
Maybe some form of gradual typing like TypeScript is somehow possible? And also like TypeScript, a repository for declarations for popular libraries.
danidiaz 8y ago
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.
- bjz_ 8y ago
  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.
Zalastax 8y ago
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.

elcritch 8y ago

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.

mcguire 8y ago

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.

deleted 8y ago
[deleted]

tree_of_item 8y ago

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

bjz_ 8y ago

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/ https://github.com/pikelet-lang/pikelet/

etatoby 8y ago

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.

AzzieElbab 8y ago
This one liner isn't really quicksort anyway.