Dependent types FTW

http://www.cse.chalmers.se/~nad/listings/dependent-lenses/README.html#1

Good thing they've provided dependent lenses side by side with non-dependent. Cause the dependent version is like 10 fucking times longer. Does anyone really think that dependent types will ever lift off for practical programming? I think that would require fucking autogeneration of proofs but that would make a human programmer obsolete.

Does anyone really think that dependent types will ever lift off for practical programming

Not any time soon. Having extremely rich type systems that let you express and ensure all kinds of strong invariants would be wonderful, but it's not clear how to program larger scale things with this yet and the tools aren't good enough.

Agda is a toyresearch language, it doesn't properly compartmentalize things, it's just for exploration. To be able to really trust a proof you need a small and solid core language for the actual proof verification. Coq has a good solid core theory which more complicated language constructs are desugaraed into, but with this new trendy category theory thing that came along with they're never going to add the axiom that you need to do proper pattern matching.

You're right about autogenerating proofs, that's a big part of making programming with dependent types practical http://adam.chlipala.net/cpdt/ - In no way does this remove the programmer! It's just that even with the best proof search stuff, programming with proofs like this isn't more effective than just hacking shit together in perl and doing your unit tests.

To change this we need to get better at understanding programs, build libraries/a wiki of formally checked mathematics (your not going to be able to write programs with strong specifications and have them typecheck without all sorts of mathematics) and get better tools which are built with correctness in mind as well as supporting proper dependent pattern matching.

>>1

Does anyone really think that dependent types will ever lift off for practical programming?

No. The future belongs to the fuzzy pattern matching system. See http://www.cs.unc.edu/~jtighe/Papers/ECCV10/

Basically programmer would draw a diagram with some annotated arrows, where to place what and what to repeat, and then it would be translated into AST and evaluated, possibly preserving a level uncertainty where needed.

I.e. a diagram with a word "find" (or just a picture of magnifying glass) with an arrow pointing to an image of a cat (pasted from clipboard) and a another arrow pointing to a picture of a hard drive.

>>3

also, a program would ask back with popup window to clarify what it will do.

>>3
>>4
hello machine-learny-man, I saw you in my x86 thread. Have you read "Fuzzy Thinking"?

You remind me of the author: Bart Kosko is the quintessential scientific cyberpunk – a hip, street-smart prophet of life in the Information Age

assertions already work for programmers at a syntax level. A dependently typed language should infer types from assertions.

All this thread tells me is that programming is being dumbed down and autists with no talent want everything to be automated for what purpose? Money. And to do what with it? Nothing but live pathetic, meaningless lives.

>>7
Life is pathetic and meaningless regardless of how you put it, so you may as well do thing that may benefit humanity.

>>8
Stupid edgy kid. You cant even get being a stupid edgy kid right. You say ``Life is pathetic and meaningless regardless of how you put it'' and then say ``so you may as well do thing that may benefit humanity.'' That doesn't fit. It should be ``kill and suicide''. Only pathetic and meaningless thing here is you. Stupid indian-nigger.

>>8
go fuck your daughter again inbred cum skin.

>>10
I would if I had one, so I'll just fuck my sister instead!

>>9
kill yourself, theistard

wow two whole posts ontopic before it devolved into retarded shitposting, that's two posts better than most threads here!

>>12
NO YOU KIWLOWEYOU SE FLEF YOU GIUFKCING FPIECE OF THITSSS!

>>13
A shit post for a shit post leaves the whole board shit.

Dude, I mean how you want to convince some Coproration to buy Dependent Types, when :
- not everyone convinced/want/like to use strong static types.
they slow down development speed, learning speed.
- not everyone convinced to even use FP at production, due lack of support .

Rust doesn't have dependent types, and everyone hyping around it like it's N1 most loved pl, in comparison to haskell somewhere at low spectrum rating position. But Rust have sort of Refined Types.

Gallina, Agda - don't even provide practical io programmging.
You can hallucinate all over type theories, but where does it lead if language you developed can't beat Visual Studio expirience? No one will switch.
You can spend 1 hour writing practical C+PHP or mastrubating to Homotopy Type theory. The choice is yours.