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.