Hacker News Reader

I love Bob Harper's view that something like Type Theory will eventually become the one-true-language. His arguments arise from a POV pretty different from the standard argument here—it's not that some particular implementation will win, but instead that the entire design space of languages we will eventually gravitate to type theory because it's just right.

At the end of the day who wants dependently typed bash?

It's a great intellectual position for happy hour at the campus pub. Yet from a practical standpoint, it's hard to see how programming languages requiring more attention to type system will facilitate banging out code for ordinary problems more quickly.

There are times when it is really important to be able to prove code is correct and times when it is enough to just provide a plausible answer. The market for ML on Rails remains without validation.

Who says it has to feel much at all like DTLs of today? I probably do want to be at least warned when the compiler can't be sure my bash is terminating.

And I'd love Bash embedded in a DT. Even if I never write the DT components being able to nicely map Bash -> DT is powerful.

Finally, I'd love Bash with sum types.

Pretty much every program humanity has produced is grossly defective. Certainly there's nothing I use heavily that hasn't failed. IMHO shipping more garbage more quickly is not a problem worth solving.

<sarcasm>That seems to be the principle use case for Javascript, and that is (arguably) the lingua franca of our generation. </sarcasm>

With something like Haskell (very good type inference) the types will only bother you if you're writing wrong code (or writing particularly complex expressions, I'm not necessarily against compilers complaining about things that are complicated).

It's not a free lunch, but damn is it cheap.

The Haskell compiler will complain if I am writing wrong Haskell code, or more generally when the types are indeterminate and can't be inferred.

This not the same as 'wrong code' in the abstract. The code will run fine if I don't pass in mismatched data, or more generally bad data. And if I am passing in bad data, static typing doesn't give me good answers, it just keeps the program from crashing. Don't get me wrong, there are times when crashing is bad. But there are times when the cost of a runtime error is nominal and the value of flexible code is high.

Static typing trades one type of cognitive overhead for another. The Java program of 500 classes is its manifestation.

What is the cognitive overhead Haskell is introducing? Types? Because as far as I can tell we use types in all OOP, they're just implicit and not checked.

Static type checking, regardless of language, requires thinking about programs in a particular way because one possible mode of failure is prioritized over all other modes. It does so regardless of whether absolute type safety deserves to be prioritized given the purpose of a particular program and it does so regardless of whether absolute type safety is an appropriate concern at a particular stage of the program's development.

Static typing can make "how do I get this to compile?" a design criterion Consider year 2038 problem. In MySQL, various date types are coerced to the timestamp type by design. Otherwise the program would not compile. Compilation takes precedence over problem solving.

http://dev.mysql.com/doc/refman/5.0/en/datetime.html

I've personally found that static typing is an aid to comprehension and thought. I spend more time fiddling with untyped code than typed code. I also disagree that static typing prioritizes a particular mode of failure—the notion of failing to typecheck is a rather general one.

There are two contexts in which one can think about data types. The first choosing among or constructing data types as abstractions. The data type as metaphor is useful regardless of language. An important property of this context is it's not just useful externally via an automobile class in a used car lot application but internally with ports and pipes for I/O and threads and locks and semaphores for processes and so on.

But the other context in which we select and choose and construct data types is because a language insists upon it. Here our choices are not based on how to best represent the world, but by how to package our metaphor into a pre-existing schema. The very first time we compile our code, we have been forced by the compiler to crystallize our code based on an early guess.

When a flat roofed building uses scuppers to provide emergency overflow drainage, it is good if water passing through them makes a mess of the plantings below and perhaps stains the facade. It indicates that the primary drains are clogged before the roof collapses. Likewise, runtime type errors might be preferable to zeros silently inserted into a database.

Static and dynamic typing each catch some types of errors at runtime at the expense of masking other types of errors at runtime.

I think runtime errors are a fine way of detecting such failings. I don't understand why typing is at odds with that.

I think types make us write out the why next to the what. That why might be a domain model justification, or something much more trivial. It's also completely possible to encode an untyped regime in a type system. You're always crystallizing your design, you just can either provide good information to understand its failings and be more prepared to fix them. Or not and chase logic errors throughout an undocumented, dynamic system.

The holy grail of type theory is to write propositions as types and have proofs fall out of those propositions naturally. Those proofs comprise your program. So-called dynamic typing throws that all out the window and just says "I'll permit any program you want to write and bail out at the first opportunity". It's a proposition that is trivially true and thus it's not useful at all.

I think type theory is supremely interesting, and I'm curious to see how far you can take it. I worry a little that at some point your type system needs its own type system, and then we've just moved the argument about typing one level of abstraction deeper.

I'm not willing to concede that strong static typing is a universal truth though. Too many people much smarter than me seem to disagree.

This is a solved problem; they are called Universe Types.

> It seems weird to think that there exists any language currently which will wind up being the one-true-language.

Odd, but not uncommon. Programmers are prone to falling in love with their tools. I've seen a lot of one-language-programmers proclaiming the advantages of their language choice over every other programming language. Luckily, this is not the case with this article. Still, I don't think there is One Language to Rule Them All.

i never understood the sentiment, that people are afraid that their tool of choice becomes "mainstream" popular

i think people argue a lot about which language is better, because programming languages need to be popular

they need to be popular, because this is the best guanranty they will have lots of good quality libraries

and a bad language with good libraries trumps a good language with no libraries

if haskell becomes "ruby" popular, and haskell i believe is actually one of the more popular functional languages, you will only benefit

I think people's negative reaction to "hipness" is just human nature, and while I completely agree it's a terrible reason to make decisions about things, I'm not certain it's able to be overcome completely.

I think people argue about which language is better for much the same reasons they argue about which mobile phone operating system is better, or which console, or which text editor. They've invested (in the case of programming languages, potentially many years) in something, and want to feel like they've invested wisely. I think that's also probably just human nature.

I disagree with the notion that programming languages need to be popular, at least, as popular as they needed to be in the past.

20 years ago it was important for languages to be popular because that was the only way they'd reach enough critical mass to be discoverable. Growing up, there was only one book store within driving distance of my house that had any programming books. That meant if you wanted to learn programming, you were limited to what had been "blessed" by industry (in my case, one book on C++ that was actually just a syntax reference). That seems to no longer be true (the internet has made discovery of programming languages easier in much the same way it's made the discovery of everything easier).

There is certainly a benefit to having critical mass, but that mass seems to be much smaller than has ever been required in the past. I've seen Haskell developers on several occasions talk about the fact that Haskell's popularity has been in this nice "happy medium" that provides enough eyeballs to flush out issues and provide feedback, but also allows them to not worry about breaking things.

A language getting popular is not all benefits with no drawbacks. It gets harder to make breaking changes to the language (Javascript can be considered a good cautionary tale about what can happen when a language becomes so popular that you are held hostage by backwards compatibility). And you can't read a single article on here about some less popular language that doesn't prompt at least one comment about how because the language isn't popular, the quality of developers using it is higher (which is always posited as a plus for hiring developers in that language). Paul Graham mentioned it regarding Python explicitly in one of his essays.

More people being part of a community means more everything. More of what's good (libraries, eyes looking at bugs, ideas on solving problems) and more of what's bad (bike-shedding, shitty libraries, conflicting programming idioms).

I have no idea if there's some magical sweet spot, where you get all the benefits of a language being popular without any of the detriments; but I suspect it doesn't exist. As it stands, yes, I'd like there to be more Haskell libraries. I'd like there to be more blog posts about using Haskell for things that aren't abstract math. But I'm not necessarily itching for Haskell to become much more popular.

We're already starting to see some of the industry people that use Haskell start to explicitly target evangelism (like the work FP Complete is doing). I think it's great that they want other people to use this thing that they like, but I am worried anytime a community switches from "stealth" mode to "evangelism" mode. Incentives around addressing problems starts to become perverse when you have to worry about messaging, and when you're trying to convert other people. It seems like it evolves eventually to cargo-culting.

well, most open source projects have a small set of core developers, a larger set of testers (users who discover bugs and report them properly) and larger set of passive users

being more popular will only slighly enlarge the core, and keep it healthy (if a member drops, someone else comes in)

popularity is good for OOS projects ... i also disagree that a larger community will increase the bad, again the core developer size will probably remain small enough to work coherently

more testers cannot be bad more libraries can never be bad, it will just increase the likeleehood of having good ones happen

another reason for languages need for popularity is that it really take a lot of time and effort to master one if you spend years mastering a tools, you sure want it to be popular for more years ... to get a chance to use this knowledge

More users means more people who feel breaking changes. If you have one user, and someone demands a change that might be breaking, there's a pretty good chance everyone who feels that is willing to go to the effort of fixing up any breakage. If you have ten million users and someone requests a change that might be breaking, you've got to treat it much more carefully.