3 ms·

> if (false) 23 else null Why isn't the type of this expression Null?

• harveywi 11y ago
  Because the type "Any" is the least upper bound of Int and Null. http://ktoso.github.io/scala-types-of-types/#unified-type-system-any-anyref-anyval http://ktoso.github.io/scala-types-of-types/#unified-type-sy...
  • p4bl0 11y ago
    I guess GP's point is that it can be statically determined that the given expression evaluates to null.
    • chrisseaton 11y ago
      To support this wouldn't you have to encode in the language spec the exact set of constant folding optimisations applied? Just 'false' is a trivial example, but maybe your compiler can see that 'true && false' is false, but mine can't? What about if the expression is some massive operation that could theoretically be found to be constant, but no real compiler is actually going to do that. You'd have different compilers determining different types based on optimisation which are supposed to be transparent. Doesn't seem desirable to me.
      • lsd5you 11y ago
        Besides, I would say (in my experience) having 'false' like this will tend to occur when debugging, to force a certain execution path. In this case it is undesirable for the compiler/model to change the static type since that may then let you make other changes which you should'nt be making, or cause compiler errors further down.
      • junke 11y ago
        This is how the existing type checker works, from primitive types and combination rules. Some rules are more precise than others, though. I think in Scala the type system does not depend on the implementation, but it is specified by the language.
        • chrisseaton 11y ago
          But 'false' isn't a type, it's just a value. The Scala type system doesn't encode boolean values as far as I know (not an expert).
      • CuriousSkeptic 11y ago
        Not necessarily, it could also be a result of encoding literals as types. If true is the unit value of True a subtype of Bool you could probably have the typsystem figure out which overload to look at (True,False or Bool) From my understanding DOT could turn out to be quite similar to this pure subtype approach http://lambda-the-ultimate.org/node/4835 http://lambda-the-ultimate.org/node/4835 so isn't that farfetched either.
  • junke 11y ago
    Well, sure, but the over-approximation is surprising given that false is constant and "if" is supposedly a well-known construct.
    • octo_t 11y ago
      thats a very slippery slope. - (0 < 1) is a constant. - ((10 + 10)*15 > 0) is a constant. where do you draw the line in the type checker at working these things out?
      • adriaanm 11y ago
        Exactly. The type checker does track constants (`false` internally has type `Boolean(false)`), but it won't drop `if` branches. That happens later, as you can see in the (abridged) output of `scalac -Xprint:all -Xprint-types`: [[syntax trees at end of typer]] // constif.scala class ConstIf extends scala.AnyRef { def m: Any = if (false{Boolean(false)}) 23{Int(23)} else null{Null(null)}{Any} } [[syntax trees at end of refchecks]] // constif.scala class ConstIf extends scala.AnyRef { def m: Any = null{Null(null)} }
      • pklausler 11y ago
        Probably somewhere before "if (halts(f,x))".
      • lfowles 11y ago
        Related to sibling comment, is the halting problem an issue if you just allow expressions without recursion/loops? Along the lines of constexpr in C++.
    • tikhonj 11y ago
      What you're suggesting is essentially combining some sort of partial evaluation with type-checking. This is going to be hard to do in a consistent, intuitive way: either you only do a very small number of obvious cases (like if (false)) which is not all that useful and just adds complexity or you try to do it in a principled fashion which is difficult and still inherently limited. Right now, the typing rule for if in Scala is reasonably simple. The condition is a boolean and the whole expression is the least upper bound of the left branch and the right branch. How much more complex would this rule have to be if it needed to fully specify when the condition gets simplified? To be sure, your idea is interesting and could probably be done well in another language. I wouldn't be surprised if this sort of capability naturally comes up in some dependently typed systems. But it wouldn't work very well in Scala: you'd be adding a lot of complexity for relatively little gain.
• Manishearth 11y ago
  This generally falls under the purview of optimizations, which are executed after type checking. In most languages type checking has little to do with the runtime values and everything to do with types. The existence of a bottom type via exceptions and returning is somewhat an exception to this, sure, but that still doesn't involve picking execution branches. I think you can actually have stuff like this make sense in dependent type systems, though.