A simple static type checker that enforces C-style programming in Julia

Overview

SimpleTypeChecker is an experimental Julia package designed to enforce C-style programming in Julia language. Note : it won't save you if your codes already contain a lot of messy dynamic dispatch. It's more appropriate for developing new codes from scratch. See demo below for an example usage.

Installation

pkg> add https://github.com/ChenNingCong/SimpleTypeChecker

Usage

ctx = SimpleTypeChecker.Inference.GlobalContext()
SimpleTypeChecker.API.addFile!(ctx, mod, filepath)
SimpleTypeChecker.API.runCheck!(ctx;checkSyntax=true)
SimpleTypeChecker.API.@nocheck fun
SimpleTypeChecker.API.check(ctx, f, tt)

SimpleTypeChecker provides several APIs to check all the functions in a file. To use this function, firstly import/include the module you want to check, then call ctx = SimpleTypeChecker.Inference.GlobalContext() to construct a context for type inference. Use SimpleTypeChecker.API.addFile!(ctx, mod, filepath) to add all the files you want to check into the context. Here mod is the module you just evaled and filepath is the filepath (absolute path) where the module is defined. Finally call runCheck! to check the context. By default we will check unsupported syntax. If you want to ignore unsupported sytnax error, use checkSyntax = false.

If you have a function that is highly dynamic or uses some features that SimpleTypeChecker doesn't support, and you are certain the function is type stable, then you can use SimpleTypeChecker.API.@nocheck fun to skip the checking of that particular function. If you don't want to import SimpleTypeChecker, then using any macro (@inline, @inbounds) is sufficient, because currently we skip checking of any macro.

Currently, only functions with concrete type annotation can be checked. If you want to check individual specializations like sum(x::AbstractArray) and println(io::IO, x), use SimpleTypeChecker.check(ctx, f, tt). SimpleTypeChecker.check accepts parameters like code_warntype and code_typed, SimpleTypeChecker.check(ctx, sin, (Float64,)). If you find this too complicated, then you can create a main function and put all the specializations in that main function. SimpleTypeChecker will recur into the subprocedure calls automatically.

Demo

  1. SimpleTypeChecker is checked against itself, the following code checks almost all the codes of SimpleTypeChecker (some codes interact with Julia's compiler so they simply can't be statically-typed)
import SimpleTypeChecker
# firstly we get the package directory of SimpleTypeChecker
const path = abspath(joinpath(splitdir(pathof(SimpleTypeChecker))[1], ".."))
ctx = SimpleTypeChecker.Inference.GlobalContext()
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.SyntaxAdaptor, joinpath(path, "src/adaptor/TreeQuery.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Inference, joinpath(path, "src/adaptor/InferenceDefinition.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Inference, joinpath(path, "src/adaptor/Inference.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Inference, joinpath(path, "src/adaptor/InferenceErrorUtility.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Inference, joinpath(path, "src/adaptor/InferenceError.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Inference, joinpath(path, "src/adaptor/ScopeChecking.jl"))
SimpleTypeChecker.API.addFile!(ctx, SimpleTypeChecker.Server, joinpath(path, "src/server/SimpleHTTPServer.jl"))
SimpleTypeChecker.API.runCheck!(ctx)
  1. You can check the test/case/case.jl of SimpleTypeChecker's test cases, which includes some common program errors.
import SimpleTypeChecker
# firstly we get the package directory of SimpleTypeChecker
const path = abspath(joinpath(splitdir(pathof(SimpleTypeChecker))[1], ".."))
const testpath = abspath(joinpath(path, "test/case/case.jl"))
include(testpath)
ctx = SimpleTypeChecker.Inference.GlobalContext()
SimpleTypeChecker.API.addFile!(ctx, CaseTest, joinpath(path, testpath))
SimpleTypeChecker.API.runCheck!(ctx)

For example, if you check test/case/case.jl, you will get a long list of error message:

────────────────────────────────────────────────────────────────
Checking MethodInstance for Main.CaseTest.f26()

/home/chenningcong/.julia/packages/SimpleTypeChecker/tu1RO/test/case/case.jl:225:11
 UndefinedError: variable y is potentially unitialized here
    y

────────────────────────────────────────────────────────────────
Checking MethodInstance for Main.CaseTest.f27()

/home/chenningcong/.julia/packages/SimpleTypeChecker/tu1RO/test/case/case.jl:235:15
 UndefinedError: variable z is potentially unitialized here
    z

────────────────────────────────────────────────────────────────
Checking MethodInstance for Main.CaseTest.f30()

/home/chenningcong/.julia/packages/SimpleTypeChecker/tu1RO/test/case/case.jl:267:13
 TypeError: 2-th paramter of type application (a.k.a parameterized type) is not a constant
    Vector{Int, x}

────────────────────────────────────────────────────────────────

Internal

The idea is simple : SimpleTypeChecker performs type inference on Julia's AST (instead of lowered IR) and also rely on Julia's type inferencer

  1. SimpleTypeChecker reads the method definitions from the file you provide, and use JuliaSyntax to parse the file and construct a loseless AST (a.k.a AST with precise location information)
  2. For each method AST f, SimpleTypeCheck walk through the AST and check common errors. If it encounters a function calls to another function g, then it calls Julia's builtin type inferencer to get the return type of g

Note : we need to rely on Julia's builtin type inferencer, because we don't have AST for every method definition (especially those in Base library). Also, inference for recursive function is generally undeciable, adding recursive check in SimpleTypeChecker will complicate a lot of thing.

Limitation

Currently there are many limitations, like we don't support destruct assignment in for-loop (for (x, v) in x). Some of them are temporal and will be removed in the future, but at least the following limitations are permanent. They are critial parts of SimpleTypeChecker's design and can't be simply removed by clever engineer efforts.

In summary, these limitations are the prices in exchange for a better error reporting.


Function calls with abstract parameters (including Union{...}, Any, Integer, where) are unconditionally disallowed, whether there is only one matching method, whether the function is a commonly used one (like ==(Any, Any)), etc.

Reason: Sometimes abstract calls are intended, like

struct A
val::Union{Int, Nothing}
end
# a.val isa Union, an abstract type
copy(a::A) = A(a.val)

So there is simply no way to tell whether an abstract call is intended or not. Then the only solution is to ban abstract calls everywhere.

Workaround: Wrap the abstract values in a struct. Only pass the wrapper and manipulate the wrapper with interface methods (In the future, SimpleTypeChecker may directly support MLStyle.jl's pattern matching and algebraic types, so we don't need to wrap and dewrap them manually).


Limited type calculations and constant propagation, no heap analysis, no complicated type narrowing (only a single isa)

Reason:

Such analyses require nontrivial bidirectional flow analysis. One immediate consequence of such complicated analyses is that it's hard to precisely locate where the error is. Codebases in Julia are generally loosely typed. If there is an error somewhere, the this error may gradually propagate to other codes. That's why it's painful to debug type instability, because you need to recurse into a long function chains and context to seek the real source of bug.

Workaround:

Do calculations in short unchecked functions


Unable to distinguish errors caused by :: and implicit convertion, like push!([1,2,3], "1").

Reason:

push!([1,2,3], "1") is a totally valid function call. Honestly speaking, should this be considered as compile time error at all?

Workaround: Almost impossible to workaround. Currently my thought:

  1. Use a whitelist. Only the functions in the whitelist can return Union{}, like error.
  2. Check functions recursively and only trust Julia's compiler when we don't have AST (this solve the problem if you have a return type assertion on a method, but the method is inferred as Union{})
  3. Manually provide interface definition for commonly used container in Base library. (Much like typeclass in Haskell, if type parameters don't satisfy the constraint, then immediately raise error)

Scope of variable in if-block and interpretation of local x::Int is vague.

Reason: Julia has no scoped if block, which raises some interesting problems of variable in if-block. Should the following case be treated as type instability?

function f(y::Bool)
    if y
        x = 1
        print(x)
    else
        x = 1.0
        print(x)
    end
end

If we perform basic-block specializations and view two x as individual unrelated copies of value 1 and 1.0, then this code is type stable. SimpleTypeChecker can actually detect it and allow it (as long as if x is not used in following branch), but I choose to ban this case. So automatically merge of different types are prohibited. This is to prevent the following case:

function f(y::Bool)
    if y
        x = 1
        println(x)
        # many more codes here...
    elseif somecond
        # ... 
    else
        # accidentally name a string as x
        x = "1"
    end
    # more code here...
    # abstract call !!!

    # error reports here, too late
    print(x)
end

What if I want to construct a Union type? then use a typed slot:

function f(y::Bool)
    local x::Union{Int, Nothing}
    if y
        x = 1
    else
        x = nothing
    end
end
You might also like...

Cookbook Method is the process of learning a programming language by building up a repository of small programs that implement specific programming concepts.

Cookbook Method is the process of learning a programming language by building up a repository of small programs that implement specific programming concepts.

CookBook - Hacktoberfest Find the book you want to read next! PRESENTED BY What is CookBook? A cookbook in the programming context is collection of ti

Nov 17, 2022

Jaksel Script, Programming language very modern and Indonesian style

Jaksel Script Jaksel Script is a new programming language, very modern, easy to learn, using Indonesia-slang language. No programming experience requi

Jan 3, 2023

💊 Event-driven DOM programming in a new style

Capsule v0.5.3 Event-driven DOM programming in a new style Features Supports event-driven style of frontend programming in a new way. Supports event d

Oct 1, 2022

Base62-token.js - Generate & Verify GitHub-style & npm-style Base62 Tokens

base62-token.js Generate & Verify GitHub-style & npm-style Secure Base62 Tokens Works in Vanilla JS (Browsers), Node.js, and Webpack. Online Demo See

Jun 11, 2022

Type predicate functions for checking if a value is of a specific type or asserting that it is.

As-Is Description As-Is contains two modules. Is - Type predicates for checking values are of certain types. As - Asserting values are of a certain ty

Feb 10, 2022

Combine type and value imports using Typescript 4.5 type modifier syntax

type-import-codemod Combines your type and value imports together into a single statement, using Typescript 4.5's type modifier syntax. Before: import

Sep 29, 2022

🧬 A type builder for pagination with prisma and type-graphql.

🧬 Prisma TypeGraphql Pagination Prisma TypeGraphql Pagination builds prisma pagination types for type-graphql. import { ... } from 'type-graphql'

Apr 21, 2022

🐬 A simplified implementation of TypeScript's type system written in TypeScript's type system

🐬 A simplified implementation of TypeScript's type system written in TypeScript's type system

🐬 HypeScript Introduction This is a simplified implementation of TypeScript's type system that's written in TypeScript's type annotations. This means

Dec 20, 2022

A transpiler from golang's type to typescript's type for collaboration between frontend & backend.

A transpiler from golang's type to typescript's type for collaboration between frontend & backend.

go2type go2type.vercel.app (backup site) A typescript transpiler that convert golang's type to typescript's type. Help front-end developer to work fas

Sep 26, 2022
Releases(v0.1.0-alpha)
Owner
null
A type programming language which compiles to and interops with type-level TypeScript

Prakaar Prakaar (hindi for "type") is a type programming language which compiles to and interops with type-level TypeScript. Prakaar itself is also a

Devansh Jethmalani 17 Sep 21, 2022
Lightweight, Portable, Flexible Distributed/Mobile Deep Learning with Dynamic, Mutation-aware Dataflow Dep Scheduler; for Python, R, Julia, Scala, Go, Javascript and more

Apache MXNet (incubating) for Deep Learning Apache MXNet is a deep learning framework designed for both efficiency and flexibility. It allows you to m

The Apache Software Foundation 20.2k Jan 5, 2023
EA Origin platform username checker

Origin EA Origin platform username checker. Instructions [?] Installation "npm i" [?] Fill in your Discord webhook details. "var webhookId = ``;" "va

yani 3 Sep 29, 2022
NodeJs, tron transaction checker

Tron node-Explorer Recommended requirements Node v14.17.5. npm 6.14.14 https://nodejs.org Development Install dependencies npm install Running applica

null 3 Aug 21, 2022
Babel-plugin-amd-checker - Module format checking plugin for Babel usable in both Node.js the web browser environments.

babel-plugin-amd-checker A Babel plugin to check the format of your modules when compiling your code using Babel. This plugin allows you to abort the

Ferdinand Prantl 1 Jan 6, 2022
this is a discord nitro generator and checker⚙ EZPZ

Language | EN Hello my dear friends ???? In this new project, I wrote a program to extract nitro discord code, which after extracting the code, verifi

Sobhan.SRZA 6 Sep 17, 2022
Gofiber with NextJS Static HTML is a small Go program to showcase for bundling a static HTML export of a Next.js app

Gofiber and NextJS Static HTML Gofiber with NextJS Static HTML is a small Go program to showcase for bundling a static HTML export of a Next.js app. R

Mai 1 Jan 22, 2022
A web component that allows you to run high level programming languages on your websites (static websites included!)

Code-Runner-Web-Component A web component that allows you to run high level programming languages on your website via the public Piston API Show your

Marketing Pipeline 28 Dec 16, 2022
When a person that doesn't know how to create a programming language tries to create a programming language

Kochanowski Online Spróbuj Kochanowskiego bez konfiguracji projektu! https://mmusielik.xyz/projects/kochanowski Instalacja Stwórz nowy projekt przez n

Maciej Musielik 18 Dec 4, 2022