I wrote a type checker: ARF. Is it novel?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

I wrote a type checker: ARF. Is it novel?

David Foster
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: I wrote a type checker: ARF. Is it novel?

Kim-Ee Yeoh
Administrator

On Mon, Sep 7, 2015 at 10:21 AM, David Foster <[hidden email]> wrote:
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: I wrote a type checker: ARF. Is it novel?

Andreas Abel
In reply to this post by David Foster
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

[hidden email]
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: I wrote a type checker: ARF. Is it novel?

David Foster
 > 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.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe