Relational typing example

[brandonwillard]

This PR introduces a simple relational typing example for Python AST.

This implementation is based on Racket examples provided by @jasonhemann.

• [ ] Add all function body statements to the typing context
• [ ] Equate ast.args with ast.Name (i.e. "symbols")
• [ ] Type elements of Sequences
• [ ] Support ast.If
• [ ] Support ast.Assign
• [ ] Support ast.Expr
• [ ] Support ast.Call
• [ ] Support operator.getitem

Example

Here's a very simple example that infers the type of a def statement:

import ast
from textwrap import dedent
# load the examples/type_inference.py module...

# Create a test statement
expr = ast.parse(dedent(
    """

    def func(y):
        return 1 + 1.0

    """), mode="single").body[0]

# Create a logic variable for the type of the statement
type_var = var()

# Run the `turnstileo` relation and return all valid values for `type_var`
res = run(
    0,
    type_var,
    turnstileo([], [], expr, type_var),
)

res[0]
# typing.Callable[[~tx_2408], float]

The goal has inferred that the statement is a Callable with an unground logic variable (i.e. ~tx_2408) as the type of its only argument (this could be interpreted as typing.Any) and a float-typed return value that was derived from the type promotion in the expression 1 + 1.0.

[majidaldo]

This is great! I've been looking at the connections between ast and sexprs. Would using Hy have any advantage if we can translate between code and sexprs? Also is this ready to be integrated?

This makes me think if we can build parsers as well. Generating a parser given a spec would be insane.

[brandonwillard]

Would using Hy have any advantage if we can translate between code and sexprs?

Hy would be convenient for a number of reasons (e.g. manipulating AST), but a lot of the same work would be involved regardless. Take a look at hydiomatic and my article about a generalized Hy repr for some very related examples.

Also is this ready to be integrated?

I would like to get some coverage for the basic control flow statements (e.g. if, for, etc.) and variadic function calls before considering this example finished.

This makes me think if we can build parsers as well. Generating a parser given a spec would be insane.

Yes, that can be—and is effectively being—done.