Just-In-Time Static Type Checking for Dynamic Languages
arxiv.org
arxiv.org
CL-USER> (defun foo (x) (compile () `(lambda (u) (aref ,x u))))
FOO
CL-USER> (foo #(2 3 2))
#<FUNCTION (LAMBDA (U)) {100B3C610B}>
NIL
NIL
CL-USER> (funcall * 0)
2
CL-USER> (foo 332)
; in: LAMBDA (U)
; (AREF 332 U)
;
; note: deleting unreachable code
;
; caught WARNING:
; Constant 332 conflicts with its asserted type ARRAY.
; See also:
; The SBCL Manual, Node "Handling of Types"
;
; compilation unit finished
; caught 1 WARNING condition
; printed 1 note
#<FUNCTION (LAMBDA (U)) {100B41E16B}>
T
T
(defun foo (x) (compile ()
`(lambda (u)
(print "Executed")
(aref ,x u))))
(foo 0)
Nowadays that kind of efficiency isn't as big of a deal as it used to be and people tend to go more towards the angle of using the type system for error detection but I still can't shake that feeling that CL's type system feels a bit off when you compare it to other modern type systems.
(this is no excuse to not at least cite Common LISP though)
Getting errors is the same if at compile-time or in the test-suite or at the customer, though having them at compile-time is of course preferred. In LISP you have all 3 cases. In static languages only the first.
These guys here solve their type-checking performance problem by deferring the check to dynamic code. Checks are expensive if your type checking code is slow, or the source code is a dynamic mess. We are talking about ruby on rails here, which is the biggest dynamic mess one can think of. It's the similar problem the JIT guys have, deferring compilation to only actually invoked code and skipping dead branches.
See 'Types in Python' from the manual:
https://common-lisp.net/project/cmucl/doc/cmu-user/compiler....
A variant of that compiler is used in the now popular SBCL implementation:
main() {
foo();
}
foo() {
if (false) {
int i = "not an int";
}
}
bar() {
int j = "not an int";
}
It gives a some of the benefits of static typing: it reports errors in code paths not hit through imperative branching. But it doesn't give all of it since it doesn't report errors in uncalled functions.
However, what it gives you in return is the ability to handle functions that don't even exist at program startup and are instead defined at runtime later in the program's execution through metaprogramming.
When?
>However, what it gives you in return is the ability to handle functions that don't even exist at program startup and are instead defined at runtime later in the program's execution through metaprogramming.
Those are already dynamically "type checked", how is this adding anything?
It would report the error in foo() when foo() is invoked, even though the code path containing the error is never executed.
> Those are already dynamically "type checked", how is this adding anything?
Only code paths that actually get executed are dynamically checked. This checks all code paths in the method.
That's "dynamic typing".
>Only code paths that actually get executed are dynamically checked. This checks all code paths in the method.
Ok, so it is extended dynamic typing. Why on earth is it being described as having anything to do with static typing?
In particular, the code that was generated won't get executed if it can be proved beforehand that there is a type error.
I agree that in effect you won't get an error message until execution, but that does not mean that this is dynamic typing. Execution time and compile time are generally interleaved with metaprogramming so it can make sense to consider static-analysis for code at runtime.
What I found strange is the fact that it happens "Just-In-Time", which for me means at the last possible moment. This is counter-intuitive with what static typing aims to do. I would prefer "ASAP static-typing" (the code could be analyzed long before it is run).
That's why I still find the COMPILE approach of Lisp better, since we have precise control over when analysis is done.
Two things come to mind when considering this approach:
1. How does it handle the type signatures changing as the code is modified? Either it must detect when the code is modified and invalidate its saved signatures for that (although dynamic metaprogramming would make that hard), or you'll just have to live with static type-checking temporarily failing until you've run the program again to let it gather a new type signature.
2. This can only be accurate if you've actually tested all of your code paths, because any code path you don't test may call some method using a type signature that Hummingbird hasn't seen before. Granted, the scripting language community already focuses heavily on 100% code coverage (though 100% code coverage doesn't necessarily mean all the code paths have been tested), but it still seems like an important limitation to be aware of.
2. I think you're right.
"In Hummingbird, user-provided type annotations actually execute at run-time, adding types to an environment that is maintained during execution. As metaprogramming code creates new methods, it, too, executes type annotations to assign types to dynamically created methods. Then whenever a method m is called, Hummingbird statically type checks m’s body in the current dynamic type environment. More precisely, Hummingbird checks that m calls methods at their types as annotated, and that m itself matches its annotated type. Moreover, Hummingbird caches the type check so that it need not recheck m at the next call unless the dynamic type environment has changed in a way that affects m."
Personally, I think they're pushing the bounds of what "statically" means, but hey, they do say it's "just-in-time static". It does indeed do the checking before executing the function, it just happens to be immediately before executing the function. A paragraph later:
"To ensure our approach to type checking is correct, we formalize Hummingbird using a core, Ruby-like language in which method creation and method type annotation can occur at arbitrary points during execution. We provide a flowsensitive type checking system and a dynamic semantics that invokes the type system at method entry, caching the resulting typing proof. Portions of the cache may be invalidated as new methods are defined or type annotations are changed. We prove soundness for our type system."
Based on how their approach works, I don't think Point 2 stands.
Being able to significantly optimize type-checking for scripting languages like this to the point where you can actually run this in production seems quite valuable. But calling it "static type-checking" is simply wrong. Granted, they're calling it "just-in-time static", but that phrase is contradictory, it would be like saying "dynamic static type checking".
1. No compile-time type checking.
2. No autocomplete / intellisense in IDEs (you can try but it's never very good).
There are a lot of rudimentary "caveman completion" packages available for Ruby coding, but nobody has ever written a good "intellisense" feature for Ruby, where "good" means something on the level of, say, Xcode's "CodeSense" auto-completion for Objective-C or Swift, or JetBrains IDEA's support for Java.
I work in Xcode a lot, but I also maintain a couple Rails apps at work. A few times a year, I get so aggravated I spend an afternoon googling the state of the art in code completion for Ruby, and trying out various editors and IDEs.
JetBrains RubyMine is consistently the best, but it is far, far inferior to Xcode in this regard. It suggests methods but not the one I am looking for, or it suggests inappropriate methods that would cause an error, etc. It can't always jump to the definition of something, or tell me all the places the method I am currently editing is called from.
Xcode has a lot of things I could complain about, but the code completion, finding caller/callees, jump to definition/counterpart... all that stuff is incomparably better than it is for Ruby in any editor I have ever seen.
And of course it is — it is incredibly hard and complicated to do a complete or even mostly-complete job of it with Ruby code. There are just too many ways to metaprogram and too little information available to the editor to make it a straightforward task.
Strange, that's my objection to type declarations.
Is objectively less readable than
def marketDataService = new Factory<MarketDataService<Stock>>()
And even the latter is not the best.
def MyClass(marketDataService){
this.marketDataService = marketDataService
It's imho the most readable. If the name is self describing and there are unit tests that prove that I'm receiving the correct type I cannot care less about the type itself.
type expression =
| Number of float
| Add of expression * expression
| Subtract of expression * expression
| Multiply of expression * expression
| Divide of expression * expression
let rec eval expr =
match expr with
| Number n -> n
| Add (expr1, expr2) -> (eval expr1) +. (eval expr2)
| Subtract (expr1, expr2) -> (eval expr1) -. (eval expr2)
| Multiply (expr1, expr2) -> (eval expr1) *. (eval expr2)
| Divide (expr1, expr2) -> (eval expr1) /. (eval expr2)
janvitek.github.io/events/PBD13/slides/JeffFoster.pdf
They apparently changed their focus to gathering type information at runtime and using it to do interesting stuff, like this recent Hummingbird research.
By the way, I think it might be possible to implement autocompletion based on that runtime information they collect.