Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Consistently apply type implications #1174

Open
5 tasks
degory opened this issue Apr 17, 2024 · 0 comments
Open
5 tasks

Consistently apply type implications #1174

degory opened this issue Apr 17, 2024 · 0 comments

Comments

@degory
Copy link
Owner

degory commented Apr 17, 2024

Type inference in ghūl works in two directions:

  1. Right to left, inner expressions to outer expressions ('type inference')
  2. Left to right, outer expressions to inner expressions ('type implication' / 'type constraints')

There are scenarios where these mechanisms could be applied but currently aren't and there are two different implementations of the second mechanism that should be unified, because currently type information doesn't propagate if the producer is using one implementation and the consumer expects the other

Producers of type implications:

  • Overload resolution produces type implications - where a single overload unambiguously matches the supplied argument types, even if some types are unknown or partially unknown, overload resolution will propose that overload and supply implied actual types for all arguments

Consumers of type implications:

  • Function literal arguments without explicit types will be assigned the type implied by the actual argument type of any matching overload. In this example, the argument of filter is already known to be int -> bool. The lambda argument n initially has unknown type, but a type implication of int -> bool is passed down into the lambda from the overload resolution for filter, and n picks up the type int from here
[1, 2, ,3 ,4] | .filter(n => n % 2 ==0) 

Producers of type constraints:

  • Local variable definitions with explicit types and initializers. The explicit type is passed into the initializer as a type constraint.
  • Return statements in functions of non-void return type. The function return type is passed into the return statement expression as a type constraint
  • Expression body of functions of non-void return type. The function return type is passed into the expression body as a type constraint

Consumers of type constraints:

  • let in expressions - Any type constraint passed into a let in expression is propagated into its expression
  • if expressions - If expressions apply any supplied constraint to their branch expressions, in preference to inferring a common type. They also propagate any type constraint into their branches.
  • List literals - List literals use any type constraint as their element type, in preference to inferring a common type. The currently do not propagate any type constraint into their branches, but they arguably should.

Type constraints and type implications should be unified:

  • Overload resolution should be changed to produce type constraints instead of implications
  • Function literal argument type inference should be changed to consume type constraints instead of implications
  • Error messages may need to be clarified in the case where type constraints are not met for function literal arguments (should be reported as the compiler failing to correctly infer argument type, rather than misleadingly reporting that the user has supplied a value of incorrect type)

Type constraints could be produced in additional places:

  • Left side of assignment statements. This is awkward to implement, because the left side expects to be given an evaluated right side to consume. However, we could try to speculatively load the left side (rather than assign to it) in order to determine its type. If that succeeds, then push the resulting type into the right side as a constraint. If it fails, discard any errors and don't set any constraint. Destructuring would need to be handled differently - we'd need to create a tuple type corresponding to the left side pattern, but discard it if the right hand side is not a tuple literal (or something else comprised of only tuple literals like a list literal or if expression)
  • List literal element types. This would require a speculative first walk to determine LUB, and then a second actual walk where the element type determined by LUB is applied to each element as a type constraint. I think this is a requirement for supporting Tuple literal type covariance  #1166 for tuple literals within a list literal)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Development

No branches or pull requests

1 participant