Wrong inferred type for values of dictionary

[caterinaurban]

From @caterinaurban on July 28, 2017 13:35

The type inferred for env in the following program is wrong:

class Aexp:
    def eval(self, env):
        return 0

class IntAexp(Aexp):
    def __init__(self, i):
        self.i = i

    def eval(self, env):
        return self.i

class BinopAexp(Aexp):
    def __init__(self, op, left, right):
        self.op = op
        self.left = left
        self.right = right

    def eval(self, env):
        left_value = self.left.eval(env)
        right_value = self.right.eval(env)
        if self.op == '/':
            value = left_value / right_value
            return value
        else:
            raise RuntimeError('unknown operator: ' + self.op)

class Statement:
    def eval(self, env):
        pass

class AssignStatement(Statement):
    def __init__(self, name, aexp):
        self.name = name
        self.aexp = aexp

    def eval(self, env):
        value = self.aexp.eval(env)
        env[self.name] = value

"""
x = 0
x = 1 / 2
"""

env = dict()
i = AssignStatement('x', IntAexp(0))
d = BinopAexp('/', IntAexp(1), IntAexp(2))
f = d.eval(env)
a = AssignStatement('x', d)
a.eval(env)
print(env)

The type should be Dict[str, float] but Dict[str, int] is inferred instead.

Copied from original issue: caterinaurban/Lyra#59

[caterinaurban]

From @mostafa-abdullah on August 2, 2017 7:34

The reason for this is that the type of self.aexp in AssignmentStatement is of type Aexp, and method eval in Aexp returns an int.

This will be solved after merging the covariance/contravariance PR, because in this case the return type of eval in Aexp will be a supertype of the return type of any overriding method.

[caterinaurban]

I tried the covariance/contravariace PR and it returns unsat...

[caterinaurban]

From @mostafa-abdullah on August 2, 2017 7:49

Yes it should give unsat because the return type of eval in Aexp is still int.

Changing return 0 to return 1.0 will give sat

[caterinaurban]

The program is perfectly correct, I do not think we should change it. The inference should just be able to infer type float for eval in Aexp. We probably have a type equality somewhere where we should have a subtyping relation instead.

[caterinaurban]

From @mostafa-abdullah on August 2, 2017 7:59

Done

[mostafa-abdullah]

This is fixed now after merging #7

[caterinaurban]

Can you add a test file called issue02.py?

[mostafa-abdullah]

The program in this issue is already a subset of the test file imp.py, which contains the correct checking for the type of the dict env.

[caterinaurban]

No, this is different because of the encoded imp program at the end of the file. I would like to have this as well.

[mostafa-abdullah]

13