Add support for module_info functions #496
Conversation
|
Hi, @xxdavid! This is great! I'll currently leave the review for a bit later, but I think I can share something on the question you ask:
In a nutshell, type inference is a significantly harder problem than type checking. In general, it might be possible to type check a fully annotated program in a hypothetical language in a reasonable time, but not to rebuild the annotations if they're missing. Actually, full type inference of practical languages like Haskell or OCaml is undecidable - that's why in some cases the programmer has to provide type annotations to enable a program to compile. It's not a new problem, though, which has focused interest on local methods originally known as local type inference and more recently as bidirectional typing. In practice, it means a type checker alternates between inferencing types where it can and only checking types where it cannot do any better (these are the places where we need annotations to be provided by a programmer). A great paper on that topic is Bidirectional Typing by Dunfield and Krishnaswami. BTW, this question was previously raised, possibly even multiple times, and possibly by me the last time :D @josefs replied back then that:
Recently I also noticed some repetition between these functions, so maybe in practice there's room for improvement. In general, though, |
|
Aha! I haven't thought of that when raising the question. Thanks for your explanation! :slight_smile: And also for linking the previous issue you created that provides additional context. I'm glad I can associate the mysterious |
|
This looks great, thanks @xxdavid! Congrats on the first contribution 🎉 |
|
@xxdavid Ahh, of course I missed something in the review 😅 Fixed in #498. It's worth taking a look at https://github.com/josefs/Gradualizer/actions/runs/3715667032/jobs/6301095725#step:6:14 even if CI is green. The current baseline on master is 39 lines of output. |
| do_type_check_expr(Env, {call, P, {remote, _, _Mod, {atom, _, module_info}} = Name, Args}) -> | ||
| Arity = arity(length(Args)), | ||
| FunTy = get_module_info_type(Arity), |
There was a problem hiding this comment.
I suppose we have a problem if Arity > 1. Perhaps we should break this clause up into explicit matching on arity 0 (Args = []) and 1 (Args = [_]) and fall though for any other arity?
I finally come up with a PR that fixes #473.
I am an Elixir person and haven't written almost any Erlang code before so there may be some things that could be done more idiomatically.
I think I got some (quite little still) idea how Gradualizer works but one thing still isn't clear to me – why isn't
type_check_expr_inimplemented in terms oftype_check_expr. From my limited perspective, it could just determine the type of the expression by callingtype_check_expr_inand then check whether the type is indeed a subtype ofResTy. Why wouldn't that work?