- 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.moors@epfl.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@milessabin.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.moors@epfl.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 (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@milessabin.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@milessabin.com> wrote:
On Tue, Oct 18, 2011 at 12:45 PM, Adriaan Moors <adriaan.moors@epfl.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@milessabin.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