Is there a static checking tool for Julia?

It is annoying that a program only report errors (e.g., no method matching …) when it reach the point of calling, especially for some time-consuming programs.

Since in Julia, we can give detailed type information, I wonder if there is any static type checking tool for Julia, which utilizes the type information to discover any possible error before running?

for example, If I write a function

function foo(x::AbstractArray)
x+1
end

which should actually be x.+1 in the function’s content.

Can Julia discover this error (Julia alone or by using some external tool) in compiling stage?

Thanks

4 Likes

Yes,


but it has zero docs.


But note that julia is a dynamic language, so it is impossible to actually be 100% sure something is an error.

E.g. in your example i can have in my source code:

if rand() > 0.5
    @eval Base.:(+)(xs::AbstractArray, y::Int) = xs .+ y
end
5 Likes

An alternative solution is some unit testing (for building blocks, or the whole problem with a low-dimensional parametrization). Eg for a project I am working on now, the estimation with a 20^3 grid takes about 3 hours on the big server, but the “toy” parametrization 2^2 takes a few seconds on a laptop, so it goes in the unit tests.

5 Likes

Both, one wants both.
And defensive programming (the use of @assert)

4 Likes

The more complex Julia systems I build, the less of a fan I am of overly defensive programming (except when working with external state, eg the network or a file system). I find that relying on dynamic (in practice, AOT for undefined methods) failure (“duck typing”) is sufficient, and ex post it always turns out that I always over-constrain with assertions.

The exceptions are checking values (as opposed to types), eg verifying that a matrix is PSD when required. But this is usually not something amenable to static analysis, and also it prompts me to redesign the API occasionally (eg accept Cholesky factors as the entry point, which are is trivial to check, and make other methods wrap this and fail there).

1 Like

Indeed values, not types.

I am not saying put in type constraints you are not going to be checking.
I am big against that.

but a few @assert length(a) == length(b) can be helpful

1 Like

I agree with you about this, but nevertheless I find that Julia frequently allows me to design code in a way that these are not needed. Eg broadcasting and linear algebra operations will fail with a dimension mismatch, so if any of those are used it should be fine. I, of course, set up CI tests for catching these errors.

I am not saying that @assert should not be used, on the contrary, just that they are needed less in Julia than some other languages I have used. I find the API carefully engineered for this, eagerly throwing an error instead of doing something clever. Cf R’s

> 1:5 + 1:2
[1] 2 4 4 6 6

which now throws a warning but that is easy to overlook.

1 Like

Any thoughts about using JuliaLang/PackageCompiler.jl as a substitute for a static type checker like google/pytype? I’m currently experimenting with this approach and am interested in hearing other perspectives/experiences. My use case is setting up data pipelines.

But PackageCompiler doesn’t do any static type checking at all, so how are they comparable?

I am really looking foward to time when there will be static analyzer of Julia.
I understand that with metaprogramming and modifications of AST it may be really difficult to infer the type correctly, but I think just the fact that Julia is dynamic language is not a no-go for static analyzers.

For example, for PHP, which is a profoundly dynamic language there now exists https://github.com/phpstan/phpstan which is able to deal with the dynamics using Union and Intersection types and type inference on them.
And of course you can write

if rand() > 0.5
    @eval Base.:(+)(xs::AbstractArray, y::Int) = xs .+ y
end

and argue that static analyzer would not be able to deal with it, but in reality, how often you use randomly, or generally externally conditioned declaration of functions in such manner that you can not tell by static analysis how it will go?

Of course for dynamic language there will be something you need to give up when wanting static analysis, but I think people who want static analysis already try to write code that can be analysed and will aim for deterministic declaration of functions.

6 Likes
1 Like