what does "skolemization" and "type packing" mean?

[woshilaiceshide]

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 is not in Skolem normal form because it contains the existential quantifier . Skolemization replaces with , where is a new function symbol, and removes the quantification over . The resulting formula is . The Skolem term contains , but not , because the quantifier to be removed is in the scope of , but not in that of ;
.....................
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.

[Adriaan Moors]

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 on a value of existential type, and so on.

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 scala-interna...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Lyle Kopnicky]

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.

[Daniel Spiewak]

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

[woshilaiceshide]

Thansk very much. I got it! A skolem is just an unkown but fixed type.

[woshilaiceshide]

Thanks very much. I'll see "rank-n types".