[TYPES] RFC: ARF - An interprocedural flow-based type checker

[David Foster]

I've written a small untyped language calculus (ARF) and an 
interprocedural flow-based type checker to explore techniques for 
efficiently inferring all types in the presence of recursive function 
calls, with no prior type declarations or annotations required in the 
original program.

* https://github.com/davidfstr/arf#assign-recurse-flow-arf

The type system I have is a flow-based type system, similar to that used 
by David Pearce's Whiley language[^1]. I have extended his approach with 
interprocedural analysis and full inference for all types, since I 
didn't want to require the programmer to insert any annotations in the 
original source code, which would be required by Pearce's original 
formulation.

The reason I developed ARF was to learn type checking techniques for my 
ultimate application: writing an optional static type checker for 
Python[^2] that can be superimposed over Python's runtime type system, 
which is more similar in flavor to flow-based type systems than other 
kinds of type systems such as Hindley-Milner. However it occurs to me 
that the ARF calculus and type checker may be interesting in its own right.

In particular ARF has very good type checking performance: O(m^2) time 
in the worst case and O(m) time in the average case, where m is the 
number of functions in the program. (These bounds are derived from 
informal reasoning and empirical timings from ARF's automated test suite.)

On the other hand, I may have just reinvented a type system that already 
exists somewhere in the academic literature, since I am not familiar 
enough with type-related terminology to effectively search the literature.

So I have two main questions for this list:

(1) Is it likely that the ARF calculus or type checking algorithm is 
novel in one or more respects, based on my descriptions of its 
properties and performance?

(2) Are there other related calculi or type checking algorithms from the 
literature?

Thank you for taking the time to read this.

-- 
David Foster
http://dafoster.net/about/

[^1]: David J Pearce. "Calculus for Constraint-Based Flow Typing". June 
2012.
[^2]: David L Foster. "Plint: An optional static type checker for 
Python". In development. <https://github.com/davidfstr/plint>