- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers

# How do I interpret this existential type?

Tue, 2011-10-18, 07:26

While trying to fit a scalaz.Monad generically to scala.util.combinator.Parser#Parsers, I came across a type I don't understand.

Here's a standalone version of the code:

https://gist.github.com/1293796

The type in question is the return type of `parserM`. (I copied the inferred type into the program.)

def parserM[P <: Parsers](parsers: P) : M[_1.parsers.Parser] forSome { val _1: ParsersW[P] } = new ParsersW[P](parsers).m

Quoth the spec:

3.2.10 Existential Types

An existential type T forSome { Q; val x: S;Q′ } is treated as a shorthand for the type T′ forSome { Q; type t <: S with Singleton; Q′ }, where t is a fresh type name and T′ results from T by replacing every occurrence of x.type with t.

3.2.3 Type Designators

A qualified type designator has the form p.t where p is a path (§3.1) and t is a type name. Such a type designator is equivalent to the type projection p.type#t.

So my first question: How can I expand the existential type to one of the form `... forSome { type t <: ... }`? In this type, `_1` is used as a qualifier in a path.

-jason

Here's a standalone version of the code:

https://gist.github.com/1293796

The type in question is the return type of `parserM`. (I copied the inferred type into the program.)

def parserM[P <: Parsers](parsers: P) : M[_1.parsers.Parser] forSome { val _1: ParsersW[P] } = new ParsersW[P](parsers).m

Quoth the spec:

3.2.10 Existential Types

An existential type T forSome { Q; val x: S;Q′ } is treated as a shorthand for the type T′ forSome { Q; type t <: S with Singleton; Q′ }, where t is a fresh type name and T′ results from T by replacing every occurrence of x.type with t.

3.2.3 Type Designators

A qualified type designator has the form p.t where p is a path (§3.1) and t is a type name. Such a type designator is equivalent to the type projection p.type#t.

So my first question: How can I expand the existential type to one of the form `... forSome { type t <: ... }`? In this type, `_1` is used as a qualifier in a path.

-jason

Tue, 2011-10-18, 08:47

#2
Re: How do I interpret this existential type?

On Tue, Oct 18, 2011 at 9:35 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:

How about `p.x.T`, where `x` is a stable value member of `p`. ?

-jason

Hi Jason,Quoth the spec:Since p.T is syntactic sugar for p.type#T, to abstract over a path, it suffices to abstract over the corresponding singleton type.

3.2.10 Existential Types

An existential type T forSome { Q; val x: S;Q′ } is treated as a shorthand for the type T′ forSome { Q; type t <: S with Singleton; Q′ }, where t is a fresh type name and T′ results from T by replacing every occurrence of x.type with t.

3.2.3 Type Designators

A qualified type designator has the form p.t where p is a path (§3.1) and t is a type name. Such a type designator is equivalent to the type projection p.type#t.

So my first question: How can I expand the existential type to one of the form `... forSome { type t <: ... }`? In this type, `_1` is used as a qualifier in a path.

To indicate the type is a stable type (otherwise you may not select an abstract type on it), the Singleton marker is used.

Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S with Singleton}

How about `p.x.T`, where `x` is a stable value member of `p`. ?

-jason

Tue, 2011-10-18, 09:47

#3
Re: How do I interpret this existential type?

On Tue, Oct 18, 2011 at 8:35 AM, Adriaan Moors wrote:

> Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S with

> Singleton}

While we're in this area, would it be correct to say that,

X#Y

is equivalent to the (hypothetical),

x.Y forAll { val x : X }

The subtype relations seem to validate that,

scala> trait X { trait Y }

defined trait X

scala> val x1 = new X {}

x1: java.lang.Object with X = $anon$1@7d316b06

scala> val x2 = new X {}

x2: java.lang.Object with X = $anon$1@a1ab167

scala> implicitly[x1.Y <:< X#Y]

res0: <:<[x1.Y,X#Y] =

scala> implicitly[x2.Y <:< X#Y]

res1: <:<[x2.Y,X#Y] =

scala> implicitly[(x.Y forSome { val x : X }) <:< X#Y]

res2: <:<[x.Y forSome { val x: X },X#Y] =

Cheers,

Miles

Tue, 2011-10-18, 10:07

#4
Re: How do I interpret this existential type?

On Tue, Oct 18, 2011 at 10:42 AM, Miles Sabin <miles [at] milessabin [dot] com> wrote:

Thanks for formulating part two of my question so clearly!

-jason

On Tue, Oct 18, 2011 at 8:35 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:

> Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S with

> Singleton}

While we're in this area, would it be correct to say that,

X#Y

is equivalent to the (hypothetical),

x.Y forAll { val x : X }

The subtype relations seem to validate that,

Thanks for formulating part two of my question so clearly!

-jason

Tue, 2011-10-18, 12:07

#5
Re: How do I interpret this existential type?

Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S with Singleton}

How about `p.x.T`, where `x` is a stable value member of `p`. ?

so, we're looking at p.x.T forSome {val p: S}this implies S declares a member x with some type U if U depends on p, encode it as U' = {p -> P'}U forSome {type P' <: S with Singleton}

thus, P#T forSome {type P <: U' with Singleton} can be used as the encoding

adriaan

ps: I'm still thinking about the (forall x: S)#T == S#T equality, but the set interpretation {x | x :S } == S makes sense

Tue, 2011-10-18, 12:17

#6
Re: How do I interpret this existential type?

On Tue, Oct 18, 2011 at 11:57 AM, Adriaan Moors wrote:

>>> Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S

>>> with Singleton}

>>

>> How about `p.x.T`, where `x` is a stable value member of `p`. ?

>

> so, we're looking at p.x.T forSome {val p: S}

> this implies S declares a member x with some type U

> if U depends on p, encode it as U' = {p -> P'}U forSome {type P' <: S with

> Singleton}

{p -> P'}U

meaning

U with P' substituted for p throughout?

> thus, P#T forSome {type P <: U' with Singleton} can be used as the encoding

> adriaan

> ps: I'm still thinking about the (forall x: S)#T == S#T equality, but the

> set interpretation {x | x :S } == S makes sense

Is there room in DOT for an explicit forAll { type/val } alongside forSome?

Cheers,

Miles

Tue, 2011-10-18, 12:47

#7
Re: How do I interpret this existential type?

{p -> P'}Uyes, sorry, should have clarified that

meaning

U with P' substituted for p throughout?

Is there room in DOT for an explicit forAll { type/val } alongside forSome?currently we don't have either, it's all abstract type members (their relation to forSome and forAll is interesting in itself, something I should get to the bottom of)

cheersadriaan

Tue, 2011-10-18, 13:07

#8
Re: How do I interpret this existential type?

On Tue, Oct 18, 2011 at 12:45 PM, Adriaan Moors wrote:

>> Is there room in DOT for an explicit forAll { type/val } alongside

>> forSome?

>

> currently we don't have either, it's all abstract type members (their

> relation to forSome and forAll is interesting in itself, something I should

> get to the bottom of)

What's your abstract type member encoding of forAll { type/val}?

Cheers,

Miles

Tue, 2011-10-18, 13:17

#9
Re: How do I interpret this existential type?

[let's move this to internals]

I think of it this way:

- an object with a type member and a value member whose type contains the type member is like an existential package

- a trait with an abstract type member and a value member whose type contains the type member corresponds to universal polymorphism

- a trait with an abstract type member and a type member whose RHS contains the type member is like a universally quantified type

I discuss this in more detail in this paper:

cheersadriaan

On Tue, Oct 18, 2011 at 2:00 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:

I think of it this way:

- an object with a type member and a value member whose type contains the type member is like an existential package

*(value existentially abstracting over a type)*- a trait with an abstract type member and a value member whose type contains the type member corresponds to universal polymorphism

*(value universally abstracting over a type)*- it's not a value (to instantiate the trait, the abstract type member needs to be made concrete), but it can be supplied any concrete type (using refinement), which makes it like universal polymorphism- a trait with an abstract type member and a type member whose RHS contains the type member is like a universally quantified type

*(type universally abstracting over a type)*I discuss this in more detail in this paper:

*Safe*Type-level*Abstraction*in*Scala*cheersadriaan

On Tue, Oct 18, 2011 at 2:00 PM, Miles Sabin <miles [at] milessabin [dot] com> wrote:

On Tue, Oct 18, 2011 at 12:45 PM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:

>> Is there room in DOT for an explicit forAll { type/val } alongside

>> forSome?

>

> currently we don't have either, it's all abstract type members (their

> relation to forSome and forAll is interesting in itself, something I should

> get to the bottom of)

What's your abstract type member encoding of forAll { type/val}?

Cheers,

Miles

--

Miles Sabin

tel: +44 7813 944 528

gtalk: miles [at] milessabin [dot] com

skype: milessabin

http://www.chuusai.com/

http://twitter.com/milessabin

Since p.T is syntactic sugar for p.type#T, to abstract over a path, it suffices to abstract over the corresponding singleton type.

To indicate the type is a stable type (otherwise you may not select an abstract type on it), the Singleton marker is used.

Thus, p.T forSome {val p: S} is encoded as P#T forSome {type P <: S with Singleton}

Quoth the REPL:

scala> trait X { type T }defined trait X

scala> val x: X = nullx: X = null

scala> lazy val y: (p#T forSome {type p <: X with Singleton}) = (error(""): x.T)warning: there were 1 deprecation warnings; re-run with -deprecation for detailsy: p#T forSome { type p <: X with Singleton } = <lazy>

hth!adriaan