Skolems

[Grzegorz Kossakowski]

Hi,

I'm getting brave enough to touch earlier phases of the compiler than backend (anything before cleanup) I find myself in need to understand a concept of a type skolem.

I vaguely understand that if you look at type parameter from inside of the scope where it's defined then I see the skolem and if I look from outside (e.g. at method definition with type parameter) then I see some poly type with bounds. Still, I don't understand what kind of problem skolems solve? What's the rationale to have them?

Any pointers to docs/discussions/examples would be useful.

--
Grzegorz Kossakowski

[Eugene Burmako]

Would be very interesting to know indeed.

[Paul Phillips]

I'm the wrong guy to answer so I won't, but I have a favorite comment from the days when I had even less idea about skolems than I do now:

    /** If this symbol is a type parameter skolem (not an existential skolem!)

     *  its corresponding type parameter, otherwise this */

    def deSkolemize: Symbol = this

Not an existential skolem!

(It's not that the comment isn't sensible, but amuses me in a manner similar to "to understand recursion, you must understand recursion.")

[Grzegorz Kossakowski]

I saw that comment and had the same feeling. :-)

--
Grzegorz Kossakowski

[martin odersky]

Skolems are indeed synthetic type "constants" that are copies of existentially bound or universally bound type variables. E.g.

if you are in the rhs a method

  def foo[T](x: T) = ... foo[List[T]]....

the skolem named T refers to the unknown type instance of T when foo is called. It needs to be different from the type parameter because in a recursive call as in the foo[List[T]] above the type parameter gets substituted with List[T], but the type skolem stays what it is. 

The other form of skolem is an existential skolem. Say you have a function

  def bar(xs: List[T] forSome { type T }) = xs.head

the each occurrence of xs on the right will give have type

  List[T'] where T' is a fresh copy of T.

That's what we call an existential skolem. Hope this helps! - Martin

--
Martin Odersky
Prof., EPFL and Chairman, Typesafe
PSED, 1015 Lausanne, Switzerland
Tel. EPFL: +41 21 693 6863
Tel. Typesafe: +41 21 691 4967

[Grzegorz Kossakowski]

On 16 July 2012 16:04, martin odersky <martin....@epfl.ch> wrote:

Skolems are indeed synthetic type "constants" that are copies of existentially bound or universally bound type variables. E.g.

if you are in the rhs a method

  def foo[T](x: T) = ... foo[List[T]]....

the skolem named T refers to the unknown type instance of T when foo is called. It needs to be different from the type parameter because in a recursive call as in the foo[List[T]] above the type parameter gets substituted with List[T], but the type skolem stays what it is. 

The other form of skolem is an existential skolem. Say you have a function

  def bar(xs: List[T] forSome { type T }) = xs.head

the each occurrence of xs on the right will give have type

  List[T'] where T' is a fresh copy of T.

That's what we call an existential skolem. Hope this helps! - Martin

It indeed helps but I have a few more doubts. It seems like recursion is at the root of the problem. Why don't we introduce skolems for class parameters?

Is it because declarations like that are illegal:

class Foo[T] extends Foo[List[T]]

?

Still we have some form of recursion that is allowed in class definitions:

class Foo[T <: Foo[T]]

so why this is not a problematic kind of recursion that not need to be solved with skolems?

--
Grzegorz Kossakowski

[Paul Phillips]

On Mon, Jul 16, 2012 at 7:40 AM, Grzegorz Kossakowski <grzegorz.k...@gmail.com> wrote:

class Foo[T <: Foo[T]]

so why this is not a problematic kind of recursion that not need to be solved with skolems?

It is a problematic kind of recursion, very much so: a whole bunch of bugs are tied up in it.

  https://issues.scala-lang.org/browse/SI-2251

For the different handling in method/class, I vaguely recall variance is a factor.  It feels like one anyway.

[martin odersky]

I think we should and we tried but because of classes' open recursion it was too tough. Consequently, we allow GADT behavior only for method type parameters. 

So, in a nutshell, skolems support GADTs (because you can attach local information to a skolem without touching the type parameters).

Cheers

 - Martin

[Adriaan Moors]

I was discussing an alternative strategy with Paul regarding TypeVars, and potentially also skolems.

The context was reducing mutation in the type checker.

The idea would be to track a map  from undetermined type parameter symbols to TypeConstraints in the Context (instead of just a list),

make subtyping (and related methods) context-sensitive (so that they can consult the undetparamToTypeConstraint map),

this would allow us to get rid of the following mutations (off the top of my head -- there may be more):

• undoLog (push a new context on the stack when a subtype check must be undoable, pop it when done)
• the substitution of typerefs to typevars (simply populate the undetparams map with fresh type constraints)
  
• skolemisation (we'd be mutating the TypeConstraint in the current context rather than the method type param symbol's info)
• this would then work uniformly for class & method type params
• type var suspension (in findMember)

Maybe something to explore in dotty?

[Paul Phillips]

On Fri, Dec 14, 2012 at 1:39 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:

this would allow us to get rid of the following mutations (off the top of my head -- there may be more):

My gleeful giggling at this prospect can be heard for decameters.

[martin odersky]

On Fri, Dec 14, 2012 at 10:39 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:

I was discussing an alternative strategy with Paul regarding TypeVars, and potentially also skolems.

The context was reducing mutation in the type checker.

The idea would be to track a map  from undetermined type parameter symbols to TypeConstraints in the Context (instead of just a list), 

make subtyping (and related methods) context-sensitive (so that they can consult the undetparamToTypeConstraint map),

this would allow us to get rid of the following mutations (off the top of my head -- there may be more):

Hi Adriaan,

It's a mouth-watering summary. I have been thinking along the same lines and it's great to see it all listed together. The main reason we cannot do it easily in the current nsc design is that contexts don't reach the isSubType method, and it would take a lot to change that. 

• undoLog (push a new context on the stack when a subtype check must be undoable, pop it when done)

Yes, except that I don't think pushing would work because adding a constraint to a variable is a global effect (in the current inference step). So I believe in the end we need to mutate the context by adding a new constraint somewhere. Simply pushing a subcontext to the children won't work. Right?

Rather than having isSubType mutate the context I was thinking of creating a subtyper object that would collect the new constraints generated during subtyping and integrating that into the current context some levels higher up.

• the substitution of typerefs to typevars (simply populate the undetparams map with fresh type constraints)
  

That's what I would hope, but I am not 100% sure we can do it yet. The problem is that by substituting typerefs to typevars we create a new instance on which we can work independently of all other instances. To avoid that substitution we'd need to convince ourselves that every polytype can appear only in a single instance in a type computation. Is that true? I would hope so, but am not sure.

• skolemisation (we'd be mutating the TypeConstraint in the current context rather than the method type param symbol's info)
• this would then work uniformly for class & method type params

If you mean the skolemization in Namers, I believe we still need it precisely because of the multiple instance problem. Skolemized variables are for the current instance of a polymorphic method. If the method calls itself recursively, the two instances are independent. E.g.

  def poly[T](x) = poly[(T, T)]((x, x))

Here we get the constraint that

    Typeparam T :> (Skolem T, Skolem T)

If we identify the skolem and the type param we get something nonsensical.

• type var suspension (in findMember)

That's actually more a question whether membership should add constraints to type variables. If it shouldn't, we need to find some mechanism to avoid adding constraints for variables in operations like

baseType. It would be nice if we could drop it, though.

 

Maybe something to explore in dotty?

Yes, definitely. I'll try some of these things out and report.

Cheers

 - Martin

 

On Wednesday, July 18, 2012 5:17:22 AM UTC-7, martin wrote:

On Mon, Jul 16, 2012 at 4:53 PM, Paul Phillips <pa...@improving.org> wrote:

On Mon, Jul 16, 2012 at 7:40 AM, Grzegorz Kossakowski <grzegorz.k...@gmail.com> wrote:

class Foo[T <: Foo[T]]

so why this is not a problematic kind of recursion that not need to be solved with skolems?

It is a problematic kind of recursion, very much so: a whole bunch of bugs are tied up in it.

  https://issues.scala-lang.org/browse/SI-2251

For the different handling in method/class, I vaguely recall variance is a factor.  It feels like one anyway.

I think we should and we tried but because of classes' open recursion it was too tough. Consequently, we allow GADT behavior only for method type parameters. 

So, in a nutshell, skolems support GADTs (because you can attach local information to a skolem without touching the type parameters).

Cheers

 - Martin

[Paul Phillips]

On Sat, Dec 15, 2012 at 2:22 AM, martin odersky <martin....@epfl.ch> wrote:

It's a mouth-watering summary. I have been thinking along the same lines and it's great to see it all listed together. The main reason we cannot do it easily in the current nsc design is that contexts don't reach the isSubType method, and it would take a lot to change that.

An additional point in favor of doing whatever it takes to introduce contexts to Types is that lubs currently cannot be calculated correctly (see examples below) since that's another place contexts don't reach. In order to correctly perform any fold over multiple types (mergePrefixAndArgs, lub, glb, etc.) we need a means of determining the acceptability of the resulting types at the point where the inference is taking place. It isn't enough to check the type at the end, because it leaves you with no way to calculate a weaker type if it the result isn't valid, and also because it might deliver an accessible type by combining inputs from inaccessible types; sort of the type-level equivalent of simplifying { ??? ; 5 } to 5.

I think all such type calculations need a mechanism to perform visibility/accessibility checks, and every intermediate type should be routed through a test which weakens the type until it is visible and accessible.

Accessibility:

 

package a {

  private[a] trait Impl { def f = 5 }

  class Vis1 extends Object with Impl

  class Vis2 extends Object with Impl

  object Vis {

    def f = new Vis1

    def g = new Vis2

    def lub = List(f, g)  // this should be (and is) a List[Impl]

  }

}

package b {

  object Elsewhere {

    import a.Vis._

    def lub = List(f, g) // this should not be (but is) a List[a.Impl]

  }

}

Visibility:

class A {

  def f = { trait A ; trait B extends A ; trait C extends B ; new C { } }

  // inferred type:

  // $anon forSome { type $anon <: Object with B; type B <: Object }

  //

  // Hey, what's a B?

  lazy val g = f

  // d.scala:8: error: type mismatch;

  //  found   : $anon(in lazy value g) where type $anon(in lazy value g) <: Object with B

  //  required: (some other)$anon(in lazy value g) forSome { type (some other)$anon(in lazy value g) <: Object with B; type B <: Object }

  //   lazy val g = f

  //                ^

}