| Skolems | Grzegorz Kossakowski | 16/07/12 05:48 | 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 |
| Re: [scala-internals] Skolems | Eugene Burmako | 16/07/12 05:53 | Would be very interesting to know indeed. |
| Re: [scala-internals] Skolems | Paul Phillips | 16/07/12 06:00 | 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.")
|
| Re: [scala-internals] Skolems | Grzegorz Kossakowski | 16/07/12 06:02 | I saw that comment and had the same feeling. :-) Grzegorz Kossakowski |
| Re: [scala-internals] Skolems | martin | 16/07/12 07:04 | 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 |
| Re: [scala-internals] Skolems | Grzegorz Kossakowski | 16/07/12 07:40 | 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 |
| Re: [scala-internals] Skolems | Paul Phillips | 16/07/12 07:53 |
It is a problematic kind of recursion, very much so: a whole bunch of bugs are tied up in it. For the different handling in method/class, I vaguely recall variance is a factor. It feels like one anyway.
|
| Re: [scala-internals] Skolems | martin | 18/07/12 05:17 | 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
|
| Re: [scala-internals] Skolems | Adriaan Moors | 14/12/12 13:39 | 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):
Maybe something to explore in dotty? |
| Re: [scala-internals] Skolems | Paul Phillips | 14/12/12 19:12 | On Fri, Dec 14, 2012 at 1:39 PM, Adriaan Moors <adriaa...@typesafe.com> wrote: My gleeful giggling at this prospect can be heard for decameters. |
| Re: [scala-internals] Skolems | martin | 15/12/12 02:22 | On Fri, Dec 14, 2012 at 10:39 PM, Adriaan Moors <adriaa...@typesafe.com> wrote: 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.
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.
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.
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.
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.
Yes, definitely. I'll try some of these things out and report. Cheers - Martin
|
| Re: [scala-internals] Skolems | Paul Phillips | 20/12/12 15:48 | On Sat, Dec 15, 2012 at 2:22 AM, martin odersky <martin...@epfl.ch> wrote: 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 // ^ } |