I wrote a type checker: ARF. Is it novel?
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. The type checking algorithm I've come up with appears not only to work but also to have good 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. So the question I'd like to pose to any type system buffs on this list is: (1) Is such an interprocedural flow-based type checking algorithm with that kind of performance likely to be novel? And if you have some interest and time to actually review the strategy and/or implementation of the algorithm at https://github.com/davidfstr/arf#assign-recurse-flow-arf, I'd love to know: (2) Are there similar type checking algorithms that already exist in the academic literature? I'm posting these questions here because I'm guessing that a number of folk that work with type systems and type checkers are likely to be subscribed to this list. If there are other more-appropriate venues, I'd love to hear about about them as well. -- David Foster
On Mon, Sep 7, 2015 at 10:21 AM, David Foster
I'm posting these questions here because I'm guessing that a number of folk that work with type systems and type checkers are likely to be subscribed to this list. If there are other more-appropriate venues, I'd love to hear about about them as well.
There's also the TYPES mailing list, of which a search should locate as top result. -- Kim-Ee
Why not use one of the 40-year old type checking algorithms? https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system What type do you infer for def id(n): return n ? On 07.09.2015 05:21, David Foster wrote:
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.
The type checking algorithm I've come up with appears not only to work but also to have good 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.
So the question I'd like to pose to any type system buffs on this list is: (1) Is such an interprocedural flow-based type checking algorithm with that kind of performance likely to be novel?
And if you have some interest and time to actually review the strategy and/or implementation of the algorithm at https://github.com/davidfstr/arf#assign-recurse-flow-arf, I'd love to know: (2) Are there similar type checking algorithms that already exist in the academic literature?
I'm posting these questions here because I'm guessing that a number of folk that work with type systems and type checkers are likely to be subscribed to this list. If there are other more-appropriate venues, I'd love to hear about about them as well.
-- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/
On 07.09.2015 05:21, David Foster wrote:
I've written a small untyped language calculus (ARF) [...]
On 9/8/15, 5:42 AM, Andreas Abel wrote:> Why not use one of the 40-year old type checking algorithms?
https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
I was aware of the Hindley-Milner type system but judged it to not be an appropriate fit for my ultimate application, namely superimposing a static type system on top of Python's runtime type system in order to give it optional static typing. The type system I have is a flow-based type system, similar to that used by David Pearce's Whiley language. I have extended his approach to interprocedural analysis, 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.
What type do you infer for
def id(n): return n
If the program calls id() with (n = int) in at least one place, with (n = bool) in at least one place, and with no other argument types elsewhere, the type of id() will be inferred as: * id(int) -> int * id(bool) -> bool You'll notice no parameterized type was introduced. The ARF type checker deals with simple non-parameterized types only.
participants (3)
-
Andreas Abel -
David Foster -
Kim-Ee Yeoh