I am not aware of a viable "dependent type system". Such ones as we have are very complicated and not generally a good engineering trade off.

It is The Dream in some ways, but it is much, much easier said than done.

▲

Ericson2314 8 months ago | parent [-]

We've head them for 20 years. Lean is getting a lot of attention. Dependent types are not very complicate --- proofs are very complicated, but that is inherent. Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

▲

jerf 8 months ago | parent | next [-]

I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.

Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.

I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.

	▲	Ericson2314 8 months ago \| parent [-]
		> not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages. Well, to be fair, I would not cry if this happened. > Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical. I wrote a tic-tac-toe in Lean. https://github.com/Ericson2314/lean-tic-tac-toe/. Yes, it took me far longer than I would have in Haskell, but that is just because: 1. Unfamiliarity with the standard library, tooling etc. I didn't expect Applicative to be in mathlib not batteries, for example. 2. I tried to prove things I wouldn't have in the Haskell version If I knew the standard library, and did plane old arbitrary-length lists and partial (bounds-checked) indexing with arbitrary nats, I would have had less fun, but also done things way faster. I am excited for the latest Machine-Learning tactics or whatever too, but the idea that "everything is going to do something they didn't before (proofs) and it will be no harder" is not a goal I am aiming for. Proofs will always be a trade-off between up-front costs and fearless refactoring on an ongoing basis. That's OK! I don't expect magic, I just want my programming language to give me the full spectrum of options, and then I can make my own economic decisions.

▲

zozbot234 8 months ago | parent | prev [-]

> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.

	▲	Ericson2314 8 months ago \| parent [-]
		> You can recover a sort of phase distinction Yes the literature says how to do this. It's not hard. Any program that could be written in something weaker like System F will have the same erasure. > inherently involve a kind of compile-time evaluation. compile-time evaluation doesn't pose a phase-separation problem. Indeed, nothing to the right of a `:` will ever need to be evaluated on runtime.