[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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>
