Summer of Programming Languages • Hacker News Board

Re: Summer of Programming Languages

#51

Post by tel » Mon, Jul 07, 2014, 4:01 PM UTC

steveklabnik wrote: post #47

Dewie wrote: post #24

Earlier quoted context omitted.

> I need either higher-kinded types or something equivalent to them. FWIW it seems that many of the Rust developers want this for Rust.

Yes, many of us do. Using Option/Result can often lead to a lot of pain without their accompanying monads, and while you can write the specific ones (there's a try macro for using Option), it'd be much, much nicer to just have monads be possible in the language itself. However, the Rust team is trying to get 1.0 out the door, and higher-kinded types would be backwards compatible, so I don't think we'll be seeing them…

The backwards compatibility argument is interesting. I think it's really compelling, but it's also worth taking into account the pains that the Haskell community has been feeling since standardizing the standard library as insufficiently generic.

I have no idea if a similar problem is possible with Rust, but it'll be interesting to see how HKTs enter the scene if and when they do.

Re: Summer of Programming Languages

#52

Post by freyrs3 » Mon, Jul 07, 2014, 4:27 PM UTC

tel wrote: post #43

aidenn0 wrote: post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows. He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered. He begins by first rigorously defining what he means by "type". In particular, it's a piece of informatio…

> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation".

That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it's technically wrong per se, but it only makes sense if one is discussing programming languages purely from first principles. Harper seems really taken aback by the popularity of Haskell compared to SML in the functional programming space, and yet can't seem to wrap his head around the reason for the adoption is not so much about having ideal PL semantics but the fact Haskell has an industrial-strength cross-platform compiler with meaningful answers to modern problems ( FFI, concurrency, package management ). Haskell is rather unique in that it has a community that seems interested in building a language as both a "means of expression" and "tools for creation" and we've made some compromises between the two, no doubt. A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.

Re: Summer of Programming Languages

#53

Post by tel » Mon, Jul 07, 2014, 4:41 PM UTC

freyrs3 wrote: post #52

tel wrote: post #43

Earlier quoted context omitted.

One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows. He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered. He begins by first rigorously defining what he means by "type". In particular, it's a piece of informatio…

> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it'…

I'm always reminded there's a long-tail to research. It's sad that so much focus goes to the peak of that distribution, though. I think the tension between useless and useful is really important!

Re: Summer of Programming Languages

#54

Post by pcwalton » Mon, Jul 07, 2014, 4:41 PM UTC

gnuvince wrote: post #5

zak_mc_kracken wrote: post #4

> Nowadays serious industrial-strength languages are emerging that are grounded in theory and informed by practice. This seems a bit overly optimistic, but it's nice to see this kind of positive attitude for a change instead of "Why invent yet another language?". I am very excited about Swift and I have some respect for what Rust is trying to accomplish, but none of these languages have much foundation in category th…

I recall reading that when Niko joined the Rust project, he kept uncovering places where the type system was unsound and was instrumental in making Rust type-safe. Can anyone confirm?

Well, we basically knew where the problems were, but Niko helped us come up with a way to fix them that was usable (the borrow check).

Re: Summer of Programming Languages

#55

Post by chriswarbo » Mon, Jul 07, 2014, 5:05 PM UTC

seanmcdirmid wrote: post #28

aidenn0 wrote: post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

There are also PL researcher who are enamored with dynamic languages. Alan Kay probably doesn't care much about static types.

Indeed, Gilad Bracha isn't a fan of static type systems.

Re: Summer of Programming Languages

#56

Post by l_dopa » Mon, Jul 07, 2014, 5:35 PM UTC

freyrs3 wrote: post #52

tel wrote: post #43

Earlier quoted context omitted.

One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows. He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered. He begins by first rigorously defining what he means by "type". In particular, it's a piece of informatio…

> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it'…

> A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems.

That's a tempting view to take regarding theory vs. practice but I don't think it holds up when you consider Harper's whole body of work and the substance of his criticisms of Haskell: He has published extensively on ML implementation and, as far as I know, has offered criticism of (GHC) Haskell's type system where it is unsound, never the (really cool) work being done on the RTS.

Re: Summer of Programming Languages

#57

Post by freyrs3 » Mon, Jul 07, 2014, 5:53 PM UTC

l_dopa wrote: post #56

freyrs3 wrote: post #52

Earlier quoted context omitted.

> Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". That's a very concise way of putting it. My personal issue with a lot of what Harper writes is not that it'…

> A lot of Harper's comments ( and many PL theorists ) seem to completely casually gloss over the gritty compiler engineering as if it's just beneath them, and that guys like SPJ and Simon Marlow are just wasting their time working on faster runtime systems and optimizations when he thinks they should be working on foundational "Holy Trinity" problems. That's a tempting view to take regarding theory vs. practice but…

I've read his papers and I own his books, so I'm not entirely unfamiliar with his contributions to the field. But I also find his criticism of Haskell to be at best detached from reality and a "holistic" view of the programming profession as a union of theory, engineering, and community. Especially when he's arguing for the use of pure academic languages like Agda or antiquated ML-dialects that haven't seen active development in 15 years, over a productive language like Haskell. In an industry where regression languages like Go and Javascript are seeing wide adoption, I think his grandstanding does a lot more harm than good.

Re: Summer of Programming Languages

#58

Post by andolanra » Mon, Jul 07, 2014, 6:01 PM UTC

tibbe wrote: post #38

rwmj wrote: post #23

Earlier quoted context omitted.

Types are no silver bullet, however one important point missed by all the other replies is that static types check all paths through the program, including rare/untested/error paths. You can sometimes make up for this with lots of testing and detailed code coverage analysis, but that can be a huge amount of effort, and might be impossible in some cases (for example: how do you easily test that your program behaves we…

There are cases you cannot really exclude by testing. For example, guaranteeing that certain function never receives a null value.

It is true that some things you just need to test, but nullability isn't actually one of them. Many languages—including SML, Haskell, Rust, and Swift—encode nullability in the type system, so those languages can guarantee at compile-time that functions never receive null values.

Re: Summer of Programming Languages

#59

Post by aidenn0 » Mon, Jul 07, 2014, 6:06 PM UTC

coldtea wrote: post #30

aidenn0 wrote: post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

> Why do programming languages researchers seem so enamored with type-safe languages? For the same reason people like unit tests. Only with mathematical rigor, checked by the compiler, and inspecting all aspects and code paths.

I agree that type-safe languages give a lot of the advantages of unit test.

I actually don't understand why those who advocate for TDD don't rather advocate you write everything in something like ATS. Every single argument I've seen for TDD would apply even more strongly to doing that.

I tried doing TDD style development for a while, and I found these two things to combine to make it unfeasible"

1) For significant amounts of real-world code writing correct tests is actually harder than writing correct code.

2) In real life you end up discarding much of the code you write.

This means that you end up spending a lot of extra effort to write well tested code that will never end up being run in production.

I find quality integration tests combined with some form of analysis of the more critical parts to be far more productive than TDD.

The equivalent for type-safe would perhaps be type-optional languages like Qi/Shen. I haven't messed around with it much, but it seems to offer rapid prototyping with an enforced type-safe mode that can be turned-on later. Unfortunately its inference engine seems to be inferior to ML or Haskell right now, so transforming code from non-typesafe to typesafe is a bit of a slog (I last tried it a year or two ago, so it may have improved in the meantime).

Re: Summer of Programming Languages

#60

Post by aidenn0 » Mon, Jul 07, 2014, 6:11 PM UTC

tel wrote: post #43

aidenn0 wrote: post #9

Why do programming languages researchers seem so enamored with type-safe languages? It seems to be a given in academia that type-safe languages are not just superior, but significantly superior to type-unsafe languages.

One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows. He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered. He begins by first rigorously defining what he means by "type". In particular, it's a piece of informatio…

Thank you for this very well written and thoughtful response. It definitely answers some of my questions. I tend to come at problems from empirical and intuitive angles, so arguments from first-principles tend to be lost on me.

This is likely because my first encounter with formal reasoning was in the field of classical philosophy, and many things I empirically knew to be wrong had been "proven" from first-principles in the literature.