|
|
HI: When I read "scala language specification", I saw "skolemization" and "type packing" in the following three sections: http://scala-lang.org/files/archive/spec/2.11/03-types.html#existential-types http://scala-lang.org/files/archive/spec/2.11/03-types.html#conformance http://scala-lang.org/files/archive/spec/2.11/06-expressions.html#expression-typing What does them mean? I found in the https://en.wikipedia.org/wiki/Skolem_normal_form , which says: ..................... s an example, the formula [image: \forall x \exists y \forall z. P(x,y,z)] is not in Skolem normal form because it contains the existential quantifier [image: \exists y]. Skolemization replaces [image: y] with [image: f(x)], where [image: f] is a new function symbol, and removes the quantification over [image: y]. The resulting formula is [image: \forall x \forall z . P(x,f(x),z)]. The Skolem term [image: f(x)] contains [image: x], but not [image: z], because the quantifier to be removed [image: \exists y] is in the scope of [image: \forall x], but not in that of [image: \forall z]; ..................... I can understand the above words, but I still do not catch the things in "scala language specificaton". Something I found that written by Martin is as follow, which I do not understand: https://groups.google.com/forum/#!msg/scala-internals/0j8laVNTQsI/kRXMF_c8bGsJ ..................... 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 ..................... Could someone give a talk? Many Thanks. You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
An existential type is a type that contains variables that have some unknown type. A skolem is a representation of that unknown type variable. When you "unpack" an existential, you strip the existential quantifier and replace the quantified (unknown) type variables by a fresh skolem, so that two different unpacking yield distinct types. This reflects that the existentially bound type variable is unknown. A skolem is some constant of which you have no knowledge, nor can you relate it to anything else but itself, which amounts to the same thing (it's an unknown). Packing an existential type is the converse operation: replace all skolems by type variables and existentially quantify them. In practice, you need to "go under the binder" (aka unpack, strip off the existential quantifiers) to compare two existential types, when you match I highly recommend chapter 24 of https://www.cis.upenn.edu/~bcpierce/tapl/ for an in-depth treatment. cheers adriaan You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
It sounds to me like skolems are the type-level analog of actual parameters. The T is the formal parameter, and the type it gets instantiated to is the actual parameter, the skolem. You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
They're more like the type-level analogue of assumptions, which can be viewed as actuals in some sense. An existential type is saying "there is some type here", and a skolem is saying "let's just pretend we have that type right here." It's lifting (or unpacking) the existential type into an inner scope in which the existential behaves like a universal. The code which uses the unpacked type must be checked with the assumption that *any* type may be found in the instantiation of the existential, since we aren't given any information beyond its kind. Amusingly, university courses in symbolic logic generally skip over this property of logic (and its extremely useful applications in proof construction) when taught by mathematics departments. Philosophy departments are generally more rigorous, and skolemization (in both directions) is usually a required technique in any higher-order symbolic proofs. This is skolemization – the equivalence between a rank-n existential and a rank-(n±1) universal – and it does work in both directions. If you squint, you can see a type parameter on a function as being existential within the scope of the function itself. This is the same idea of packing and unpacking, but in reverse and with a universal rather than an existential. This is also why parametric polymorphism can be viewed as a form of information hiding (a property generally associated with existentiality, rather than universality). Daniel You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
Thansk very much. I got it! A skolem is just an unkown but fixed type. You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
Thanks very much. I'll see "rank-n types". You received this message because you are subscribed to the Google Groups "scala-internals" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout. |
Related discussions
Discussion Overview
Group Scala-internals
asked Mar 7 2016 at 07:26
active Mar 17 2016 at 00:51
posts:6
users:4
Recent questions