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

implement higher-order unification for type constructor inference #2712

Closed
scabug opened this issue Nov 27, 2009 · 20 comments
Closed

implement higher-order unification for type constructor inference #2712

scabug opened this issue Nov 27, 2009 · 20 comments
Assignees
Milestone

Comments

@scabug
Copy link

scabug commented Nov 27, 2009

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 ... 
}
@scabug
Copy link
Author

scabug commented Nov 27, 2009

Imported From: https://issues.scala-lang.org/browse/SI-2712?orig=1
Reporter: @adriaanm
Other Milestones: 2.12.0-M5
See #4719
Blocks #5993

@scabug
Copy link
Author

scabug commented Jun 4, 2011

Harrison Klaperman (hlklaperman) said:
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...

@scabug
Copy link
Author

scabug commented Oct 19, 2011

@Blaisorblade said:
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.

@scabug
Copy link
Author

scabug commented Nov 6, 2011

@milessabin said:
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.

@scabug
Copy link
Author

scabug commented Dec 9, 2011

@Blaisorblade said:
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.

@scabug
Copy link
Author

scabug commented Dec 2, 2012

@retronym said:
See also #6744, where we would like to infer these sort of types in pattern matching.

@scabug
Copy link
Author

scabug commented Dec 2, 2012

@pchiusano said:
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).

@scabug
Copy link
Author

scabug commented Apr 19, 2013

Dan Rosen (mergeconflict) said:
To Paul's comment, I agree that looking at the type parameters as curried, partially applied from left to right (#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 * -> *.

@scabug
Copy link
Author

scabug commented Sep 17, 2014

@Blaisorblade said:
It seems somehow I never mentioned higher-order pattern unification by Miller, which is what Agda uses — the paper I linked ("Unification via explicit substitutions: The case of higher-order patterns") is indeed about that. For whatever reason, everybody steers away from the original Huet algorithm, including modern implementation of lambdaProlog (which is what "Partial Polymorphic Type Inference and Higher-Order Unification" uses).

@scabug
Copy link
Author

scabug commented Jun 30, 2015

@adriaanm said:
Oh, jira.

@scabug
Copy link
Author

scabug commented Jun 30, 2015

@SethTisue said:
#2712 closed!! Dewey defeats Truman!!

@scabug
Copy link
Author

scabug commented Jun 30, 2015

@milessabin said:
That was cruel and heartless ...

@scabug
Copy link
Author

scabug commented Jun 30, 2015

@etorreborre said:
My heart rate went up for a moment...

@scabug
Copy link
Author

scabug commented Jun 30, 2015

Stephen Compall (s11001001) said:
long, wistful sigh

@scabug
Copy link
Author

scabug commented Jul 1, 2015

Jed Wesley-Smith (jedws) said:
well, that was (briefly) exciting!

@scabug
Copy link
Author

scabug commented Jul 23, 2015

Matthew Pocock (drdozer) said:
I keep on hitting this issue in various forms, most recently when trying to use type lambdas to fill in one of two types on a * -> * -> * kinded type. I have this type:

case class RangeAs[R, V](range: R, lower: V, upper: V)

object RangeAs {
  trait Aux[V] {
    type l[R] = RangeAs[R, V]
  }
}

There are various implicit instances with RangeAs.Aux[X]#l as one of their type parameters. They are not found in all situations if I attempt to summon them using the lambda. However, if I do this:

type RangeAsX[T] = RangeAs.Aux[X]#l[T]

Now if I summon them using RangeAsX, they are found.

@scabug
Copy link
Author

scabug commented Apr 12, 2016

@ijuma said:
For the watchers of this JIRA that haven't seen this on Twitter, Miles posted a demo project exercising a proposed fix for this JIRA:

https://github.com/milessabin/si2712fix-demo

@scabug
Copy link
Author

scabug commented Apr 15, 2016

@milessabin said:
PR against 2.12.x here: scala/scala#5102.

@scabug scabug closed this as completed May 27, 2016
@scabug
Copy link
Author

scabug commented Aug 26, 2016

@milessabin said:
Backport to 2.11.8 available here.

@scabug
Copy link
Author

scabug commented Oct 18, 2016

@adriaanm said:
2.11.9 PR: scala/scala#5343

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