Name: Anonymous 2014-05-05 17:39
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.
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.