feat: Type check lists and comprehensions #69
Conversation
mark-koch
changed the title
guppy/checker/expr_checker.py
Outdated
| node, | ||
| ) | ||
| if exp_ty: | ||
| assert var is not None |
There was a problem hiding this comment.
I think the argument to this function should then be exp_ty: tuple[FunctionType, FreeTypeVar] | None
guppy/checker/expr_checker.py
Outdated
| ) | ||
| if exp_ty: | ||
| assert var is not None | ||
| exp_ty = cast(FunctionType, exp_ty.substitute({var: ty})) |
There was a problem hiding this comment.
I think things would be neater if this substitution happened in the caller and there was a comment in this function saying what is assumed
| # The rest is checked in a new nested context to ensure that variables don't escape | ||
| # their scope | ||
| inner_locals = Locals({}, parent_scope=ctx.locals) | ||
| inner_ctx = Context(ctx.globals, inner_locals) |
There was a problem hiding this comment.
Should this be inheriting type variables from ctx as well?
There was a problem hiding this comment.
Presumably yes, but we're not tracking them in the Context yet since we don't have polymorphic FuncDefns yet. (This is related to the discussion in the polymorphism PR #61 (comment))
| @@ -240,6 +292,22 @@ def visit_Tuple(self, node: ast.Tuple) -> tuple[ast.expr, GuppyType]: | |||
| node.elts = [n for n, _ in elems] | |||
| return node, TupleType([ty for _, ty in elems]) | |||
|
|
|||
| def visit_List(self, node: ast.List) -> tuple[ast.expr, GuppyType]: | |||
There was a problem hiding this comment.
My inclination is to get rid of this and see if we need it. Lists seem like more of a checkable thing anyway
There was a problem hiding this comment.
I agree that morally, lists feel checkable. But in practice, I think it's good to be able to synthesize a type whenever possible. For example, we want to allow users to write
xs = [1, 2, 3]instead of always having to provide an annotation
xs: list[int] = [1, 2, 3]But this only works if we can synthesize lists.
There was a problem hiding this comment.
I guess the more involved thing to do is come up with a fresh type variable, T for the list element, and when it's used in a comprehension or function application, there will be a synthesised type A -> B such that you can unify T with A.
But in the absence of that (I think this is a later stage in the polymorphism timeline), synthesising lists works!
guppy/checker/expr_checker.py
Outdated
|
|
||
| def visit_IterNext(self, node: IterNext) -> tuple[ast.expr, GuppyType]: | ||
| var = FreeTypeVar.new("Iter", False) | ||
| exp_ty = FunctionType([var], TupleType([FreeTypeVar.new("T", True), var])) |
There was a problem hiding this comment.
I'm not really sure why the "T" variable is linear here. It seems like we would maybe want its linearity to be a function of whether it came from a comprehension over a list or a linst?
There was a problem hiding this comment.
Also, should we not make some note that "T" is the element type of "Iter"
There was a problem hiding this comment.
I'm not really sure why the "T" variable is linear here
Good point, we shouldn't require linearity here. In fact, a user could even write a custom iterator on a linst of qubits that yields classical measurement results in __next__. Or the other way round, a custom iterator on a classical list could return a newly allocated Qubit in __next__. So we cannot infer linearity of the element type from the linearity of the iterator.
Also, should we not make some note that "T" is the element type of "Iter"
You mean storing this as an annotation somewhere? I guess we're already keeping track of it in the synthesized type that is returned
There was a problem hiding this comment.
You mean storing this as an annotation somewhere? I guess we're already keeping track of it in the synthesized type that is returned
I mean, the function type here seems to be forall Iter. Iter -> forall T. [T, Iter]. It seems odd that there's no recorded relationship between T and Iter, and afaict nothing to say that all of the Ts for a given iterator should be the same (maybe in python they don't need to be??)
There was a problem hiding this comment.
Note that we have a FreeTypeVar (now called ExistentialTypeVar) here, so no quantifiers in the type.
Following the change in f51f0bf, we check that the type of the Iter.__next__ function that the user has written for the type Iter can be unified with Iter -> (?T, Iter). This is the only restriction, so there is indeed no direct relationship between the Iter type and the element type T.
However, there can only be a single __next__ method for each type, so the signature of the associated __next__ function uniquely determines the element type for the iterator. Thus, the returned T should be the same for each iteration.
No description provided.