Skip to content

Type check for polymorphic function types #13918

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

Open
Adam-Vandervorst opened this issue Nov 10, 2021 · 7 comments
Open

Type check for polymorphic function types #13918

Adam-Vandervorst opened this issue Nov 10, 2021 · 7 comments

Comments

@Adam-Vandervorst
Copy link

Adam-Vandervorst commented Nov 10, 2021

Compiler version

3.1.2-RC1-bin-20211102-82172ed-NIGHTLY

Minimized code

I've found it really hard to minimize this due too all the moving components.
You can click the little triangle to see the full attempt.

Here are the bits where I think it goes wrong:

// a generated group of tests for type V
// reduced from a collection of these
val condUpperBoundPartialOrdering: [V] => () => TestGroup[V]

// a function that check if a group of tests applies to a specific object
// inline here is necessary for it to work (the positive case)
inline def appliesTo[V](tl: TestLattice[_, V], v: TestGroup[V]): Boolean

// applying the test check to an object
// reduced form a "reduce"
def app[X, Y](x: X, f: X => Y): Y
// Necesarry abstract definitions
trait JoinLattice[A] extends PartialOrdering[A]:
  override def tryCompare(x: A, y: A): Option[0 | 1 | -1] = ???
  override def lteq(x: A, y: A): Boolean = ???

trait UpperBound[A]
trait LowerBound[A]
trait Finite[A]:
  val elements: Set[A]

trait Atomic[A] extends LowerBound[A]
trait CoAtomic[A] extends UpperBound[A]

trait BoundedJoinLattice[A] extends JoinLattice[A] with LowerBound[A]
trait DoubleBoundedJoinLattice[A] extends BoundedJoinLattice[A] with UpperBound[A]
trait AtomicJoinLattice[A] extends BoundedJoinLattice[A] with Atomic[A]
trait BoundedCoAtomicJoinLattice[A] extends BoundedJoinLattice[A] with CoAtomic[A]
trait DoubleAtomicJoinLattice[A] extends BoundedCoAtomicJoinLattice[A] with AtomicJoinLattice[A]

trait FiniteDoubleAtomicJoinLattice[A] extends DoubleAtomicJoinLattice[A] with Finite[A]

// Necesarry concrete definitions
def optionsLattice[A](options: Seq[A]) = new FiniteDoubleAtomicJoinLattice[Set[A]]:
  val elements = options.toSet.subsets.toSet

def evidenceLattice[A] = new BoundedJoinLattice[(Set[A], Set[A])] {}

// Test utils
abstract class TestGroup[V]:
  type R
  val group: String

case class TestLattice[R, V](val name: String, lattice: R, elements: Iterable[V]):
  type Lattice = R
  type Carrier = V

object TestLattice:
  def fromFinite[R <: Finite[V], V](name: String, lattice: R) =
    TestLattice(name, lattice, lattice.elements)

// Util for example
def app[X, Y](x: X, f: X => Y) = f(x)

inline def appliesTo[V](tl: TestLattice[_, V], v: TestGroup[V]) =
  tl.lattice match
    case q: v.R => println(("matches", v, q))
    case q => println(("misses", v, q))

// Values for example
val to_test = Seq(
  TestLattice("Evidence (Set, Set)", evidenceLattice[Int], {
    val range = (0 to 3).toSet.subsets.toSet
    for x <- range; y <- range yield (x, y)
  }),
  TestLattice.fromFinite("Options (Set)", optionsLattice(1 to 4))
)

val condUpperBoundPartialOrdering = [V] => () => new TestGroup[V]:
  type R = UpperBound[V] & PartialOrdering[V]
  val group = "UpperBound PartialOrdering laws"

@main def example =
  for ins <- to_test do
    // this works correctly
    app(condUpperBoundPartialOrdering[ins.Carrier](), v => appliesTo(ins, v))
    // this does not compile
//    app(condUpperBoundPartialOrdering, v => appliesTo(ins, v[ins.Carrier]()))

Output

[error]    |      app(condUpperBoundPartialOrdering, v => appliesTo(ins, v[ins.Carrier]()))
[error]    |                                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |Found:    ([V] => () => TestGroup[V]{R = IP.lib.UpperBound[V] & PartialOrdering[V]}) => 
[error]    |  Unit
[error]    |Required: ([V] => () => TestGroup[Any]{R = IP.lib.UpperBound[Any] & PartialOrdering[Any]}) =>
[error]    |  Unit

Expectation

Work the same as

app(condUpperBoundPartialOrdering[ins.Carrier](), v => appliesTo(ins, v))

Two things here:

  • I kinda expect ([V] => () => TestGroup[V]{R = IP.lib.UpperBound[V] & PartialOrdering[V]}) to match type ([V] => () => TestGroup[Any]{R = IP.lib.UpperBound[Any] & PartialOrdering[Any]})?
  • I expect (λx.G) (f v) to be equivalent to (λx.G[x := (f x)]) v.
@Adam-Vandervorst Adam-Vandervorst changed the title Polymorphic function types type check Type check for polymorphic function types Nov 10, 2021
@KacperFKorban KacperFKorban added the stat:needs minimization Needs a self contained minimization label Nov 10, 2021
@KacperFKorban
Copy link
Member

  1. Could you fill in the compiler version?
  2. Could you also paste a complete snippet you're running?

@Adam-Vandervorst
Copy link
Author

Adam-Vandervorst commented Nov 10, 2021

I updated the post, but I think I've reduced it to:

class Base[X] {type Carrier = X}
class Cond[V] {type Match}

trait TA[X]
trait TB[X]
trait TAdvancedA[X] extends TA[X]
trait TAdvancedB[X] extends TB[X]

trait T1[X] extends Base[X] with TA[X]
trait T2[X] extends Base[X] with TA[X] with TAdvancedB[X]

def insT1[A] = new T1[Set[A]] {}
def insT2[A] = new T2[(Set[A], Set[A])] {}

val condAB = [V] => () => new Cond[V] {type Match = TA[V] & TB[V]}

@main def example =
  def app[X, Y](x: X, f: X => Y) = f(x)

  for ins <- Seq(insT1[String], insT2[Int]) do
    // this works correctly
    println(app(condAB[ins.Carrier](), v => ins.isInstanceOf[v.Match]))
    // this does not compile
//    println(app(condAB, c => {val v = c[ins.Carrier](); ins.isInstanceOf[v.Match]}))

@odersky odersky added itype:enhancement and removed itype:bug stat:needs minimization Needs a self contained minimization labels Nov 11, 2021
@odersky
Copy link
Contributor

odersky commented Nov 11, 2021

It's known that polymorphic function types don't play well with type inference, and usually have to be instantiated explicitly.

@Adam-Vandervorst
Copy link
Author

What does it mean to be instantiated explicitely here?
Is there a spec or test case that circumvents this issue I can take a look at?

@bishabosha
Copy link
Member

bishabosha commented Nov 12, 2021

What does it mean to be instantiated explicitely here?

you will need to supply the types to app explicitly:
e.g.

for ins <- Seq(insT1[String], insT2[Int]) do
  println(app[condAB.type, Boolean](condAB, c => {val v = c[ins.Carrier](); ins.isInstanceOf[v.Match]}))

@Adam-Vandervorst
Copy link
Author

Hmm that only works in the case of hard coded conditions right @bishabosha?
So with foreach instead of app

  val inss = Seq(insT1[String], insT2[Int])
  val conds = Seq(condAB, condQA)

  for ins <- inss; cond <- conds do
    val v = cond[ins.Carrier]()
    println(ins.isInstanceOf[v.Match])

I can't use condAB.type (and this fails with parameter cond does not take type parameters).
But anything else is too wide? E.g.

  val conds = Seq[[V] => () => TestGroup[V]](condAB, condQA)

gives the wrong result.

@bishabosha
Copy link
Member

What you are doing in this example relies on static types to work, so I can only to suggest that you zip each Cond with a test when you construct the Seq

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

4 participants