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

implement higher-order unification for type constructor inference

    Details

    • Type: Improvement Improvement
    • Status: Open
    • Priority: Minor Minor
    • Resolution: Unresolved
    • Affects Version/s: None
    • Fix Version/s: None
    • Component/s: Misc Compiler
    • Labels:
      None
    • Environment:

      tcpoly_infer

      Description

      implement what's described in "Partial polymorphic type inference and higher-order unification"

      object Test {
        def meh[M[_], A](x: M[A]): M[A] = x
        meh{(x: Int) => x} // should solve ?M = [X] X => X and ?A = Int ... 
      }
      

        Issue Links

          Activity

          Hide
          Harrison Klaperman added a comment -

          You can find that paper here: http://www.cs.cmu.edu/~fp/papers/lfp88.pdf. I hope this is useful to others who stumble upon this issue. Now if only I understood what the paper were talking about...

          Show
          Harrison Klaperman added a comment - You can find that paper here: http://www.cs.cmu.edu/~fp/papers/lfp88.pdf . I hope this is useful to others who stumble upon this issue. Now if only I understood what the paper were talking about...
          Hide
          Paolo G. Giarrusso added a comment -

          Further work on that problem is described in "Unification via explicit substitutions: The case of higher-order patterns" - http://www.cs.cmu.edu/~fp/papers/INRIA-RR-3591.pdf, from Dowek, Hardin, Kirchner and Pfenning (Pfenning is the author of the above paper). I am not an expert, but this work is cited in Pierce's TAPL (Sec. 23.6, pag. 355), which explains that unlike the algorithm above it is terminating and always finds a unique solution; the paper suggests that this work applies to an important subcase. However, I cannot fully judge myself the respective merits of the two papers.

          Show
          Paolo G. Giarrusso added a comment - Further work on that problem is described in "Unification via explicit substitutions: The case of higher-order patterns" - http://www.cs.cmu.edu/~fp/papers/INRIA-RR-3591.pdf , from Dowek, Hardin, Kirchner and Pfenning (Pfenning is the author of the above paper). I am not an expert, but this work is cited in Pierce's TAPL (Sec. 23.6, pag. 355), which explains that unlike the algorithm above it is terminating and always finds a unique solution; the paper suggests that this work applies to an important subcase. However, I cannot fully judge myself the respective merits of the two papers.
          Hide
          Miles Sabin added a comment -

          With dependent method types we have a somewhat cumbersome, but just about usable workaround. The key idea is to use implicits to destructure a type, and then pick out and use its component parts as dependent types.

          // Template we will unpack into
          trait UnpackM[MA] {
            type M[_]
            type A
          }
            
          // Destructuring implicits
          implicit def unpackM1[M0[_], A0] = new UnpackM[M0[A0]] {
            type M[X] = M0[X]
            type A = A0
          }
          
          implicit def unpackM2[M0[_, _], A0, B0] = new UnpackM[M0[A0, B0]] {
            type M[X] = M0[A0, X]
            type A = B0
          }
          
          def meh[MA](x : MA)(implicit u : UnpackM[MA]) : (u.M[String], List[u.A]) = null
          //      ^^          ^^^^^^^^^^^^^^^^^^^^^^^^     ^^^^^^^^^^^       ^^^
          //      (1)                   (2)                    (3)           (3)
          // 1: Type variable being destructured
          // 2: Destructuring implicit
          // 3: Uses of (dependent) component types
            
          val m = meh{(x: Int) => x}
          implicitly[m.type <:< (Int => String, List[Int])]
          

          See also here for a slightly more elaborate scalaz inspired example.

          Show
          Miles Sabin added a comment - With dependent method types we have a somewhat cumbersome, but just about usable workaround. The key idea is to use implicits to destructure a type, and then pick out and use its component parts as dependent types. // Template we will unpack into trait UnpackM[MA] { type M[_] type A } // Destructuring implicits implicit def unpackM1[M0[_], A0] = new UnpackM[M0[A0]] { type M[X] = M0[X] type A = A0 } implicit def unpackM2[M0[_, _], A0, B0] = new UnpackM[M0[A0, B0]] { type M[X] = M0[A0, X] type A = B0 } def meh[MA](x : MA)(implicit u : UnpackM[MA]) : (u.M[String], List[u.A]) = null // ^^ ^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^ ^^^ // (1) (2) (3) (3) // 1: Type variable being destructured // 2: Destructuring implicit // 3: Uses of (dependent) component types val m = meh{(x: Int) => x} implicitly[m.type <:< (Int => String, List[Int])] See also here for a slightly more elaborate scalaz inspired example.
          Hide
          Paolo G. Giarrusso added a comment -

          Milles Sabin, your workaround is interesting:
          But unfortunately the example you link still needs these two lines:

          type EitherInt[A] = Either[Int, A]
          implicit object EitherTC extends TC[EitherInt]

          Moreover, your code does not even correctly solve the original problem - it only infers that Int => Int matches M0[A0, B0] with M0 = Function1, not that it matches M1[A1] with M1[X] = X => X.

          Show
          Paolo G. Giarrusso added a comment - Milles Sabin, your workaround is interesting: But unfortunately the example you link still needs these two lines: type EitherInt [A] = Either [Int, A] implicit object EitherTC extends TC [EitherInt] Moreover, your code does not even correctly solve the original problem - it only infers that Int => Int matches M0 [A0, B0] with M0 = Function1, not that it matches M1 [A1] with M1 [X] = X => X.
          Hide
          Jason Zaugg added a comment -

          See also SI-6744, where we would like to infer these sort of types in pattern matching.

          Show
          Jason Zaugg added a comment - See also SI-6744 , where we would like to infer these sort of types in pattern matching.
          Hide
          Paul Chiusano added a comment -

          Would it be any easier to just look for partial applications of existing type constructors in left-to-right order? Haskell does roughly this (actually, type constructors are just curried, see below), it is tractable, and people don't seem to have an issue with the limitation, though occasionally you do have to introduce a new type just to flip the order of some type parameters.

          Here's an example:

          case class State[S,A](run: S => (A,S))
          object Blah {
            def foo[M[_],A](m: M[A]): M[A] = m
            ...
            val blah = foo(State((i: Int) => ("hi",i+1)))
          }
          

          Another way to think about this is that type constructors are curried, so State[S,A] is actually represented as Ap(Ap(State, S), A), and likewise the M[A] is Ap(freevar, A) - these unify with freevar = Ap(State, S).

          Show
          Paul Chiusano added a comment - Would it be any easier to just look for partial applications of existing type constructors in left-to-right order? Haskell does roughly this (actually, type constructors are just curried, see below), it is tractable, and people don't seem to have an issue with the limitation, though occasionally you do have to introduce a new type just to flip the order of some type parameters. Here's an example: case class State[S,A](run: S => (A,S)) object Blah { def foo[M[_],A](m: M[A]): M[A] = m ... val blah = foo(State((i: Int) => ("hi",i+1))) } Another way to think about this is that type constructors are curried, so State [S,A] is actually represented as Ap(Ap(State, S), A), and likewise the M [A] is Ap(freevar, A) - these unify with freevar = Ap(State, S).
          Hide
          Dan Rosen added a comment -

          To Paul's comment, I agree that looking at the type parameters as curried, partially applied from left to right (SI-4719) is probably usually good enough.

          If State[S, A] has pseudo-Haskell-ish kind (*, *) -> *, then State[S][A] would have kind * -> * -> *, and State[S] would have kind * -> *.

          Show
          Dan Rosen added a comment - To Paul's comment, I agree that looking at the type parameters as curried, partially applied from left to right ( SI-4719 ) is probably usually good enough. If State[S, A] has pseudo-Haskell-ish kind (*, *) -> * , then State[S][A] would have kind * -> * -> * , and State[S] would have kind * -> * .

            People

            • Assignee:
              Adriaan Moors
              Reporter:
              Adriaan Moors
              TracCC:
              Alan, arjan blokzijl, Christos KK Loverdos, Eric Torreborre, Evgeny, Ismael Juma, Ittay Dror, Johannes Rudolph, Jorge Ortiz, Josh Suereth, Kris Nuttycombe, Mark Harrah, Michael, Miles Sabin, Nick Partridge, Seth Tisue, Tony Morris, weihsiu
            • Votes:
              64 Vote for this issue
              Watchers:
              45 Start watching this issue

              Dates

              • Created:
                Updated:

                Development