Hacker News Reader

Comment by typesafety | Hacker News Reader

There are numerous holes in the type system. Just browse their bug tracker to see. And several of them are not just "bugs" but deep flaws in the type system.

View on HN

I think the key thing is that there is no mechanism to be sure that messages you send to actors are immutable. There is a compiler plugin in development to help, though.

That's really a different issue than type safety.

Indeed, you are right...

http://www.slideshare.net/jboner/akka-talk-at-geneva-jug-sca...

slide 34: immutable msgs , typed actors

The same could be argued of Haskell and many ML derivatives. Do you think this is particularly clever to point out?

So I'm curious, can you point to known problems with Haskell or ML that do not involve using the unsafe features? Scala has problems even without resorting to "unsafe" features like casting or native methods.

GHC 7 recently broken with the traditional ML type checking / inference mechanism because it's not expressive enough for the kind of the code that Haskell wants to support. Noone has this stuff figured out, certainly not ML, Haskell, or Scala. Benjamin C Pierce has even written about how some domains are positively painful w/ strong type systems and how contracts are a more expressive solution.

I'd like to see the ideas behind the Art of the Metaobject Protocol applied to type systems. Allow users to selectively fill those holes that relevant for their domain.

I don't see any mention of a specific safety problems. Plus, I am given to believe that there are actually numerous papers on the extensions involved in the Haskell type system. Consider http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn

That is the paper I'm referring to. Type safety is an arms race with expressiveness and the paper pretty much says so.

REPLY: You're argument is reductive to the point of being useless - i.e. you could write a type checker for a domain of programs so small as to be comical. type safety and the domain of the provable programs are inextricably intertwined.

I guess I'm not following, because type safety is a property of typed language. Expressive power is orthogonal. There are type systems that are more expressive and less expressive and ideally you design your language so that regardless of where it lies on the spectrum it has type safety. Otherwise, the type system does not really provide you with any real guarantees.

"I guess I'm not following, because type safety is a property of typed language. Expressive power is orthogonal."

This is where you have it wrong, and it's well known that it's wrong. Anyways...

Scala's is a series of compromises made to give a more expressive type system to a language that interacts with the JVM and and Java libraries. Saying its not "safe" to some arbitrary metric is neither insightful nor helpful to anyone. You can find it as "ironic" as you like, but it's not a particularly fair criticism by many metric.

I'm guessing you've never actually proven type safety for a non-trivial language, if any. While there are many ways type safety could be stated for Scala, I'm pretty sure most Scala programmers would like the version of type safety that states "if I never use a type cast, I can never get a class cast exception." If you think that is too strong of a statement, then fine, but I think most people would agree this is a reasonable expectation for Scala.

a type system can be both logically consistent and expressive. the trade-off is with things like the efficiency with which it can prove the program is correct (and even the possibility that it cannot be proved at all).

what typesafety is talking about is errors. not trade-offs. that the type system says something is safe when it is not.

Please point to a few.

https://lampsvn.epfl.ch/trac/scala/ticket/963 https://lampsvn.epfl.ch/trac/scala/ticket/2856

among others

Hm... As an early Scala/Akka developer, and contributor I would like to see these issues addressed by the team because I'm seeing a lot of trac jacking going on. This usually only happens when there isn't a response to issues.

Are you of the opinion that the problems with the Scala type system are unfixable?

I would like them to be fixable, because otherwise Scala is a decent language, but it is too early to say.

Hi Tony,

isn't #963 more or less fixed? (It crashes the compiler, but doesn't fail at runtime anymore ...)

Could you post a new example of it if it isn't?

Isn't crashing the compiler pretty far to the "less" side of "more or less fixed"?

Failure to compile is always better than generating wrong bytecode.

Right, but I don't think "fixed: replaced with compiler crash" is a resolution you'll see in many bug databases

Reply on news.ycombinator.com