4 ms·

Well, sure, but the over-approximation is surprising given that false is constant and "if" is supposedly a well-known construct.

by junke 11y ago

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.
- junke 11y ago
  I think I can understand if Scala does not want to consider this kind of constant folding: after all, in most code you are supposed to have the same type on the "then" and "else" branch (in OCaml for example you don't have the possibility, as far as I know, to reproduce this case). I was surprised because I though it is quite a standard analysis in compilers nowadays. I had in mind SBCL precise type-checking (Common Lisp). Consider for example: (describe (lambda (x) (if nil x nil))) #<FUNCTION (LAMBDA (X)) {1005F6E9FB}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES NULL &OPTIONAL)) The derived type is NULL (which contains only NIL). And, more importantly, the compiler signals the presence of dead code, which is helpful for finding typos. It can handle more complex situations where the mistake is not obvious. The type system supports interval types like "(integer low high)": (describe (lambda (x) (if x 3 2))) #<FUNCTION (LAMBDA (X)) {100613759B}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (INTEGER 2 3) &OPTIONAL)) As well as set operations on types: (describe (lambda (x) (if x 2 4))) #<FUNCTION (LAMBDA (X)) {10062F5C8B}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (OR (INTEGER 2 2) (INTEGER 4 4)) &OPTIONAL)) So it is definitely doable, and even though it is still limited, it is less limited and quite useful.
  - tel 11y ago
    I'm not too familiar with SBCL but I highly doubt that those are static types. This sort of information is pretty ascertainable if you really want it, but it's going to be rough going doing non-runtime checking over types this rich.
    - junke 11y ago
      There are declared types and derived types, which are obtained by type inference and propagation. As much as possible, those types are used by the compiler, at compile-time, to signal type errors that are bound to happen at runtime, given the known types. But the code is robust and you can give a string to a function that is declared to accept a number (e.g. from the REPL): your program won't crash, because types are checked at runtime too (you have an exception). So, with default safety and speed optimization levels, adding type declarations will actually add runtime checks. But if you say "trust me, this will be a fixnum, produce some efficient code", then the type discrimination that would happen at runtime is bypassed and you directly emit the opcodes related to your type and this is how you optimize your code. For example, requesting a high-level of speed and low safety/debug will report a lot of optimization notes from SBCL, like: "forced to do GENERIC-+ instead of FIXNUM-+ because of type uncertainty". http://www.lispforum.com/viewtopic.php?f=2&t=191 http://www.lispforum.com/viewtopic.php?f=2&t=191 http://www.xach.com/sbcl/doc/x282.html http://www.xach.com/sbcl/doc/x282.html http://www.pvk.ca/Blog/2013/11/22/the-weaknesses-of-sbcls-type-propagation/ http://www.pvk.ca/Blog/2013/11/22/the-weaknesses-of-sbcls-ty...

Well, sure, but the over-approximation is surprising given that false is constant and "if" is supposedly a well-known construct.

by 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.

junke 11y ago
I think I can understand if Scala does not want to consider this kind of constant folding: after all, in most code you are supposed to have the same type on the "then" and "else" branch (in OCaml for example you don't have the possibility, as far as I know, to reproduce this case). I was surprised because I though it is quite a standard analysis in compilers nowadays. I had in mind SBCL precise type-checking (Common Lisp). Consider for example: (describe (lambda (x) (if nil x nil))) #<FUNCTION (LAMBDA (X)) {1005F6E9FB}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES NULL &OPTIONAL)) The derived type is NULL (which contains only NIL). And, more importantly, the compiler signals the presence of dead code, which is helpful for finding typos. It can handle more complex situations where the mistake is not obvious. The type system supports interval types like "(integer low high)": (describe (lambda (x) (if x 3 2))) #<FUNCTION (LAMBDA (X)) {100613759B}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (INTEGER 2 3) &OPTIONAL)) As well as set operations on types: (describe (lambda (x) (if x 2 4))) #<FUNCTION (LAMBDA (X)) {10062F5C8B}> [compiled function] Lambda-list: (X) Derived type: (FUNCTION (T) (VALUES (OR (INTEGER 2 2) (INTEGER 4 4)) &OPTIONAL)) So it is definitely doable, and even though it is still limited, it is less limited and quite useful.
- tel 11y ago
  I'm not too familiar with SBCL but I highly doubt that those are static types. This sort of information is pretty ascertainable if you really want it, but it's going to be rough going doing non-runtime checking over types this rich.
  - junke 11y ago
    There are declared types and derived types, which are obtained by type inference and propagation. As much as possible, those types are used by the compiler, at compile-time, to signal type errors that are bound to happen at runtime, given the known types. But the code is robust and you can give a string to a function that is declared to accept a number (e.g. from the REPL): your program won't crash, because types are checked at runtime too (you have an exception). So, with default safety and speed optimization levels, adding type declarations will actually add runtime checks. But if you say "trust me, this will be a fixnum, produce some efficient code", then the type discrimination that would happen at runtime is bypassed and you directly emit the opcodes related to your type and this is how you optimize your code. For example, requesting a high-level of speed and low safety/debug will report a lot of optimization notes from SBCL, like: "forced to do GENERIC-+ instead of FIXNUM-+ because of type uncertainty". http://www.lispforum.com/viewtopic.php?f=2&t=191 http://www.lispforum.com/viewtopic.php?f=2&t=191 http://www.xach.com/sbcl/doc/x282.html http://www.xach.com/sbcl/doc/x282.html http://www.pvk.ca/Blog/2013/11/22/the-weaknesses-of-sbcls-type-propagation/ http://www.pvk.ca/Blog/2013/11/22/the-weaknesses-of-sbcls-ty...