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

implicit search should more uniformally carry constraints through chained conversions/searches #4699

Closed
scabug opened this issue Jun 15, 2011 · 8 comments
Assignees
Milestone

Comments

@scabug
Copy link

scabug commented Jun 15, 2011

  1. implicit search and implicit conversion search treat undetermined type parameters differently
  2. constraints are carried over in an ad-hoc way (by tracking undetermined type parameters in the context)
    --> this works for influencing the inference of type parameters by "later aspects" of the expression, but not for inferring implicit values, since these cannot be left undetermined while type checking an expression (see [#SI-4653])

the idea of generalising tracking of undetermined implicit types (type parameters)/implicit values and their constraints could drive the solution for [SI-3340], [SI-3346], [SI-2781] and [SI-3270]

@scabug
Copy link
Author

scabug commented Jun 15, 2011

@scabug
Copy link
Author

scabug commented Jan 26, 2012

@Blaisorblade said:
I was wondering: can available implicits be modeled as constraints? Also, could constraint solving be done once per statement, instead of on each invocation (as currently specified)?

The more I run into problems, the more it seems that even more should be delegated to a constraint solver (see also #5298).

@scabug
Copy link
Author

scabug commented Jan 28, 2012

@paulp said:
I've always thought we should be using a separate solver, but I might be biased because it'd be that much less code for me to manage.

@scabug
Copy link
Author

scabug commented Jul 3, 2012

@dcsobral said:
I think using constraint solvers takes advantage of a lot of work that have been done to make them fast, makes it easier to produce a formal specification for it, and easier to change the knobs.

Then again, I don't even know what's underneath, so I might be completely off and this comment just noise.

@scabug
Copy link
Author

scabug commented Jul 3, 2012

@paulp said:
I know what's underneath (on the scala side - I don't know what's underneath the constraint solvers) and if anything you understate the advantages.

@scabug
Copy link
Author

scabug commented Jul 3, 2012

@Blaisorblade said:
I think that writing (and publishing) an implementable and reasonable formal specification has an even bigger advantage: you need to make it understandable and regular (which benefits users). To fix a bug like #5298, you just need to translate bounds to constraints directly; with an ideal proof of "completeness", such a bug would likely be impossible by design, although existing completeness proofs for local type inference systems seem to often have various restrictions. The only obstacle is that defining the formalization risks being extremely complicated - I think it could even be enough for a PhD thesis.

But wasn't Hubert Plociniczak, PhD candidate, planning to use constraint solving to improve both Scala type inference and for the type debugger [1], based on research by Martin Odersky et al. on one side, and GHC hackers on the other? He also gives a number of convincing arguments on why one should use constraint systems. Among others, it's easier to explain type inference errors in terms of constraints.

Of course research proposals for PhD students are not binding - my research proposal had absolutely no relevance (I'm a PhD student). A lot of disclaimers apply for me too: my knowledge of type inference goes barely beyond Pierce's TAPL book, and I've only skimmed his research proposal (too hard for me, sorry).

[1] Hubert Plociniczak, 2010. Making sense out of an advanced type system. Edic research proposal. Available at
http://wiki.epfl.ch/edicpublic/documents/Candidacy%20exam/hubert_plociniczak_candidacy.pdf

@scabug
Copy link
Author

scabug commented Jul 10, 2013

@adriaanm said:
Unassigning as milestone deadline was reached.

@scabug
Copy link
Author

scabug commented Dec 11, 2013

@adriaanm said:
fixed as part of #3346

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants