Higher ranked types?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Higher ranked types?

David MacIver
Scala has higher kinded types, which is nice. They have some
limitations but are basically very useful.

What it doesn't have is higher ranked types. i.e. types with explicit
foralls in them. For example:

def id[T](x : T) = x

I can define a function corresponding to this method as follows:

id(_)

But this doesn't work. I have to assign a parameter type in order to
make use of this. (In actual fact this does compile, but apparently
not to anything very useful and it looks like a bug).

So I can have an Int => Int, but not a forall T => T.

Another area where I particularly want this is that a case class's
companion object has the following signature:

case class Foo(x : Int);

gives

object Foo{
  def apply(x : Int) : Foo = ...;
  def unapply(x : Foo) : Some(Product1[Int]) = ...
}

(Actually this doesn't work at the moment. But moving swiftly on...)

Now, it would be nice to give a common trait for this (and I don't
just mean conceptually nice. One of the things I'm trying to do in
SBinary is to provide generic methods of dealing with binary
representations of case classes, and I keep running into typing and
implementation restrictions. I think this would be useful for any sort
of generic handling of case classes). Say

trait CaseCompanion1[Case, T]{
  def apply(x : T) : Case;
  def unapply(x : Case): Some[Product1[T]]
}

Then Foo's companion can implement CaseCompanion1[Foo, Int].

But there's a problem. This can't work properly:

case class Bar[T](x : T);

object Bar extends CaseCompanion1[????]

We need Bar to have a type parameter. But it can't, it's an object!

Adding some sort of universal quantification would let us do something like:

object Bar extends forall T CaseCompanion[Bar[T], T]

And it would just work nicely.

The way I see this working is that any type parameters in a forall get
moved to type parameters on members of the object. In particular,
members which can't have type parameters are thus forbidden (or, if
one prefers, required to have their types not dependent on T, or
assignable to what their type would be with T for any possible value
of T. The details need thinking about). This is analagous to ML's
value restriction.

This seems like it shouldn't be too hard to implement - it's somewhere
where type erasure is actually rather useful, as you won't have to
change the representations much, but I suspect it's going to play hell
with typing rules. Still, I'd find it very useful, so I live in hope.
:-) What does everyone else think?
Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

Geoffrey Alan Washburn-4
David MacIver wrote:
> Scala has higher kinded types, which is nice. They have some
> limitations but are basically very useful.
>
> What it doesn't have is higher ranked types. i.e. types with explicit
> foralls in them.

Strictly speaking higher-rank types are not limited to foralls, so in a
sense Scala does have first-class higher-rank existential types.

However, it is certainly possible to encode higher-rank universal types.
     I have previously shown how to do this by taking advantage of the
fact that it is possible to encode universals using existentials:

http://existentialtype.net/2008/03/09/higher-rank-impredicative-polymorphism-in-scala/

However, that is more elaborate than is really necessary.  See the
following example:

trait Univ1[Bound1,Body[_]] {
   def applyUniv[T1<:Bound1] : Body[T1]
}

trait Univ2[Bound1,Bound2,Body[_,_]] {
   def applyUniv[T1<:Bound1,T2<:Bound2] : Body[T1,T2]
}

// ... so on for N > 2

object Test extends Application {
   val u : Universal = new UniversalImpl

   def id[T](x : T) = x

   type Id[T] = T => T
   val id = new Univ1[Any,Id]
     { def applyUniv[T <: Any] : Id[T] = id[T] _ }

   val idString = id.applyUniv[String]
   val idStringList = id.applyUniv[List[String]]

   println(idString("Foo"))
   println(idStringList(List("Foo", "Bar", "Baz")))

   type Double[T] = T => (T, T)
   val double = new Univ1[Any,Double]
     { def applyUniv[T <: Any] : Double[T] = (x : T) => (x, x) }

   val doubleString = double.applyUniv[String]
   val doubleStringList = double.applyUniv[List[String]]

   println(doubleString("Foo"))
   println(doubleStringList(List("Foo", "Bar", "Baz")))
}


The above is less than ideal still, as Scala does not presently have
support for anonymous type functions, and it is still heavier than
Scala's existential types.

There had been some discussion of adding first-class universal types to
Scala, but it turns out that they actually complicate Scala's type
inference algorithm in a non-trivial fashion.  But we still may do
something about it eventually.

Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

Miles Sabin
In reply to this post by David MacIver
On Fri, May 9, 2008 at 9:37 AM, David MacIver <[hidden email]> wrote:
> Scala has higher kinded types, which is nice. They have some
> limitations but are basically very useful.
>
> What it doesn't have is higher ranked types. i.e. types with explicit
> foralls in them.
<snip/>

Vincent Cremet came up with an encoding for this a while back,

  object HigherKinded extends Application {
    trait Forall[A[_]] { def Apply[T](): A[T] }

    def id[T](x : T) = x

    type Fn[T] = T => T

    val Id : Forall[Fn] = new Forall[Fn] { def Apply[T]() : Fn[T] = id }

    println(Id.Apply()("Hello world"))
    println(Id.Apply()(123))
  }

Cheers,


Miles
Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

David MacIver
Right. I know you can encode it like that. For some things it works
adequaly, but it e.g. doesn't work very well for my use case with a
trait for case classes.

The problem is that currently you can (often with far more hackery
than is desirable) encode separate types which behave in a universally
quanitified way, but there's no good way of getting universal
quantification for existing types.

On Fri, May 9, 2008 at 10:32 AM, Miles Sabin <[hidden email]> wrote:

> On Fri, May 9, 2008 at 9:37 AM, David MacIver <[hidden email]> wrote:
>> Scala has higher kinded types, which is nice. They have some
>> limitations but are basically very useful.
>>
>> What it doesn't have is higher ranked types. i.e. types with explicit
>> foralls in them.
> <snip/>
>
> Vincent Cremet came up with an encoding for this a while back,
>
>  object HigherKinded extends Application {
>    trait Forall[A[_]] { def Apply[T](): A[T] }
>
>    def id[T](x : T) = x
>
>    type Fn[T] = T => T
>
>    val Id : Forall[Fn] = new Forall[Fn] { def Apply[T]() : Fn[T] = id }
>
>    println(Id.Apply()("Hello world"))
>    println(Id.Apply()(123))
>  }
>
> Cheers,
>
>
> Miles
>
Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

David MacIver
In reply to this post by Geoffrey Alan Washburn-4
On Fri, May 9, 2008 at 10:20 AM, Geoffrey Alan Washburn
<[hidden email]> wrote:

> David MacIver wrote:
>>
>> Scala has higher kinded types, which is nice. They have some
>> limitations but are basically very useful.
>>
>> What it doesn't have is higher ranked types. i.e. types with explicit
>> foralls in them.
>
> Strictly speaking higher-rank types are not limited to foralls, so in a
> sense Scala does have first-class higher-rank existential types.

Good point.

> However, it is certainly possible to encode higher-rank universal types.
>  I have previously shown how to do this by taking advantage of the fact that
> it is possible to encode universals using existentials:
(snipped code)
> The above is less than ideal still, as Scala does not presently have support
> for anonymous type functions, and it is still heavier than Scala's
> existential types.

Right. I'm familiar with the encodings. They're better than nothing,
but the problem is that it creates a total divide between the
universally quantified types and their first rank counterparts. And it
doesn't work for my case class use case and similar where I want an
object which is a forall T Foo[T].

> There had been some discussion of adding first-class universal types to
> Scala, but it turns out that they actually complicate Scala's type inference
> algorithm in a non-trivial fashion.

Fair enough. That's a shame, but I'll live. :-)

> But we still may do something about it eventually.

*crosses fingers hopefully*
Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

Geoffrey Alan Washburn-4
David MacIver wrote:
> *crosses fingers hopefully*

Now that I looked more closely at your case class example, having first
class universals would not do what you want anyway.  They won't "float"
like they would in languages based upon Hindley-Milner type inference.


Reply | Threaded
Open this post in threaded view
|

Re: Higher ranked types?

Geoffrey Alan Washburn-4
In reply to this post by David MacIver
David MacIver wrote:

> Adding some sort of universal quantification would let us do something like:
>
> object Bar extends forall T CaseCompanion[Bar[T], T]
>
> And it would just work nicely.

No, this would not.  If you look at the rules for subsumption of
universals and existential types this is the same as saying that

   object Bar extends CaseCompanion[Bar[U], U]

for some fresh type variable U.  There is no sensible way Bar could
provide implementations of the methods apply and unapply with types

   def apply(x : U) : Case;
   def unapply(x : Case): Some[Product1[U]]

because U may not be named inside of Bar.

Reply | Threaded
Open this post in threaded view
|

Re: Re: Higher ranked types?

Matt Hellige
On Fri, May 9, 2008 at 5:24 AM, Geoffrey Alan Washburn
<[hidden email]> wrote:

> David MacIver wrote:
>
>>
>> And it would just work nicely.
>
> No, this would not.  If you look at the rules for subsumption of universals
> and existential types this is the same as saying that
>
>  object Bar extends CaseCompanion[Bar[U], U]
>
> for some fresh type variable U.  There is no sensible way Bar could provide
> implementations of the methods apply and unapply with types
>
>  def apply(x : U) : Case;
>  def unapply(x : Case): Some[Product1[U]]
>
> because U may not be named inside of Bar.
>

But it does seem intuitively sensible that this should work like
existentials: I can't name U or assume any bounds for it, but I should
be able to just pass the values around in an opaque way:
 object Bar extends CaseCompanion[Bar[U], U] {
   def apply(x : U) : Bar[U] = new Bar[U](x)
   def unapply(x : Bar[U]): Some[Product1[U]] = Some(Tuple1(x.x))
}

I know existentials are not the right machinery for this. If explicit
forall is also the wrong machinery, the question then is: what is the
right machinery? Is there a fundamental problem with allowing this
kind of reuse? I seem to remember that you provided a problematic
example the last time this came up, but I can't find it in the
archives... :(

Matt

--
Matt Hellige / [hidden email]
http://matt.immute.net