I’d add here that the features that have been the primary focus is development (namely caching code, main entry point, decoupling stdlib, etc) are all prereq to small binaries.
14 Likes
@Benny I know complaining and demanding doesn’t spark developer resources but maybe it bumps this item in the priority list. Thanks for all the links! The status of StaticCompiler makes this look quite a challenge I must say… I thought it’s basically just ditching eval, some tree shaking and Bob’s your uncle!
@Imiq after tim.holy kinda (rightfully) said “If you want this but can’t help then maybe spend some money on it” I felt like nobody wanted to say “I want it but I can’t help but I also don’t want to spend money.” which I meant by awkward silence. I didn’t mean nothing is moving forward.
@AMJ high five then! 
Also thanks for the links!
@aplavin sorry, was maybe not constructive to mention Python. We use C++ if we have to (closed source, stand alone, fast, whatever) and Python otherwise simply because everyone knows it and it’s used everywhere. From my little experience I consider Julia superior to Python in every way.
@Imiq the clear advantage that Python has over Julia is that it occupies the nice-to-use-cant-produce-small-binaries-scripting-language seat and everybody uses it because everybody else uses it… But the nice-to-use-scientific-compiled-language seat is still vacant if you ask me.
I’m happy to see some movement here! I keep my hopes up, maybe at some point I can help.
4 Likes
Thanks for sharing your experience, it adds context and nuance to the discussion.
Given Julia’s current architecture, you can get small binaries if and only if your code is type stable - that is, if your code contains no dynamic dispatch. Otherwise either some methods are missing (so it’s compiled incorrectly) or you have to include all the source codes and LLVM in your binary product, which renders small binaries impossible.
The real problem is that most of Julia codes are not fully type stable - maybe 99% part of the codes are stable but 1% is unstable. This is either unintensional (like mix of Float and Int) or intensional (to reduce JIT latency), but we need to identify these 1% codes and manually fix them, otherwise our static compiler simply stucks. Unfortunately, for large codebases searching for these dynamic codes are painful if we use @code_xxx to test every possible method combination.
Therefore, to produce small binaries, people have to change how they program in Julia in a fundamental way - we need to use static type checker to ensure the absent of dynamic dispatch (which is not easy, as type stability is not well defined and there’s no simply rule for us to decide what is well-typed program). What’s more, libraries that use dynamic dispatch can be used by static libraries. Is this acceptable for most of Julian?
So it’s more of an aesthetic problem instead of a technical problem.
3 Likes
This paper has formalized and quantified stability and groundedness:
• type stability is when a function’s return type depends only on its argument types, and
• type groundedness is when every variable’s type depends only on the argument types
12 Likes
Since you talk about this paper and it’s referenced several times in discord/stack, here is my opinion:
-
Even using such a broad and relexed definition of type stability, many popular Julia packages still have a high portion of unstable/ungrounded codes. This only makes the aforementioned problem look worse.
-
There are many different ways to model a problem and each of them can yield a different result. This paper presents one but it doesn’t mean everyone will agree on that. But we have to agree on one of the model (which one, though?).
-
This paper’s formalization doesn’t quite match the underlying static compilation model. Julia’s compiler can give up on complicated path-dependent types or big unions and degrade into Any and dynamic dispatch, even if it’s type stable in this paper’s sense. What’s important here is a guarantee of static compilation: if I do X/follow rule X, then my codes can be compiled statically.
-
It’s too hard for programmers and implementers to reason about this model. Type checking becomes extremely hard.
The goal of program analysis and formal methods (used in this paper) are completely different from type systems. The former can use some advanced tools like model checking and no need to be 100% precise, while the latter are generally cheap and straightforward. You can define like “type stability” like in this paper but such definition takes too much time to verify. Also if there’s (type stability) error, there’s no easy way for programmers to dignose and fix it.
Therefore any practical implementation will deviate from the model in this paper. Now the problem stands still : which model of type stability should I choose?
5 Likes
That’s not generally true. You can have type systems that require model checking in their subtyping relationship. Languages utilizing such type systems are even more niche than Julia though.
The model in the paper is of course simplest for proving things about the type system, and implementing it “straight from that” would of course be bad. Still, the definitions they give are useful and lead to exactly the kind of output JET.jl provides you.
3 Likes
This is, what I am waiting for (for some specific tasks/ideas), but, AFAIK, it is yet not possible to do it. If I have NOW type stable code, like a minimal “Hello World”, I have yet no tool to create a minimal binary. It has to come in some near or middle future.
Am I wrong? Did I missed something while waiting?
1 Like
I think you are referring those refinement type systems, either Liquid Haskell or RustHorn. Unfortunately they are simply program analysis in disguise and use of type systems is not essential in this case. They simply use type systems to generate Horn/SAT clauses (I would rather call them syntax-guided program analysis). One evidence is that types in such type system have no canonical form and you simply accumulate every predicative on every path and then your types blow up along the way.
Since you mention it, the problem faced by refinement type systems is almost the same as Julia. Refinement type systems can’t handle function abstraction and if-then-else gracefully.
Consider the return type of if-then-else:
if (cond) (P x) (Q x). Depending on the condition cond, we have P x or Q x. Then either:
- For classic type theorist, this is illegal because return type is different on each branch. (= no union type)
- For subtyping type theorist, we join two predicates and return
(P \/ Q) x. This is path-independent program analysis. Too imprecise (type calculation is disallowed) - The most precise one
(cond -> P x) \/ (not cond -> Q x)is path-dependent program analysis. Then you have path explosion.
To prove any non-trival useful property, we have to choose option 3. But for large program native implementation sucks. Too many paths. We need to omit path condition somehow, then it falls in the scope in program analysis. Then what’s purpose of refinement type? Why not use powerful program analysis from the start?
Like I have mentioned before, there are many useful definitions. This paper just provides one of them and I don’t agree with that, because it allows too many path-dependent types and ill-structured programs, which makes type reasoning hard (even worse than C++'s templates). Also, Julia’s builtin compiler doesn’t implement that model, whose implementation changes over time.
Program analysis is generally more “automatic” than type systems. But the result is hard to read due to the fundamental limit of any bidirectional type inference algorithm (or “subtyping with model checking”). Also, abstract interpretation interacts really bad with subtyping and recursive functions. You need to iterate multiple times to converage and if you make some type errors, you get a lot of Bottom. You need to convince the general public that the model of JET.jl is good enough for developping static programs, not me.
2 Likes
I can only say that there’s no essential technical difficulty in current Julia’s architecture. But I don’t know whether it will be implemented in some near or middle future.
Still, even if your code is type stable, Julia has a small 10~20MB runtime for gc/array/multi-threading, so your small binaries won’t be less than this size. I don’t think size like 1MB or 2MB is possible.
Honestly speaking if you believe this is a real concern then you should consider switching to C++/Fortran instead of waiting indefinitely. You have seen in this thread that core developers are in shortage. Also, their supports for incremental compilation and IDE are more mature.
5 Likes
I don’t think that’s correct: it’s conflating missing methods and dynamic dispatch, but the LLVM kitchen sink is only required in case of missing methods.
Take this example:
v = Union{Int,String}[1, 2, "a"]
x = first(shuffle(v))
do_something(x)
It’s type unstable since x can be an Int or a String. But the compiler could easily include the two corresponding specializations of do_something in the binary. The runtime would need to include an implementation of dynamic dispatch, but that’s a small thing, much smaller than the LLVM and source code.
Why not? Many languages have a runtime that includes these things in much less than 10-20MB.
My hunch is that you’re being overly pessimistic about this. I think there’s a ton of situations where you have numerical code that’s working on well defined types or a small number of possible types that could be compiled to smallish libraries/binaries like this. Once we have the tooling to make the simpler cases easy, I expect there will be more and more interest and efforts to increase the range of supported cases and address issues in common packages. And I also expect a synergy of efforts between work on small binaries and work on TTFX.
4 Likes
For reference here is a “hello world” size benchmark:
3 Likes
julia> using StaticCompiler, StaticTools
julia> hello_world(args...) = println(c"Hello, world!");
julia> compile_executable(hello_world, (Int, Ptr{Ptr{UInt8}}), "./");
shell> ./hello_world
Hello, world !
shell> ls -alh hello_world
-rwxr-xr-x 1 mason mason 16K Oct 18 19:52 hello_world
16kb is pretty good*!
*terms and conditions apply, speak to a clinical psychologist to assess if StaticCompiler.jl is right for you
20 Likes
I remember being told StaticCompiler is probably not “the path forward”, so small demons like these while are indeed cool & cute at the same time, probably shouldn’t be extrapolated to recommendation for a company product 
4 Likes
Depends on what one means by that. The package itself is definitely not going to be the canonical go-to package for AOT compilation. But the actual mechanisms and ideas behind it are applicable for ‘real deal’ future applications.
StaticCompiler is a proof of concept
6 Likes
right, what I mean is if it works for the things at hand it’s great. But I don’t want to show these examples and the AOT we did for benchmarks to people and say “just try to extrapolate this pattern to your 10k lines Julia project and jUsT try to make it compile”
2 Likes
That’s why I said
You’d have to be insane to try and use it on a 10k loc professional project. It’s relevant to the roadmap though.
It seems I have to give it a try, should I? You two are sending mixed signals to me 
…I know exactly what I’m saying becasue I have managed to implement such a prototype in LLVM. The case you make contains no dynamic dispatch (at runtime) because of union splitting. I think it’s safe to say that “No dynamic dispatch (at runtime) == No missing method”.
So you admit that there’s a mismatch between your definition of type stability and the static compilation model? We now have multiple non-equivalent concepts. That’s why I ask for an agreement on the model we should use. What’s the exact standard? Also, it’s easy because you only consider small examples. Large examples never work like this. Union splitting stucks quite quickly because compiler stops to split when union is “large” → but 4 is an arbitrarily chosen number to ensure termination.
But how do you know, Julia’s user groups are willing to write their codes in this way ,or whether most of Julia’s current codebases satisfy this criteria?
Such situations are easy to image because there are a lot of static numerical Fortran/C codes, and in theory any direct translation of such codes into Julia is a valid target for static compilation. I will call this “C style static compilation model”. But this is more non-trivial than you may think. Like I said, it’s an aesthetic problem.
Specifically:
- (For new codes) Julia currently has no other (runtime) ad-hoc polymorphism, except for dynamic dispatch. Even if only 0.1% codes use this feature then your codes fail to compile statically. And unlike C, Julia has no function pointers and it can’t emulate dispatch table. What’s the alternative? (FunctionWrapper.jl ?)
- (For old codes) Some libraries are written without the monitor of type checker (e.g. JET.jl) and they are of bad shape. A lot of effects are needed to correct these type errors before they can be compiled. Generic types are not fully parameterized. Float and int are mixed accidentally (then 50 lines of Julia codes blow up into 3000 lines of IR). Another example are the matrix factorization libraries. People forget to wrap their matrix with
Symmetricandeigen.
Introducing static compilation will fundamentally change how Julia works and create an internal two-language problem. I am perfectly fine with writing my code in C-style. That’s what I have done in my type checker (I am impatient so I implement my own) GitHub - ChenNingCong/SimpleTypeChecker: A simple static type checker that enforces C-style programming in Julia
But what about other users? JET.jl still says it’s an experimental analyzer and only Julia experts know how to use all these things (XXXCompiler.jl, XXXChecker.jl) . Unless you can convince most people and formally include all these tools into the core language, they are still just proof-of-concept, no matter how clever they are.
1 Like
sorry, that wasn’t clear from what you said, maybe my English is bad 
. I think many reading this thread are genuinely evaluating Julia for binary production deployment from a new user perspective, we should err on the being clear and explicit side.
2 Likes