This page is no longer maintained — Please continue to the home page at www.scala-lang.org

How do I interpret this existential type?

9 replies
Jason Zaugg
Joined: 2009-05-18,
User offline. Last seen 38 weeks 5 days ago.
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

adriaanm
Joined: 2010-02-08,
User offline. Last seen 31 weeks 4 days ago.
Re: How do I interpret this existential type?
Hi Jason,
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.
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
Jason Zaugg
Joined: 2009-05-18,
User offline. Last seen 38 weeks 5 days ago.
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:
Hi Jason,
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.
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}

How about `p.x.T`, where `x` is a stable value member of `p`. ?
-jason
milessabin
Joined: 2008-08-11,
User offline. Last seen 33 weeks 3 days ago.
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

Jason Zaugg
Joined: 2009-05-18,
User offline. Last seen 38 weeks 5 days ago.
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:
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
 
adriaanm
Joined: 2010-02-08,
User offline. Last seen 31 weeks 4 days ago.
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
milessabin
Joined: 2008-08-11,
User offline. Last seen 33 weeks 3 days ago.
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

adriaanm
Joined: 2010-02-08,
User offline. Last seen 31 weeks 4 days ago.
Re: How do I interpret this existential type?
 {p -> P'}U
meaning

 U with P' substituted for p throughout?
yes, sorry, should have clarified that 
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
milessabin
Joined: 2008-08-11,
User offline. Last seen 33 weeks 3 days ago.
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

adriaanm
Joined: 2010-02-08,
User offline. Last seen 31 weeks 4 days ago.
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  (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

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland