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

[Gabriel Scherer]

The assumption made in your note [^max-refinements-in-loop], namely
that there is a bounded number of types refining each other and that
you can thus always compute the fixpoint in finite time, will not hold
in richer type systems, if you have higher-order functions for example
(consider a recursive function that consumes infinitely many
arguments). Ultimately you may run into the well-known problem that
polymorphic recursion is not inferrable in absence of type
annotations.

I was not entirely satisfied with the complexity argument you provide.
You describe several different corner cases and their complexity
analysis, and assume that any program (can be decomposed in
subprograms that) will behave in a way similar to one of these corner
cases -- that they are effectively the worst cases in a formal sense.
However, this assumption that the corner cases cover all possible
programs is not clear to me.

I am far from an expert on this corner of the literature, but I think
you may be interested in the work on Flow Analysis that happened
approximately at the same time as the detailed study of polymorphic
recursion (in the nineties). In particular, the work of Christian
Mossin on flow analysis seems relevant. It was done in a typed setting
but, in "Higher-Order Value Flow Graphs" (1997) a dynamic type is
considered; it could be interesting to translate your language to his
system to compare your analyses.
(His formalism, in terms of a flow graph built out of programs, allows
for rigorous proofs of complexity in terms of the size characteristics
of the constructed graph.)

On Thu, Sep 10, 2015 at 6:53 AM, David Foster <davidfstr at gmail.com> wrote:
> [ 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>