3 ms·

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 wh

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.

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.