Union types

[Sciss]

hi,

I wanted to put an idea in the round that came up in a comment of a stackoverflow entry ( http://stackoverflow.com/questions/5645700/whats-the-difference-between-scala-and-red-hats-ceylon-language/5646305#comment-6468943 ):

We have a sort of type intersection in the form of `A with B`, so that in

def perform( x: A with B ) { ... }

we can assume the functionality of both types `A` and `B`. Wouldn't it be a very interesting idea to explore the possibility of a type *union*, like

def perform( x: A or B ) { ... }

so that the main body of that method can safely invoke anything on `x` which is common between types `A` and `B`. It would then be possible to do an exhaustive match like this:

def perform( x: A or B ) {
...
x match {
case a: A => ...
case b: B => ...
}
}

and that way in some distant version of Scala one would overcome the need to have method overloading and multiple constructors.

Although we will hopefully in this distant version have fully supported runtime generics, this could also solve the case of

def perform( a: List[ A ]) { ... }
def perform( b: List[ B ]) { ... }

under the condition that erasure is still happening, because then you could do

def perform( a: List[ A or B ]) { ... }

i know there is `Either` but that has many disadvantages against this union types -- it is extra verbose, cannot handle view bounds on its type parameters without much extra bloat of implicits work, and it cannot handle more than two types.

best, -sciss-

[Paul Phillips]

On 4/15/11 9:00 AM, Sciss wrote:
> we can assume the functionality of both types `A` and `B`. Wouldn't it be a very interesting idea to explore the possibility of a type *union*, like
>
> def perform( x: A or B ) { ... }

https://lampsvn.epfl.ch/trac/scala/ticket/3749

"We plan to address this issue in future versions of Scala by
introducing union types, so that the approximation of the least upper
bound you see here could be denoted directly (and precisely) as
java.lang.Double or java.lang.Long. [...]

First, we need to work out the nitty gritty details of the theory, though."

[Chris Twiner]

How often would you use that where the more general structural types wouldn't work?

[Sciss]

Hooray !!!

`List(1.0, 2)` by the way is a good example of where this could be extremely useful, too.

best, -sciss-

[Sciss]

note that A and B do not necessarily have any substantial common interface! the pattern matching example below is exactly where union types would fit in and structural types clearly not.

[Jim McBeath]

Mitch Blevins implements this in his blog entry "Stuttering Or":
http://cleverlytitled.blogspot.com/2009/03/so-i-read-both-jim-mcbeath-and-michids.html

--
Jim

On Fri, Apr 15, 2011 at 05:00:30PM +0100, Sciss wrote:
> Date: Fri, 15 Apr 2011 17:00:30 +0100
> From: Sciss <con...@sciss.de>
> To: scala-l...@googlegroups.com
> Subject: [scala-language] Union types

[Sciss]

very neat!

the only downsides are that the compiler cannot check the matches for exhaustiveness, that i cannot use common interface between the types, and that you need to import half a dozen imports (that always makes me slightly depressed and i think this is an example of why people keep having the impression that scala is too complicated).

best, -sciss-

[Randall R Schulz]

On Friday April 15 2011, Paul Phillips wrote:
> On 4/15/11 9:00 AM, Sciss wrote:
> > we can assume the functionality of both types `A` and `B`. Wouldn't
> > it be a very interesting idea to explore the possibility of a type
> > *union*, like
> >
> > def perform( x: A or B ) { ... }
>
> https://lampsvn.epfl.ch/trac/scala/ticket/3749
>
> "We plan to address this issue in future versions of Scala by
> introducing union types, so that the approximation of the least upper
> bound you see here could be denoted directly (and precisely) as
> java.lang.Double or java.lang.Long. [...]

The LUB of two arbitrary types will in general subsume many types that
would not otherwise be compatible with either of the two original
types, so this does not seem to me like a proper interpretation of the
union of two types.

> First, we need to work out the nitty gritty details of the theory,
> though."

Randall Schulz

[Vlad Patryshev]

Thanks; curious, familiar technique: building colimits in toposes (Mikkelsen, Pare)

[Ben Hutchison]

FWIW, I was wanting the same capability myself last week, to address
the difficulty of overloading methods by parameter type, when the
types are parametrized.

I often find myself wanting an API to respond to several related
parametrized types. Some common examples:

aMethod(t: T)
aMethod(optT: Option[T])
aMethod(ts: Seq[T])

It would be nice to support this without requiring implicit conversions.

-Ben

[Alex Repain]

2011/4/18 Ben Hutchison <b...@playscapegames.com>

FWIW, I was wanting the same capability myself last week, to address
the difficulty of overloading methods by parameter type, when the
types are parametrized.

I often find myself wanting an API to respond to several related
parametrized types. Some common examples:

aMethod(t: T)
aMethod(optT: Option[T])
aMethod(ts: Seq[T])

It would be nice to support this without requiring implicit conversions.

Not exactly the same problem. What you want is syntactic sugar to  port some methods to container types, but that is not exactly what union types would create. Union types would allow you to do

aMethod(a: A or Option[A]) : B

which is somehow equivalent to what you're looking for. This example can clearly be desugared to :

aMethod(a: A) : B
aMethod(Option[A]) : B

I personnally think that implicits are the right way to go for that case.
Union types would also allow you to do :

anotherMethod(abs: Seq[A or B]) : C

or even stranger :

another method(a: A) : B or C

which means that the Seq requested as parameter would contain potentially A instances and B instances at same time. The problem is more complex and as Martin said, I think the integration of such thing in Scala has to be studied first, to check it doesn't break the coherence of the type system.

[Shelby]

Re: Union (i.e. disjunction) type

https://issues.scala-lang.org/browse/SUGGEST-22

Scala has the compound (i.e. conjunction) type by employing `with`,
but it does not have a union (i.e. disjunction) type.

I hope I have successfully demonstrated how to simulate a nearly first-
class union type:

http://groups.google.com/group/shapeless-dev/browse_thread/thread/01f26830027f3517/7c1006ac6e638044?#7c1006ac6e638044

And the negation of the disjunction:

http://www.chuusai.com/2011/06/09/scala-union-types-curry-howard/#comment-1160

I have filed today two bug reports that hinder use of that simulated
union type.

Beyond that, I am pondering if Scala is going to lose significant
competitive ground w.r.t. to Ceylon if it doesn't add a completely
first-class union type asap. And go beyond Ceylon by adding some way
to extend the disjunction (e.g. for heterogeneous types) as I
demonstrated at link above for negation.

Afaics it is necessary for supporting heterogeneous collections type-
safely without resorting to the (probably unbearable for novices, and
more "Scala is difficult to read" accusations) complexity of the
experimental metascala.

I have been thinking that first-class intersection types are very
important, both for the [reasons Ceylon has them][8], and because
instead of [subsuming][9] to `Any` which means unboxing with a `match`
on expected types can generate a runtime error, the unboxing of a
([heterogeneous collection][10] containing a) disjunction can be type
checked. Unions are more straightforward than the [complexity of using]
[11] the experimental [HList][12] of [metascala][13] for heterogeneous
collections.

[8]: http://ceylon-lang.org/documentation/1.0/faq/language-design/#optional_types
[9]: http://stackoverflow.com/questions/8360413/selectively-disable-subsumption-in-scala-correctly-type-list-contains
[10]: http://lambda-the-ultimate.org/node/4394#comment-68110
[11]: http://jnordenberg.blogspot.com/2008/08/hlist-in-scala.html
[12]: http://stackoverflow.com/questions/185972/arrays-in-scala/205729#205729
[13]: http://stackoverflow.com/questions/3508077/does-scala-have-type-disjunction-union-types/3508357#3508357

P.S. There is a duplicate syntax-highlighted version buried nearer to
the bottom of the following stackoverflow answer:

http://stackoverflow.com/questions/3508077/does-scala-have-type-disjunction-union-types/7460312#7460312

P.S.S. Consider reading the Ceylon language design FAQ[8], as it
appears to me to be significant substance in their effort, although I
am not yet clear on what corner cases may be lurking in their attempts
to simplify and make code more amenable to the mainsteam.

[Shelby]

http://ceylon-lang.org/documentation/1.0/faq/#when_will_it_be_ready
http://ceylon-lang.org/documentation/1.0/introduction/#principal_typing_union_types_and_intersection_types
http://ceylon-lang.org/documentation/1.0/faq/language-design/#optional_types

[Adriaan Moors]

Hi Shelby,

We're working on the next generation of Scala's type system, which will include union types.

These things are extremely hard to get right (a type system with union&intersection types and path-dependent abstract types with lower- and upper-bounds has not been studied formally yet afaik, and it turns out to be a particularly potent&challenging mix).

We'll take all the time we need to convince ourselves that the end result is both sound and usable.

cheers

adriaan

[Sciss]

that's great news adriaan! you can do union types "top-down" in the design phase of a library with super-traits, but it would be really phantastic to be able to construct them "bottom-up" / "ex-post" with a union operator. it would add one of the things that are great about haskell's conciseness. if it takes till scala 3, no problem, i keep the thumbs pressed that it is possible to implement them!

best, .h.h.

[Shelby]

Hi Adiaan, it is inspiring to read that union types are under
consideration.

If my (twist on Miles Sabin's) implementation above is correct,
apparently the disjunction is the conjunction with subtyping in the
contravariant direction, with each item in the conjunction subtyped in
the contravariant direction. That appears to be a statement of De
Morgan's laws where negation is subtyping in the contravariant
direction.

This makes sense to me, because the set of all supertypes includes
every type (via common supertype `Any`) not in the type being negated.

[Rex Kerr]

On Tue, Mar 6, 2012 at 4:52 PM, Shelby <she...@coolpage.com> wrote:

If my (twist on Miles Sabin's) implementation above is correct,
apparently the disjunction is the conjunction with subtyping in the
contravariant direction, with each item in the conjunction subtyped in
the contravariant direction. That appears to be a statement of De
Morgan's laws where negation is subtyping in the contravariant
direction.

Yes, that's correct--I believe that I had an exchange with Miles regarding exactly that in the comments on his union types post.

Consequently, my version of his implementation of union types looks like so:
  // Type unions using contravariance
  // Usage: def f[T: Union[Int, String]#Check](t: T) = t match { case i: Int => i; case s: String => s.length }
  trait Contra[-A] {}
  type Union[A,B] = { type Check[Z] = Contra[Contra[Z]] <:< Contra[Contra[A] with Contra[B]] }

--Rex

[Adriaan Moors]

these encoding are neat, but the union types we're working on go beyond what you can do "in user space"

assume membersOf(S) = MS, membersOf(T) = MT

then, membersOf(S \/ T) = MS intersect MT,  (not a typo -- the members of a union type is the intersection of the sets of members of its constituents)

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

conversely, membersOf(S /\ T) = MS union MT (where, again, overlapping members have their types intersected)

(note that this is a work in progress, so I won't speculate on when/how/whether/... this ends up in a scalac near you)

[Miles Sabin]

On Wed, Mar 7, 2012 at 1:11 PM, Adriaan Moors <adriaa...@gmail.com> wrote:
> these encoding are neat, but the union types we're working on go beyond what
> you can do "in user space"
>
> assume membersOf(S) = MS, membersOf(T) = MT
>
> then, membersOf(S \/ T) = MS intersect MT,  (not a typo -- the members of a
> union type is the intersection of the sets of members of its constituents)
>     where the intersection is computed by including only synonymous members
> from both MS and MT,
>     say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/
> Tt of the intersected set
>
> conversely, membersOf(S /\ T) = MS union MT (where, again, overlapping
> members have their types intersected)
>
> (note that this is a work in progress, so I won't speculate on
> when/how/whether/... this ends up in a scalac near you)

Deep mixin composition redux? Like it :-)

Cheers,

Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
g+: http://www.milessabin.com
http://twitter.com/milessabin
http://www.chuusai.com/

[Rex Kerr]

On Wed, Mar 7, 2012 at 8:11 AM, Adriaan Moors <adriaa...@gmail.com> wrote:

these encoding are neat, but the union types we're working on go beyond what you can do "in user space"

assume membersOf(S) = MS, membersOf(T) = MT

then, membersOf(S \/ T) = MS intersect MT,  (not a typo -- the members of a union type is the intersection of the sets of members of its constituents)

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

Wait, what?  So if I have bools and strings and union them with ints and strings, the members of the union type of the two of those are only strings?!  I must be misunderstanding what you're saying, because that doesn't seem like the idea of "union" to me.

I do like the general idea, if I understand what the general idea is, but the details are puzzling.  Perhaps I don't understand what you mean by "membersOf", since your "intersection" looks to me like the product of the sets.

I'm sure it will all make sense when it is written up formally, but if you have time to clarify the teaser, I'd appreciate it.

  --Rex

[Jan Vanek]

Intuition goes like follows: Imagine you have type E = S v T. If you have val e: E, then e's real type can be either S or T but you don't know which, you only know it is E, so the only members you can safely access on x are those which are in both S and in T, i.e. an intersection. And vice-versa with E = S & T, you can safely access all members in S and also in T, i.e. a union.

Regards,

Jan

[Alex Repain]

2012/3/7 Adriaan Moors <adriaa...@gmail.com>

these encoding are neat, but the union types we're working on go beyond what you can do "in user space"

assume membersOf(S) = MS, membersOf(T) = MT

then, membersOf(S \/ T) = MS intersect MT,  (not a typo -- the members of a union type is the intersection of the sets of members of its constituents)

According to that definition, Int V String  is pretty much Nothing, which is incredibly not useful... 

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

How are we supposed to get these two values with conflicting names together in the first place ? I think there is something wrong (or insanely genious ?) in your definition of Union types ...

 

conversely, membersOf(S /\ T) = MS union MT (where, again, overlapping members have their types intersected)
 

This is not at all the same union (resp. intersection) types as Miles' . If the names are that ambiguous (a quick internet check got me "untagged union types", "union types" and other different concepts), we probably shouldn't be using them...

[Sciss]

aren't union types supposed to do what the pipe operator does in haskell?

data Ordering = EQ | LT | GT
data Tree a = Leaf a | Branch (Tree a) (Tree a) deriving Eq
data Day = Sunday | Monday | Tuesday | Wednesday | Thursday | Friday | Saturday deriving (Enum)

etc.

(http://www.haskell.org/tutorial/stdclasses.html)

that would be for the main purpose of having them altogether. i, too, think that intersection between their members doesn't make sense... we need to be able to express Saturday | Sunday without resorting to:

sealed trait Day
sealed trait MondayOrTuesday extends Day
sealed trait MondayOrWednesday extends Day
...
case object Monday extends MondayOrTuesday with MondayOrWednesday with ...

right?

best, ..hh..

[Alex Repain]

2012/3/7 Jan Vanek <j3v...@googlemail.com>

Intuition goes like follows: Imagine you have type E = S v T. If you have val e: E, then e's real type can be either S or T but you don't know which, you only know it is E, so the only members you can safely access on x are those which are in both S and in T, i.e. an intersection. And vice-versa with E = S & T, you can safely access all members in S and also in T, i.e. a union.

Right, but you're talking about members, while ... oooh wayddaminute. "members" as for "fields"... And not as for "instances" ... Now I'm unconfused.

[Klaus Havelund]

This might already have been discussed. It concerns the way tagged
union types are
written in Scala. For example a standard Tree of integers:

trait Tree
case class Leaf(x:Int) extends Tree
case class Branch(left:Tree, x:Int, right:Tree) extends Tree

(ignoring that it has to be sealed to be protected from new
alternatives to be added).

We can then do pattern matching over trees as in:

def sum(tree: Tree): Int =
  tree match {
    case Leaf(x) => x
    case Branch(l,x, r) => sum(l) + x + sum(r)
  }

In other functional programming (FP) languages we would define the
type along the following lines
(syntax varies from language to language of course, but the essence is this):

datatype Tree = Leaf(x:Int) | Branch(left: Int, right: Int)

The Scala way of repeating additional keywords:

case class ... extends ....

can be somewhat annoying. It would be nice with the shorter form.

Now, there is an argument for the longer form since it allows for
adding methods etc to the alternatives,
which the standard FP style does not. One could then consider an
alternative such as:

datatype Tree {
  case class Leaf(x:Int)
  case class Branch(left:Tree,x:Int, right:Tree)
}

which would for example allow us to add a toString method to each alternative:

datatype Tree {
  case class Leaf(x:Int) {
    def toString: String = ...
  }

  case class Branch(left:Tree,x:Int, right:Tree) {
    def toString: String = ...
  }
}

[Tom Switzer]

This sounds great. I just assumed a union type would immediately devolve to a pattern match, replacing overloading. If we're allowed access to the members though, how is List[Int] V List[String] handled? What does .head return? Int V String? Or would it not be accessible because the return types are different?

[Jesper Nordenberg]

What would be the use case for this feature? I can see the use of B <: A
& C <: A => (B | C) <: A, but this feature looks more like structural
typing.

/Jesper Nordenberg

[Alex Repain]

2012/3/7 Jesper Nordenberg <mega...@yahoo.com>

What would be the use case for this feature? I can see the use of B <: A & C <: A => (B | C) <: A, but this feature looks more like structural typing.

It is about that, at least partly. Union types are a way to reduce code duplication for unrelated types that yet have structural similarities. The way I see it, one of the straightforward use will be with the types under AnyVal, since they are loosely related in the type system, but structurally very close.

Also, heterogeneous collections ?

[Jan Vanek]

On 07.03.2012 19:03, Tom Switzer wrote:

allowed access to the members though, how is List[Int] V List[String] handled? What does .head return? Int V String? Or would it

Yes. Int V String. As Adriaan wrote:

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

I don't know but wildly speculate that methods with parameters are synonymous only when they have identical parameter types. So if there is:

class T { def f(i: Int, j: Int) {} }
class S { def f(s: String, t: String) {} }

in T v S there is no f. This would also mean that if there is var m: Ts and var m: Tt then in the T v S there is only def m: Ts V Tt (getter), but no setter.

Regards,
Jan

[Kevin Wright]

The whole idea is really quite clever.  Imagine you have:

trait Bippy {

  def bippyMethod(x: String): Int

  def takeAction(arg: TwoWheeledVehicle): Error

}

trait Wibble {

  def wibbleMethod(x: Int): String

  def takeAction(arg: PoweredVehicle): Exception

}

The union would then contain the intersection of the members (methods/properties).  The fun part is how the parameters and return types of these members also get unified:

trait Bippy or Wibble {

  def takeAction(arg: TwoWheeledVehicle with PoweredVehicle): Throwable

}

If you had an instance of such a thing, you could of couse pattern match it.  You could also invoke the takeAction method, supplying an instance of Motorbike and receiving a Throwable in response.

Now imagine it used with primitives, guaranteeing some basic arithmetic operations to be available regardless of exactly what type you had.  It's an approach that would make a nice counterpoint to specialisation, and could make it easy to avoid a lot of boxing/unboxing performance issues depending on the underlying implementation.

For more info, there's a draft paper here http://lampwww.epfl.ch/teaching/foundations_of_software/docs/dependent_types.pdf

You can also google against the magic words "dependent object types" for other papers and to get a feel for how these ideas evolved.

[Shelby]

Adriaan's idea appears to be more complete from a type theoretic
perspective.

On Mar 8, 4:50 am, Jan Vanek <j3va...@googlemail.com> wrote:
> in T v S there is no f. This would also mean that if there is var m: Ts
> and var m: Tt then in the T v S there is only def m: Ts V Tt (getter),
> but no setter.

So Adriaan's idea extends the union to method members, so that it is
possible to delay the pattern matching destructuring.

class T { def m: Int }
class S { def m: String }

def f(u: T V S): Int V String = u match {
case x: T => x.m
case x: S => x.m
}

Adriaan's idea additionally allows (as well as I assume the above).

def f(u: T V S): Int V String = u.m

On Mar 8, 12:14 am, Alex Repain <alex.rep...@gmail.com> wrote:
> According to that definition, Int V String is pretty much Nothing, which
> is incredibly not useful...

[...]

> This is not at all the same union (resp. intersection) types as Miles'

I assume Int V String can still be pattern match destructured into an
Int or a String. Afaics, Adriaan's idea adds functionality, but also
includes the unions that Miles, Rex, and I were expressing.

Adriaan I am contemplating there may be a relationship with the
members and De
Morgan's laws.

[Shelby]

On Mar 8, 5:33 am, Kevin Wright <kev.lee.wri...@gmail.com> wrote:
> For more info, there's a draft paper here
> http://lampwww.epfl.ch/teaching/foundations_of_software/docs/dependent_types.pdf

So to bring mixin inheritance into conformance with the model, the
type of duplicate inherited members would be a union of the
duplicates? Linearization wouldn't occur and order within the
intersection list wouldn't matter?

Then we wouldn't need a separate model for multiple inheritance?

[Jan Vanek]

Hi Kevin,

On 07.03.2012 22:33, Kevin Wright wrote:

The whole idea is really quite clever.  Imagine you have:

trait Bippy {

  def bippyMethod(x: String): Int

  def takeAction(arg: TwoWheeledVehicle): Error

}

trait Wibble {

  def wibbleMethod(x: Int): String

  def takeAction(arg: PoweredVehicle): Exception

}

The union would then contain the intersection of the members (methods/properties).  The fun part is how the parameters and return types of these members also get unified:

trait Bippy or Wibble {

  def takeAction(arg: TwoWheeledVehicle with PoweredVehicle): Throwable

}

If you had an instance of such a thing, you could of couse pattern match it.  You could also invoke the takeAction method, supplying an instance of Motorbike and receiving a Throwable in response.

Of course the further it gets, the better. What discouraged me is following. Say we have

class T { def foo(a: Int, b: Int) {} }
class S { def foo(a: String, b: String) {} }

then it is imaginable to have T or S with

def foo[(a: Int, b: Int) & (a: String, b: String)]

which, according to Adriaan's rules (if we take those tuples as T and S in his example) could be interpreted as:

def foo(a: Int & String, b: Int & String)

and it is all OK. The & sort of propagated into the tuple.

However, if you want to be symmetric and have T with S, this would have

def foo[(a: Int, b: Int) v (a: String, b: String)]

Here, you can't propagate the v into the tuple, because you'd have

def foo(a: Int v String, b: Int v String)

which would allow you to call the foo e.g. like foo(1, "a"). This is not correct, you can only call it with 2 Ints, or with 2 Strings. I don't have an answer for this asymetricity. But perhaps there is one, or, better, it doesn't arise at all.

Now imagine it used with primitives, guaranteeing some basic arithmetic operations to be available regardless of exactly what type you had.  It's an approach that would make a nice counterpoint to specialisation, and could make it easy to avoid a lot of boxing/unboxing performance issues depending on the underlying implementation.

For more info, there's a draft paper here http://lampwww.epfl.ch/teaching/foundations_of_software/docs/dependent_types.pdf

You can also google against the magic words "dependent object types" for other papers and to get a feel for how these ideas evolved.

Thanks a lot for the link, will look at it. I need more lives...

Regards,
Jan

[Shelby]

On Mar 8, 5:59 am, Jan Vanek <j3va...@googlemail.com> wrote:
> then it is imaginable to have T or S with

Do you mean T V S?

> def foo[(a: Int, b: Int) & (a: String, b: String)]

Then how do you get this, if only synonymous members are allowed?

Wouldn't that be instead?

def foo[(a: Int, b: Int) V (a: String, b: String)]

[Alex Repain]

2012/3/7 Jan Vanek <j3v...@googlemail.com>

In the case of T with S (intersection type, but really "with" fits in better), the fields of T with S are the union of the fields of T and the fields of S. However, if two methods with same name but different signatures are to be mixed in, we don't have to do anything. We have the two methods and that's it, no need to get down to the method arguments' level :). We get both methods without losing in type restrictions (in your case, without getting the parasitic method foo(a: Int, b: String), for instance).

Note that if the type signatures are conflicting, the current mixin axiom is to use the "last" definition in composition order (you may wanna check SLS or some other source before taking my word for it). In that sense, the current "with" statement is not strictly an intersection type, or rather, it's an intersection type with an additional paradigm.

[Kevin Wright]

In the case of "T with S", this is true.  It's the least upper bound of all types that inherit both T and S, so of course both signatures of foo are in scope.  We already have this and use it extensively with mixins.

Another valid interpretation is a single implementation of foo, defined as:

def foo[A <: Int or String](a: A, b: A)

The extra type param is necessary, because the alternative:

def Foo(a: Int or String, b: Int or String)

would permit the two arguments to be of different types, which breaks the contract of both types being unified!

So why favour the unified method as opposed to overloads?

For one thing, it's arguably more correct and consistent with the overall "dependent object types" proposal.  e.g. such methods are still semantically valid even in cases where overloaded methods would generate a compiler warning about erasure (imagine mixing in two version of the same trait, but with different type params).

It also becomes a whole lot easier to reason about once you start considering the union of two intersection types, or the intersection of two union types (plus it's easier for the compiler to optimise)

Note that if the type signatures are conflicting, the current mixin axiom is to use the "last" definition in composition order (you may wanna check SLS or some other source before taking my word for it). In that sense, the current "with" statement is not strictly an intersection type, or rather, it's an intersection type with an additional paradigm.

 

I believe that discrepancy was part of the reason why this proposal was devised in the first place :)

Now imagine it used with primitives, guaranteeing some basic arithmetic operations to be available regardless of exactly what type you had.  It's an approach that would make a nice counterpoint to specialisation, and could make it easy to avoid a lot of boxing/unboxing performance issues depending on the underlying implementation.

For more info, there's a draft paper here http://lampwww.epfl.ch/teaching/foundations_of_software/docs/dependent_types.pdf

You can also google against the magic words "dependent object types" for other papers and to get a feel for how these ideas evolved.

Thanks a lot for the link, will look at it. I need more lives...

Regards,
Jan

On 7 March 2012 20:50, Jan Vanek <j3v...@googlemail.com> wrote:

On 07.03.2012 19:03, Tom Switzer wrote:

allowed access to the members though, how is List[Int] V List[String] handled? What does .head return? Int V String? Or would it

Yes. Int V String. As Adriaan wrote:

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

I don't know but wildly speculate that methods with parameters are synonymous only when they have identical parameter types. So if there is:

class T { def f(i: Int, j: Int) {} }
class S { def f(s: String, t: String) {} }

in T v S there is no f. This would also mean that if there is var m: Ts and var m: Tt then in the T v S there is only def m: Ts V Tt (getter), but no setter.

Regards,
Jan

--
Kevin Wright
mail: kevin....@scalatechnology.com
gtalk / msn : kev.lee...@gmail.com

quora: http://www.quora.com/Kevin-Wright

google+: http://gplus.to/thecoda

twitter: @thecoda

vibe / skype: kev.lee.wright

steam: kev_lee_wright

"My point today is that, if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent": the current conventional wisdom is so foolish as to book that count on the wrong side of the ledger" ~ Dijkstra

[Shelby]

On Mar 8, 7:30 am, Kevin Wright <kev.lee.wri...@gmail.com> wrote:

> On 7 March 2012 22:53, Alex Repain <alex.rep...@gmail.com> wrote:
> Note that if the type signatures are conflicting, the current mixin axiom
>
> > is to use the "last" definition in composition order (you may wanna check
> > SLS or some other source before taking my word for it). In that sense, the
> > current "with" statement is not strictly an intersection type, or rather,
> > it's an intersection type with an additional paradigm.
>
> I believe that discrepancy was part of the reason why this proposal was
> devised in the first place :)

That is one of the points I was also making in my prior reply to you.
Additionally I need to go review all the reasons why we need
linearization of mixins, because at least that requirement of linear
order disappears.

I assume such a change could break existing code. I concur that
arguably the significant benefit appears to be the type system becomes
more complete (e.g. no unityping to Any on subsumption to greatest
lower bounds, i.e. not abandoning static typing: http://kwout.com/quote/y6x47gyj
) and thus sound, easier to reason about, unifying concepts which
enables optimizations, etc..

On Mar 8, 5:36 am, Shelby <she...@coolpage.com> wrote:
> Adriaan I am contemplating there may be a relationship with the
> members and De Morgan's laws.

Before posting to this thread, I had some use cases that indicated
that union type was necessary to make the type system more complete
(and thus very important), and now I see the paper on "dependent
object types" formalizes it. Now I am visualizing a relationship to De
Morgan's laws, subtyping, and Adriaan+paper's general
conceptualization of union (disjunction) and intersection
(conjunction) types. C.f. the prior observation of the relationship of
negation to subtyping in De Morgan's laws:

http://groups.google.com/group/scala-language/msg/637e214e6e6ceaf8

Union and intersection are duals. With intersection in the type
system, we can subsume in the covariant direction without losing
static typing, i.e. least upper bounds doesn't always end up `Nothing`
(bottom type). With union in the type system, we can subsume in the
contravariant direction without losing static typing, i.e. greatest
lower bounds doesn't always end up `Any` (top type).

Afaics, the S \/ T is the type we can assign to from the covariant
direction, i.e. constrains the subtypes, and `MS intersect MT` is the
type we inherit from to the contravariant direction, i.e. constrains
the members.

Thus the type system will have holes, unresolvable bugs, and corner
cases without a union type.

And the simulation I (based on Miles and Rex's ideas) provided in user
land is conceptually compatible with the above generalization. Thus
perhaps we could enable (hack) something sooner than reformulating
Scala's type system around this generalization, so at least we have
the S \/ T for the critical use cases interim. The `MS intersect MT`
generalization could follow later?

Thoughts?

[Adriaan Moors]

I oversimplified in my example. In practice, method types would only be allowed to match if their argument types match, and then the \/ or /\ is pushed down only to its result type.

It would get a lot hairier if you also want to push down to the argument types.

In theory, intuitively, I'd think you'd have to flip the /\ and \/ around since you're pushing down into a contravariant position. Thus, (A => B) \/ (C => D) becomes (A /\ B) => (C \/ D).

I've heard there are problems with this, but I don't remember exactly what they are. In any case, DOT does not push down /\ or \/ into function types. (There are no methods in the calculus -- just members with lambdas.)

(sorry, I don't have time to go into detail -- the pattern matcher awaits ;-))

[Adriaan Moors]

On Wednesday, March 7, 2012 7:14:44 PM UTC+1, Jesper Nordenberg wrote:

What would be the use case for this feature?

to have composition (\/ or /\) preserve more type information about the structure (the members) of the types you're composing -- right now, linearisation picks a winner, and all the other member's efforts have been for naught (as far as contributing to the signature goes, they can only force the types in certain directions of the subtype lattice)

with this scheme, everybody contributes with the same power

also, note that this is strictly a generalisation of the current scheme, since you can simplify the composed types to what linearisation comes up with now if the types of the members conform

[Shelby]

On Mar 8, 3:42 pm, Adriaan Moors <adriaan.mo...@gmail.com> wrote:
> In theory, intuitively, I'd think you'd have to flip the /\ and \/ around
> since you're pushing down into a contravariant position. Thus, (A => B) \/
> (C => D) becomes (A /\ B) => (C \/ D).

That appears to be the generalization of requiring "synonymous" (i.e.
invariant inputs in the contravariant position) members, and validates
that the members of the union is the intersection of the members.
Relating to my prior post, it appears the generalization is the
duality of covariance.

> I've heard there are problems with this, but I don't remember exactly what
> they are.

Wouldn't it conflict with overloaded members in the sense that we
don't want to box overloaded members into a union and be forced to
manually destructure them with `match`?

> In any case, DOT does not push down /\ or \/ into function types.
> (There are no methods in the calculus -- just members with lambdas.)

Maybe that is because per the above conflict concern, wouldn't we want
to avoid abstracting at the method level?

[Shelby]

On Mar 6, 7:00 am, Shelby <she...@coolpage.com> wrote:
> I hope I have successfully demonstrated how to simulate a nearly first-
> class union type:
>
> http://groups.google.com/group/shapeless-dev/browse_thread/thread/01f...
>
> And the negation of thedisjunction:
>
> http://www.chuusai.com/2011/06/09/scala-union-types-curry-howard/#com...

[...]

> P.S. There is a duplicate syntax-highlighted version buried nearer to
> the bottom of the following stackoverflow answer:
>
> http://stackoverflow.com/questions/3508077/does-scala-have-type-disju...

An update on my attempt to model union types in Scala:

https://issues.scala-lang.org/browse/SI-5549?focusedCommentId=57261&page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel#comment-57261

> P.S.S. Consider reading the Ceylon language design FAQ[8], as it
> appears to me to be significant substance in their effort, although I
> am not yet clear on what corner cases may be lurking in their attempts
> to simplify and make code more amenable to the mainsteam.

Looks like Higher Kinds might end up being the key feature that Ceylon
won't be able to do (in version 1.0 at least):

http://groups.google.com/group/ceylon-dev/browse_thread/thread/46dc2304dd8f54b1/de1a723bd6185a3e?#de1a723bd6185a3e

I realize Higher Kinds aren't currently utilized by the Scala standard
library, but I (and I surmise the Scalaz folks probably) think Functor
and its derivatives are critically necessary for reuse and modularity.

[Jason Zaugg]

On Fri, May 4, 2012 at 11:40 AM, Shelby <she...@coolpage.com> wrote:
> I realize Higher Kinds aren't currently utilized by the Scala standard
> library, but I (and I surmise the Scalaz folks probably) think Functor
> and its derivatives are critically necessary for reuse and modularity.

The standard library employs type constructor polymorphism, too:

https://github.com/scala/scala/blob/master/src/library/scala/collection/generic/GenericTraversableTemplate.scala#L17

-jason

[martin odersky]

Yes, indeed. The one thing where we hoped we could use them but ended up not to was in the collection classes themselves. There were too many irregularities at the leaves, for instance caused by the desire to embed arrays and strings and bitsets as collections, to be able to use higher-kinds in the root class (hint: arrays, strings, bitsets are not generic). So in the end hk-types were used in the factory classes only, because there they save code and we can simply roll factories by hand if the underlying type is not generic. The whole thing is really an illustration of the fragile base class problem.

Cheers

 - Martin

[Tony Morris]

On 04/05/12 19:40, Shelby wrote:
> I realize Higher Kinds aren't currently utilized by the Scala standard
> library, but I (and I surmise the Scalaz folks probably) think Functor
> and its derivatives are critically necessary for reuse and modularity.

We do, for some estimated large number of we.

--
Tony Morris
http://tmorris.net/

[Vlad Patryshev]

Tony,

I wonder what was the motivation behind choosing higher kind for, say the definition of Functor in scalaz, as opposed to, say something like this:

trait Functor {
  type f0[_]
  def f1[A,B](f:A=>B): f0[A] => f0[B]
}

Thanks,
-Vlad

[Miles Sabin]

On Fri, May 4, 2012 at 2:28 PM, Vlad Patryshev <vpatr...@gmail.com> wrote:
> I wonder what was the motivation behind choosing higher kind for, say the
> definition of Functor in scalaz, as opposed to, say something like this:
>
> trait Functor {
>   type f0[_]
>   def f1[A,B](f:A=>B): f0[A] => f0[B]
> }

You haven't gained anything by making it a member rather than a
parameter: f0[_] has kind * => *.

Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
g+: http://www.milessabin.com
http://twitter.com/milessabin
http://underscoreconsulting.com
http://www.chuusai.com

[Jason Zaugg]

On Fri, May 4, 2012 at 3:28 PM, Vlad Patryshev <vpatr...@gmail.com> wrote:
> Tony,
>
> I wonder what was the motivation behind choosing higher kind for, say the
> definition of Functor in scalaz, as opposed to, say something like this:
>
> trait Functor {
>   type f0[_]
>   def f1[A,B](f:A=>B): f0[A] => f0[B]
> }
>
> Thanks,
> -Vlad

You are asking about the choice between type parameters and type
members -- both encodings use type constructor polymorphism.

In many regards, the encodings are similar, as seen by the type alias
Functor_ herein:

scala> trait Functor { type F[_] } // map method elided
defined trait Functor

scala> implicit object listFunctor extends Functor { type F[a] = List[a] }
defined module listFunctor

scala> type Functor_[F_[_]] = Functor { type F[a] = F_[a] }
defined type alias Functor_

scala> def foo[F[_]: Functor_] = ()
foo: [F[_]](implicit evidence$1: Functor_[F])Unit

scala> foo[List]

scala> foo[Option]
<console>:12: error: could not find implicit value for evidence
parameter of type Functor_[Option]
foo[Option]
^

One practical problem is that the implicit scope for Functor_[X] does
not include the companion object of X, so you'll either need to put
your instances in object Functor (which turns out to be a bad idea
[1])

I tried out this encoding once with a subset of Scalaz, to explore the
advantages afforded by dependent method types. IIRC, the motivating
example was:

trait Functor { self =>
type F[_]
def compose(other: Functor): Functor { type F[A] = self.F[other.F[A]]] } = ...
}

def FunctionFunctor[I]: Functor { type F[O]=(I = O) }

FunctionFunctor[Int].compose(FunctionFunctor[String])

With the Scalaz encoding [2], you need to pass in the type parameter
to compose explicitly.

-jason

[1] https://github.com/scalaz/scalaz/blob/scalaz-seven/README.md
[2] https://github.com/scalaz/scalaz/blob/scalaz-seven/core/src/main/scala/scalaz/Functor.scala#L35

[Shelby]

Suggestion that we move any further discussion of higher kinds to
another thread, or scala-debate, then post a link here. So we don't
obscure discussion on the union type.

I am guilty of injecting it into this thread. My intention was to
answer my prior question as to whether Ceylon's union types gave it
some significant advantage over Scala. And I just wanted to say that
higher kinds are critical. Perhaps we can debate/discuss it further in
another thread.

I am now rereading section 6 Ad-hoc Polymorphism with Implicits, of
Fighting Bit Rot with Types, so I can compose a post to scala-debate.
I am be interested to get in depth into the design choices made. Is
there a pre-existing thread I should post to?

[Shelby]

On May 4, 10:00 pm, Shelby <she...@coolpage.com> wrote:
> Suggestion that we move any further discussion of higher kinds to
> another thread, or scala-debate, then post a link here.

[...]

> I am now rereading section 6 Ad-hoc Polymorphism with Implicits, of
> Fighting Bit Rot with Types, so I can compose a post to scala-debate.

Here is the link:

http://groups.google.com/group/scala-user/browse_thread/thread/770172e72892d8f3/8af329c4090c8b2c?#8af329c4090c8b2c

That responds to this:

[Shelby]

Afaics, adding first-class disjunctions is incompatible with the ability to instantiate structural types:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/eyNqO-soKQIJ

Did I make a mistake?

On Wednesday, March 7, 2012 9:11:01 PM UTC+8, Adriaan Moors wrote:

these encoding are neat, but the union types we're working on go beyond what you can do "in user space"

assume membersOf(S) = MS, membersOf(T) = MT

then, membersOf(S \/ T) = MS intersect MT,  (not a typo -- the members of a union type is the intersection of the sets of members of its constituents)

    where the intersection is computed by including only synonymous members from both MS and MT,

    say val m: Ts from MS and val m: Tt from MT yield a member val m: Ts \/ Tt of the intersected set

conversely, membersOf(S /\ T) = MS union MT (where, again, overlapping members have their types intersected)

(note that this is a work in progress, so I won't speculate on when/how/whether/... this ends up in a scalac near you)

On Tuesday, March 6, 2012 11:16:37 PM UTC+1, Rex Kerr wrote:

On Tue, Mar 6, 2012 at 4:52 PM, Shelby <she...@coolpage.com> wrote:

If my (twist on Miles Sabin's) implementation above is correct,
apparently the disjunction is the conjunction with subtyping in the
contravariant direction, with each item in the conjunction subtyped in
the contravariant direction. That appears to be a statement of De
Morgan's laws where negation is subtyping in the contravariant
direction.

Yes, that's correct--I believe that I had an exchange with Miles regarding exactly that in the comments on his union types post.

[Shelby]

Structural types inhabit bottom, thus are unsound?

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/iJHDLTcaB38J

[Shelby]

Resolution: both of my prior concerns are invalid:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/fbh3LY7M64kJ