Sample of `forSome { val `?

Question

Scala Language Specification specifies syntax of Existential Types as

Type               ::= InfixType ExistentialClauses
ExistentialClauses ::= ‘forSome’ ‘{’ ExistentialDcl
                       {semi ExistentialDcl} ‘}’
ExistentialDcl     ::= ‘type’ TypeDcl
                    |  ‘val’ ValDcl

I have seen a lot code use forSome and type together, e.g.

List[T] forSome { type T; }

But I have never seen forSome with val, is there any sample?

Harkness

Related question Existential Quantification over Values – Gamp

Answer 1

If you think about it, you'll soon realize that the only time values appear in types is wit path dependent types. By example:

trait Trait {
  val x: { type T }
  val y: x.T // path dependent type: here comes our val
}

Applying this to existential types we can now easily cook up a sample of forSome { val:

type SomeList = List[v.T] forSome { val v : { type T }; }

The above type denotes any list whose elements are of a path dependent type v.T.

By example:

object X { 
  type T = String
  val x: T = "hello" 
}
val l1: SomeList = List(X.x) // compiles fine
val l2: SomeList = List(123) // does not compile

Granted, SomeList is pretty useless as is. As often, such an existential type would only be really useful as part of a bigger type.

Deepen

Thank you but sorry, I still can't understand. Why X.x is conform to v.T forSome { val v : { type T }; }? Does X.x has the member type T? But from type T = String; val x:T="hello", I can't see x has {type T}. – Harkness

It is not that X.x has the member type T, but rather that it is of type T. Here X (an object or in other words a value) corresponds to v in our type dependent type. In addition X.x has the type X.T. So it is clearly true that X.x satisfies the type v.T, given that X is definitely some value. – Escrow

Self-correction: I meant "path dependent type" rather than "type dependent type" – Escrow