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

Shallow type inference #273

Merged
merged 6 commits into from
Feb 3, 2021
Merged

Shallow type inference #273

merged 6 commits into from
Feb 3, 2021

Conversation

yannham
Copy link
Member

@yannham yannham commented Jan 22, 2021

Depend on #272. Address #139. Determine the type of some unannotated let-bound expressions outside of statically typed code:

  • constants (of the language): number literals, string literals (without interpolated expression), booleans
  • lists: list literals are given the List Dyn type.
  • variables: retrieve the type from the environment.

what this PR doesn't do

  • infer function types (Dyn -> Dyn). It's not clear in what practical situation you would actually need it. If needed, we can do add this later.
  • infer record types: Same as functions. Plus, there are two possible competing types {_ : Dyn} and { | Dyn}, but this is maybe a sign that this a problem with the type system's definition, rather than with inferring the type of records.

Base automatically changed from feature/parametrized-lists to master January 25, 2021 09:16
@dpulls
Copy link

dpulls bot commented Jan 25, 2021

🎉 All dependencies have been resolved !

@yannham yannham force-pushed the feature/shallow-type-inference branch from 00a1456 to b97568f Compare January 28, 2021 11:11
@yannham yannham marked this pull request as ready for review January 28, 2021 11:36
@yannham yannham requested a review from aspiwack February 2, 2021 08:25
src/typecheck.rs Outdated
Comment on lines 817 to 819
// If there are interpolated expressions inside a string, we can't guarantee that this is a
// well-typed string (e.g. "#{1 + 1}" is not). We can only do so if all chunks are string
// literals.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But isn't it guaranteed that if it is well-typed (dynamically), then it is a string? In which case it's fine to return the string type in all cases.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My rule of thumb was that it shouldn't infer a precise (Exact) type for an expression that wouldn't pass the typechecker, that is if apparent_type(e) = exact(T) then e : T must be well-typed. But "#{1 + 1} : Str is not well-typed.

That said, the semantics of interpolated string enforce that such expressions either fails with a type error or evaluate to a string at run-time indeed. So let's return Str in all cases then.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this rule already didn't apply to the Assume case. The only thing that you need of a type, in this gradual type context, is that if the expression doesn't blame, then it has this type (with a fairly strong notion of “doesn't blame”).

src/typecheck.rs Outdated
Term::StrChunks(chunks) if chunks.iter().all(is_literal) => {
ApparentType::Exact(Types(AbsType::Str()))
}
Term::List(_) => ApparentType::Exact(Types(AbsType::List(Box::new(Types(AbsType::Dyn()))))),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a little bit weird to call this case Exact isn't it?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, it was in opposition to Approximated. Maybe Precise, or Inferred?

@yannham yannham merged commit 05ae942 into master Feb 3, 2021
@yannham yannham deleted the feature/shallow-type-inference branch February 3, 2021 16:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants