Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Summer of Programming Languages

existentialtype.wordpress.com

Post reply on HN
Print view View original

11–20 of 78 posts

Re: Summer of Programming Languages

#11

Post by chipsy »

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.

It's a form of automation, which is, for understandable reasons, the most popular form of "progressive" PL thought. With a very powerful type system, the compiler can make inferences about the program that would otherwise be the programmer's burden. A powerful type system that is also safe allows whole classes of errors to either cease to exist, or be moved from runtime testing(where the programmer needs time and debugging skill to pinpoint their origin) to a compile-time error message. Either way, effort is saved each time the type system catches one of those errors.

Re: Summer of Programming Languages

#12

Post by pjmlp »

lmm wrote: post #10
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.

Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wr…

My experience with unit tests for dynamic languages as a replacement for proper static typing done at the compiler level, is that it just doesn't work.

Sure it works for the lonely coder or small shops, but as soon as the project scale increases anything goes.

Managers will push for features over unit tests, no one will refactor code without taking a few days with the caveat not all places will be touched and the team atrition will bring in new devolpers forced to read implementation code to be sure how to properly call the functions/methods.

Advanced static typed languages with HM type inference are a better option for large scale development.

Hence it may be that is harder to get funding for other types of research.

Other issue is that dynamic languages fo their very nature make tooling harder problem to solve, hence less interesting for many researchers, pressed with delivering quick results.

Re: Summer of Programming Languages

#13

Post by chriswarbo »

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.

In the case of Robert Harper in particular, see this blog post: http://existentialtype.wordpress.com/2011/03/19/dynamic-lang...

Re: Summer of Programming Languages

#14

Post by eli_gottlieb »

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.

Type-safe languages allow you to check the correctness of a program by proving a theorem about it: it will never suffer from implementation-defined, unspecified (by the language) behavior. Because of this property, programs written in a type-safe language have many more traces corresponding to the programmer's intention, by default, than programs written in unsafe languages. The tradeoff is that the programmer can have a harder time expressing his intentions.

Re: Summer of Programming Languages

#15

Post by jballanc »

lmm wrote: post #10
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.

Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wr…

I don't necessarily think they are wrong, but I also think that (as with most "silver bullets") type-safety is not without it's shortcomings.

For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer

Except, that's wrong. When we raise an Integer to a negative Integer (2^-2), the result will be some fractional value. If we want to retain full numeric precision, it'll have to be something like a Rational. So now your function's type signature is: Integer -> Integer -> Rational.

But that's also wrong. So what are we to do? Maybe positive and negative integers should be separate types? PositiveInt and NegativeInt, let's say. But then what about subtraction? Should it's type signature be: PositiveInt -> PositiveInt -> PositiveInt? What about 2 - 3? Whoops!

So, there's no way, with types alone, to simply and accurately encode all basic math operations. All you can do is throw a Domain Error when someone violates certain boundary conditions, and tell them to check their arguments before deciding which function to call.

...meanwhile, dynamic languages will happily return whatever type is most appropriate for the arguments given.

Re: Summer of Programming Languages

#16

Post by lmm »

jonnybgood wrote: post #7
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…

> but none of these languages have much foundation in category theory or the ambitious kind of type system that Haskell has been pioneering for a while. Is that a requirement? If so, why?

I've never seen a "bolt-on" type system work, and I've used a few (e.g. JSR308). So I think it's something that needs to be built into the language itself.

Having used a system with higher-level type constructs I find myself thinking in them. So many complex sequences of operations shake out as something much simpler once you realise the right monad, or arrow, or so on. And it becomes painful to manually expand it out; it would be like working in a language without generics. So I couldn't stand to work in a language that can't express these concepts; I need either higher-kinded types or something equivalent to them.

And for a type system that powerful, I'd want some assurance it was correct. Theoretical underpinnings are not the only way to do that - if it had been in use a while, and had enough tests and experience to give me a decent level of confidence, that would be enough. But for a new language I think the only way I could be confident enough to use it would be if it had this kind of theoretical backing.

Re: Summer of Programming Languages

#17

Post by lmm »

jballanc wrote: post #15
lmm wrote: post #10

Earlier quoted context omitted.

Academics don't care so much about things like programming speed. And the academic environment focusses on proof; a type-safety property will seem much better than a unit test even when both took the same amount of time and have the same practical value. (For all that, I agree with them though. Maybe the reason programming languages researchers think that is because it's true? Do you have reason to believe they're wr…

I don't necessarily think they are wrong, but I also think that (as with most "silver bullets") type-safety is not without it's shortcomings. For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer Except, that's wrong. When we raise an Intege…

Any property that you can actually be confident about, you can encode into the type system. If you care that x ^ (y - z) is an integer, you'd better have some reason to believe that y > z. If you don't care or can't be sure, let x ^ (y - z) return Integer | Rational, and pattern-match for the cases (or treat them as some supertype, Numeric or some such). Or if you really can't figure out the proof but still think it's correct, you can cast, and then your program will error out at runtime if you're wrong, which is at least safe.

In a dynamic language, your mistake passes silently; the result you thought was an integer is actually a fraction, but your program carries on going. Maybe it turns it into a string and uses it as a file path, so something you thought was a simple filename has a slash in it. Maybe that breaks your security model. Pretty unlikely in this specific case, but that's how bugs happen.

Re: Summer of Programming Languages

#19

Post by jballanc »

lmm wrote: post #17
jballanc wrote: post #15

Earlier quoted context omitted.

I don't necessarily think they are wrong, but I also think that (as with most "silver bullets") type-safety is not without it's shortcomings. For example, consider the exponentiation function. When we raise an Integer to a positive Integer (2^2), the result will always be a positive Integer. You would expect the type of such a function to be: Integer -> Integer -> Integer Except, that's wrong. When we raise an Intege…

Any property that you can actually be confident about, you can encode into the type system. If you care that x ^ (y - z) is an integer, you'd better have some reason to believe that y > z. If you don't care or can't be sure, let x ^ (y - z) return Integer | Rational, and pattern-match for the cases (or treat them as some supertype, Numeric or some such). Or if you really can't figure out the proof but still think it'…

Right, but it's also much simpler and faster for the programmer to write one function with one return type, and later modify it to add a return type if the requirements change. I think this is obviously why dynamic languages rose in prominence coincidentally with the rise in rapid prototyping and agile development. That said, this is also why large companies with codebases that need to be maintained over multiple decades will always go with static languages.

What really interests me are languages like Julia or Dart, with their gradual typing, or Clojure and core.typed. You retain the flexibility and speed of development of a dynamic language, with the possibility of later adding type safety guarantees to your code without having to rewrite it from scratch.

Re: Summer of Programming Languages

#20

Post by fit2rule »

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.

I would say its because academic researchers don't spend nearly enough time actually using these languages industriously in the worst-case scenarios. If more effort was spent in understanding how, for example, SIL-4 (safety integrity level 4) development is done with non-type-safe languages (hint: code coverage tests, tests, tests..), then there would (imho) be less motivation to continually churn out 'new solutions to old problems' .. which have been solved, already.

Fact is, if you can't trust your language because of its type system, you develop tools to build that trust around your particular application of the language. If that is 'too much work for you' .. then by all means, avoid the work by reinventing the wheel. In Academia, you can get away with that because you don't have customers, and you don't have an industry demanding results. At most you have peers whom you have convince that steering their groupthink in your direction is worth the effort.

Post reply on HN