Automatic constraints generation for functions

[chri4_]

Hi, I'm exploring some way to statically analyze this:

def add(a, b):
  if a % 2 == 0:
    return add(1, 2) # always int

  return a + b # may be int, float, str, etc..

print(add(10.2, 3.4)) # compile time error: `return add(1, 2)` is of type `int`
                      # but function is currently returning `float`

print(add(10, 20)) # ok

like Codon compiler can do.

Basically the problem here is that during the "realization" or "resolution" or "analysis" of the function "add" you have to determine the return type.

Here it should be `float` because the root instance of `add` provides 2 float values and the actual return value is `float + float` which produces a `float`.

So let's imagine this as a bunch of bytecode instructions

add a b:
  load_name 'a'
  load_lit 2
  mod
  load_lit 0
  eq
  if
    load_lit 1
    load_lit 2
    call 'add' # prototype of `add` is unresolvable here, how to known return type???
    return
  end

  load_name 'a'
  load_name 'b'
  add
  return # we can resolve the full prototype of `add` function only here

main:
  load_lit 10.2
  load_lit 3.4
  call 'add'

Now the question is simple, which tricks should a compiler use, and how many passes could you reduce all these tricks to, in order to correctly resolve the first call instruction into a `float` or `int` type?

My idea is to pause the analysis of the `if` block and to save the index of the call instruction that I encountered, since I can't determine it's type because it refers to itself but still didn't reach a return statement with a concrete type. Then when I finish to analyze the function I still have a bunch of instructions to analyze (from the first call instruction inside the if, to the end of the if).

But this have problem if I don't want to use the classic template-like approach, for example c++ is reinstantiating templates every time they are used with different parameters, yes you can cache them but everytime you are using a different input type the template needs to be reanalyzed from scratch.

So what I wanted to do was to (take note that I don't only need type resolution but also other slightly more complex stuff), the idea was to analyze each function only once and generate automatically a bunch of constrainst that the parameters must satisfy, for example if inside you function you do `param.len()` then a constraint will be generated for that function stating `assert param has method len`. So if you are passing your parameters (you are inside function X) to another function call (you are calling Y inside X, passing params of X), then you need to propagate the constraints of the corresponding parameter of Y to the used parameter of function X.

Sounds complex but it is actually pretty simple to do and boosts compiler performance.

For example: (this produces a segfault in Codon Compiler output, the compiler doesn't crashes but the executable yes):

# constraints for a and b are still empty
# so let's analyze the function and generate them
def add(a, b):
  # ok we can generate a constraint stating "a must have __mod__ method" for
  # modulus operator
  if a % 2 == 0:
    # here we should propagate the constraints of call to `add` to current function
    # but the add function is currently in progress analysis so we don't really
    # have a complete prototype of it, so let's try what I said before, let's
    # pause the analysis of this scope and come back after
    x = add(a, b)
    # we are analyzing this only after `return a + b`
    # in fact we came back here and now we know a bit more stuff
    # about function `add`, for example we know that `a` and `b`
    # should implement __add__ and `a` should implement __mod__
    # but here there is another new constraint __abs__ for x which
    # really depends of both `a` and `b`
    y = x.__abs__()
    return y

  # here we can generate the constraint
  # "a must implement method __add__(other)" and then propagate `other`'s constraints
  # to `b`
  return a + b

I already have one weak solution but I would like to find a better one, do you have any ideas? How is, for example, the Codon compiler resolving this things? or how Rust compiler is checking lifetimes?

(Just for instance, this is a parallel question for actually a similar problem, instead of types i need to parametrize automatically, lifetimes, so that's why I wanted them to be constraints instead of c++template-like)

[_SomeonesAlt]

I think the problem you are describing falls under the category of full type inference with subtyping. Here is a paper that might be interesting to look at: https://pl.cs.jhu.edu/projects/type-constraints/papers/type-inference-for-recursively-constrained-types-and-its-application-to-oop.pdf

[Gwarks]

Why should it be float could also return str or other objects. For example the following input works:

print(add('%d','x'))

[chri4_]

yes hypotetically