[Haskell-cafe] I wrote a type checker: ARF. Is it novel?

David Foster davidfstr at gmail.com
Wed Sep 9 03:15:50 UTC 2015


 > 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.


More information about the Haskell-Cafe mailing list