Scala Programming Language
  1. Scala Programming Language
  2. SI-4699

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

    Details

      Description

      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

        Issue Links

          Activity

          Hide
          Paolo G. Giarrusso added a comment -

          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 SI-5298).

          Show
          Paolo G. Giarrusso added a comment - 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 SI-5298 ).
          Hide
          Paul Phillips added a comment -

          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.

          Show
          Paul Phillips added a comment - 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.
          Hide
          Daniel Sobral added a comment -

          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.

          Show
          Daniel Sobral added a comment - 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.
          Hide
          Paul Phillips added a comment -

          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.

          Show
          Paul Phillips added a comment - 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.
          Hide
          Paolo G. Giarrusso added a comment -

          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 SI-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

          Show
          Paolo G. Giarrusso added a comment - 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 SI-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
          Hide
          Adriaan Moors added a comment -

          Unassigning as milestone deadline was reached.

          Show
          Adriaan Moors added a comment - Unassigning as milestone deadline was reached.
          Hide
          Adriaan Moors added a comment -

          fixed as part of SI-3346

          Show
          Adriaan Moors added a comment - fixed as part of SI-3346

            People

            • Assignee:
              Eugene Burmako
              Reporter:
              Adriaan Moors
            • Votes:
              4 Vote for this issue
              Watchers:
              10 Start watching this issue

              Dates

              • Created:
                Updated:
                Resolved:

                Development