I'm writing some formal semantics for Python. Hopefully some Python guru's can help me out. As program execution moves down through a list of statements, each assignment statement (or expression) it encounters, it infers the type based on context.But does it store this type somewhere then (so the next time in encounters it can check the store and check the type), or does it perform the operation, then throw away the type, and then infer the type again the next time it encounters the variable? This is for Python 3+ btw (hopefully I've made that clear)
Python uses dynamic typing. The type is part of the value. Wherever a value goes, its type goes with it. (You can get an independent value that corresponds to that type with the type() function.) A value's type is only thrown away when the whole value is thrown away. A variable is just a reference to a value: each variable refers to exactly one value, and in general it can be any possible value, with no restrictions on type.
For example, in
a = 2
Python doesn't make a an int variable; 2 is what has the type int. a is just a reference to 2, which happens to be an integer. When you then write
b = a + 3
Python gets the type of a by simply getting the value referred to by a, and then getting the type of that. The expression is evaluated and the result stored in b.
From the point of view of a statically typed language, it's as if every variable in Python has the same type value, thus each holds a value.
For more information on static and dynamic typing, see this other question.