Archive for types

Resumption

That was a longer hiatus than I had intended. Partly because not everything went according to plan.

My original plan was that, upon returning from my vacation, I would spend my remaining time at EPFL writing a technical report explaining everything I knew about the problems with Scala Classic. Instead, on my first day back in the office, Martin came by with a draft of a new formal system, DOT (for Dependent Object Types), that he came up with while he was on vacation. After about four weeks I managed to root out pretty much all of the obvious problems with DOT, but another four weeks was not enough to get the proofs and the metatheory into a state that we were happy with. I am not really sure what will happen with DOT in the long term.

There are a few clever things about DOT that avoid some of the problems I encountered with Scala Classic. For example, Scala Classic only had intersection types while DOT has both intersection and union types, which solves some problems with computing the members of types.  However, with Scala Classic I was trying to model a minimal subset Scala language as it exists, without adding any new features that many never be supported by the full language. I have no idea if we will see union types in the actual Scala implementation anytime soon.

The other thing DOT does is give up the goal of trying to be a minimal subset of Scala and throws out quite a few important things from a user perspective. For example, there are no methods (only λ-abstractions), no existentials, no built-in inheritance or mix-in composition (though you can encode it by hand), and object fields must be syntactically values.

This last restriction is particularly important because it solves by fiat the problems that arose in Scala Classic from using paths that have an empty type in dependent type projections. However, it also means that you may not be able to directly encode some Scala programs into DOT without an effect or termination analysis. Therefore, while DOT has the potential to be a useful intermediary step, there will still be more work to be done to provide a semantics for a more realistic subset of the Scala language.

I have been in Copenhagen for a little over a month now, but I am not really ready to comment on the research I have been doing here yet.  So in the meantime I'll probably focus more on fonts and typography.

Comments (1)

Literally dependent types

Given that the formalization of Scala Classic has ground to a halt, for reasons I may go into later, I spent part of today hacking on the Scala compiler itself to add support for singleton literals. Currently, Scala allows singleton types for stable identifiers. My modification allows literals to be used in singleton types. I can't promise that it will be in the forthcoming Scala 2.7.2 release, but I would like it to be.

Overall it was far less work than I was expecting.  Scala already internally supports what it calls "constant types", there is just no way to write them in Scala source code presently.  Consequently, most of the effort was in extending the parser.

Given my modifications, it is now possible to write code like the following:

  1.  
  2. scala> val x : "foo".type = "foo"
  3. x: "foo".type = foo
  4.  

What I was not expecting was that out-of-the-box things like the following would work:

  1.  
  2. scala> val x : "foobar".type = "foo" + "bar"
  3. x: "foobar".type = foobar
  4. scala> val y : 10.type = 2 * 5
  5. y: 10.type = 10
  6. scala> def frob(arg : 10.type) : 6.type = arg - 4
  7. frob: (10.type)6.type
  8.  

Unfortunately the excitement soon passes when you realize all the things you can't do with singleton literals (yet). Even if we turn on the experimental dependent method support, you can't write things like

  1.  
  2. def add(arg : Int) : (arg + 5).type = arg + 5
  3.  

because these are exactly what they are called, singleton literals, not full-blown dependent types.

One cute example, based on a use suggested by Sean McDirmid, would be that some people might do something like the following with implicits:

  1.  
  2. implicit stringToColor(arg : String) : java.awt.Color = java.awt.Color.getColor(arg)
  3.  

However, with singleton literals you can tighten it up by ensuring that for some strings it will never fail:

  1.  
  2. implicit redToColor(arg : "red".type) : java.awt.Color = java.awt.Color.RED
  3. implicit blueToColor(arg : "blue".type) : java.awt.Color = java.awt.Color.BLUE
  4.  

Happily, the type inferencer already chooses the most specific implicit conversions.

In any event, they will hopefully become more useful as the type system continues to grow. I am also sure someone will probably come up with a clever use for them that hasn't occurred to me yet. If so, let me know.

Comments (5)

Even better than the real thing

Scala Classic

Several weeks ago I decided that instead of calling the core calculus that I have been working on Featherweight Scala, which could be confusing given that there is already a different calculus with that name, that I would call it Scala Classic.

I had hoped to submit a paper on Scala Classic to POPL 2009, but it has been taking too long to work out the metatheory. Partly because I am developing a mechanized proof of type soundness in Twelf, and on my first attempt at representing heaps I think tried to be too clever.  However, a more traditional treatment of heaps leads to the need to explicitly represent typing contexts, rather than the implicit treatment of contexts more commonly used in Twelf.

This afternoon I finally finished the proof of the theorem that is traditionally called "substitution".  However, the proof of type preservation will also require another theorem formalizing a substitution-like property for singleton types.  I am hoping that I can prove that theorem more quickly now that I've built up all the explicit context theory.  I have not thought much about whether there are any unusual theorems needed to prove progress.

In any event, I would ideally have the proofs finished by the beginning of August.  My current plan is to try submitting the paper to PLDI (which is even in Europe this year), unless some obviously better venue comes to my attention.

One of the reasons I would really like to have the proofs done by August is that I will be teaching a PhD level course here at EPFL this fall on mechanized sepcifications and proofs, with a strong emphasis on deductive systems. It also looks like I may fill in some for a masters level course based on TAPL.  So between those two things, I am not going to have nearly as much time for research as would be ideal.

Comments

Functors in Scala

Following on my earlier entry on modules in Scala, I'll give an encoding of Standard ML style functors here. You can get a pretty close approximation by using class constructor arguments. However, I am going to cheat a little to get the closest encoding I think is possible by using the experimental support for dependent method types. You can get this by running scala or scalac with the option -Xexperimental. It works okay at least some of the time, but no one has the time at the moment to commit to getting it in shape for general consumption.

So here is my example of how the encoding works. First, the SML version:

  1.  
  2. signature Eq = sig
  3. type t
  4. val eq: t -> t -> bool
  5. end
  6.  
  7. signature RicherEq = sig
  8. include Eq
  9. val neq: t -> t -> bool
  10. end
  11.  
  12. functor mkRicherEq(arg : Eq) :> RicherEq where type t = arg.t = struct
  13. type t = arg.t
  14. val eq = arg.eq
  15. fun neq x y = not (eq x y)
  16. end
  17.  

We can transliterate this example into Scala as:

  1.  
  2. type Eq = {
  3. type T
  4. def eq(x: T, y: T): Boolean
  5. }
  6.  
  7. type RicherEq = {
  8. type T
  9. def eq(x: T, y: T): Boolean
  10. def neq(x: T, y: T): Boolean
  11. }
  12.  
  13. def mkRicherEq(arg: Eq) : RicherEq { type T = arg.T } = new {
  14. type T = arg.T
  15. def eq(x: T, y: T) = arg.eq(x, y)
  16. def neq(x: T, y:T) = !eq(x, y)
  17. }
  18.  

The only problem I discovered is that it is not possible to define RicherEq in terms of Eq as we could in SML:

  1.  
  2. scala> type RicherEq = Eq { def neq(x: T, y: T): Boolean }
  3. <console>:5: error: Parameter type in structural refinement may
  4. not refer to abstract type defined outside that same refinement
  5. type RicherEq = Eq { def neq(x: T, y: T): Boolean }
  6. ^
  7. <console>:5: error: Parameter type in structural refinement may
  8. not refer to abstract type defined outside that same refinement
  9. type RicherEq = Eq { def neq(x: T, y: T): Boolean }
  10. ^
  11.  

Why this restriction exists I don't know. In fact, this sort of refinement should work in the current version of Featherweight Scala, so perhaps it can be lifted eventually.

I still need to think about higher-order functors, and probably spend a few minutes researching existing proposals. I think this is probably something that cannot be easily supported in Scala if it will require allowing method invocations to appear in paths. However, off hand that only seems like it should be necessary for applicative higher-order functors, but again I definitely need to think it through.

Comments (2)

Modules in Scala

I just saw a thread on Lambda the Ultimate where I think the expressive power of Scala in comparison to Standard ML's module system was misrepresented. I don't want to go into all of the issues at the moment, but I figured out would point out that you can get the same structural typing, opaque sealing, and even the equivalent of SML's where type clause.

For example, consider the following SML signature:

  1.  
  2. signature Nat = sig
  3. type t
  4. val z: t
  5. val s: t -> t
  6. end
  7.  

This signature can be translated in to Scala as:

  1.  
  2. type Nat = {
  3. type T
  4. val z: T
  5. def s(arg: T): T
  6. }
  7.  

It is then possible to create an implementation of this type, and opaquely seal it (hiding the definition of T). In SML:

  1.  
  2. structure nat :> Nat = struct
  3. type t = int
  4. val z = 0
  5. fun s n = n + 1
  6. end
  7.  

In Scala:

  1.  
  2. val nat : Nat = new {
  3. type T = Int
  4. val z = 0
  5. def s(arg: Int) = arg + 1
  6. }
  7.  

In many cases when programming with SML modules it is necessary or convenient to give a module that reveals the definition of an abstract type. In the above example, this can be done by adding a where type clause to the first line:

  1.  
  2. structure nat :> Nat where type t = int = struct
  3. ...
  4.  

We can do the same thing in Scala using refinements:

  1.  
  2. val nat : Nat { type T = Int } = new {
  3. ...
  4.  

Great, right? Well, almost. The problem is that structural types are still a bit buggy in Scala compiler at present. So, while the above typechecks, you can't quite use it yet:

  1.  
  2. scala> nat.s(nat.z)
  3. java.lang.NoSuchMethodException: $anon$1.s(java.lang.Object)
  4. at java.lang.Class.getMethod(Class.java:1581)
  5. at .reflMethod$Method1(<console>:7)
  6. at .<init>(<console>:7)
  7. at .<clinit>(<console>)
  8. at RequestResult$.<init>(<console>:3)
  9. at RequestResult$.<clinit>(<console>)
  10. at RequestResult$result(<console>)
  11. at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
  12. at sun.reflec...
  13.  

There were some issues raised about how faithful an encoding of SML functors, and well-known extensions for higher-order functors, one can get in Scala. Indeed, off the top of my head it is not entirely clear. So I need to think more about that before I write some examples.

Comments (7)

Featherweight Scala lives

With everything else I've been having to deal with the past couple months, I have not made nearly as much progress on Featherweight Scala as I would have liked. Fortunately, in the past two weeks I have finally started to get back on track.

Probably what makes working out the design of Featherweight Scala so difficult is that I am trying my best to commit to it being a valid subset of Scala. It seems like whenever I try to simplify one part of the language, it just introduces a complication elsewhere. Still, I think so far that I have been able to ensure that it is a subset with two exceptions.

The first exception is that some programs in Featherweight Scala will diverge in cases where the Scala compiler will generate a terminating program. This is because in programs that attempt to access an uninitialized field, Scala will return null, while Featherweight Scala diverges. Since the program many never attempt to use the null value, it may simple terminate without raising a NullPointerException.

The second exception arises because type checking in Featherweight Scala's type system is most likely undecidable. Given that the design is in flux, I haven't precisely verified this, but it seems quite plausible given its expressive power is similar to languages where type checking is known to be undecidable. Because type checking is undecidable, and the Scala language implementation attempts to have its type checking phase be terminating, there should be some programs that can be shown to be well-typed in Featherweight Scala that the Scala compiler will reject.

I think the other thing I've determined is that I do not understand F-bounded quantification as well as I thought I did. At least, I find myself worried about the cases where the typing rules presently require  templates, that have not yet been verified to be well-formed, to be introduced as hypotheses while verifying their own correctness. So I need to do some additional reading to see how some other languages deal with this issue. Certainly I can put my mind at ease by making the type system more restrictive, but I do not want to be so restrictive that it is no longer reasonable to call the language Featherweight Scala.

Update: Okay, so after looking at Featherweight Generic Java and νObj again more closely, they both do essentially the same kind of thing. In FGJ, the class table is well-formed if all its classes are well-formed, but checking a class's well-formedness may require presupposing that that class tale is well-formed. In νObj, the well-formedness of recursive record types is checked under the assumption that the record's self-name has the type of the record. Certainly the same sort of things come up when verifying the well-formedness of recursive functions and recursive types, but at least there what is being assumed is at a higher level of abstraction: when checking a recursive function you assume that the function has some well-formed type, or when checking a recursive type you assume that the type has some well-formed kind.

Comments

Revisiting higher-rank impredicative polymorphism in Scala

I've been meaning to write this up for a while, but it seems like there has always been something else I really ought to be doing. So I expect this will be a bit more terse than I might like. Anyway, when I wrote about encoding higher-rank universal quantification in Scala back in March, I used a rather elaborate scheme involving the use of Scala's first-class existential quantifiers. While this was the point of the exercise, surprisingly, no one called me on the fact that if you just want higher-rank impredicative polymorphism in Scala, there is a much simpler encoding. Maybe it was obvious to everyone or no one read closely enough to think of raising the issue. So today, I'll explain the better way to encode them.

First we can define an infinite family of traits to represent n-ary universal quantification, much like Scala represents n-ary functions types:

  1.  
  2. trait Univ1[Bound1,Body[_]] {
  3. def Apply[T1<:Bound1] : Body[T1]
  4. }
  5.  
  6. trait Univ2[Bound1,Bound2,Body[_,_]] {
  7. def Apply[T1<:Bound1,T2<:Bound2] : Body[T1,T2]
  8. }
  9.  
  10. // ... so on for N > 2
  11.  

Really, the key to this encoding is the use of higher-kinded quantification to encode the binding structure of the quantifier.

Now it is possible to write some examples similar to what I gave previously, but more concisely:

  1.  
  2. object Test extends Application {
  3. def id[T](x : T) = x
  4.  
  5. type Id[T] = T => T
  6. val id = new Univ1[Any,Id]
  7. { def Apply[T <: Any] : Id[T] = id[T] _ }
  8.  
  9. val idString = id.Apply[String]
  10. val idStringList = id.Apply[List[String]]
  11.  
  12. println(idString("Foo"))
  13. println(idStringList(List("Foo", "Bar", "Baz")))
  14.  
  15. type Double[T] = T => (T, T)
  16. val double = new Univ1[Any,Double]
  17. { def Apply[T <: Any] : Double[T] = (x : T) => (x, x) }
  18.  
  19. val doubleString = double.Apply[String]
  20. val doubleStringList = double.Apply[List[String]]
  21.  
  22. println(doubleString("Foo"))
  23. println(doubleStringList(List("Foo", "Bar", "Baz")))
  24. }
  25.  

As I mentioned previously, this example would be much improved by support for anonymous type functions in Scala. I am pretty sure Scala will eventually support them, as they would not require any deep changes in the implementation. They could be just implemented by desugaring to a higher-kinded type alias with a fresh name, but depending on when that desugaring is performed, it is possible that it would result in poor error messages. Supporting curried type functions is also quite desirable, but given my current knowledge of the internals, that seems like adding them will require some more elaborate changes.

I think Vincent Cremet was the first person to suggest this sort of encoding, and I vaguely recall reading about it on one of the Scala mailing lists, but I could not find the message after a little bit of time spent searching.

Comments (4)

A new species

I spent some time last night looking more closely at Carette and Uszkey's new paper on species, as mentioned recently on Lambda the Ultimate. I mostly concentrated on the first few sections and the Haskell bit at the end. They say many tantalizing things, and I had kind of hoped the punchline would be something like "here is how you can write code in a beautifully functional style over graphs and cyclic structures" (assuming I understood the potential of species correctly).  Perhaps in a follow up paper.

I also found it interesting that their dot product operator sounds more like the traditional Cartesian product type (one of each type), and their Cartesian product type sounds much more like an intersection type (the value is a structure having both types). Perhaps it is a notational holdover from previous work on species. It also seem to make for some nice concrete examples of the "locative" aspects of Girard's Ludics.

Now back to reviewing journal and ICFP papers...

Comments (2)

Correction on existential unpacking

(WordPress ate my first draft, grrr.)

So after thinking about it further, I was incorrect, and it is possible to explicitly unpack existentials in Scala. As with some other languages, it is done via pattern matching. The following example illustrates how:

  1. val x : List[T] forSome { type T } = List(42)
  2. val w = x match { case y : List[u] => ((z : u) => z)(y.head) }

However, in practice this functionality seems to be rather fragile. For example, the following two variations are rejected:

  1. val x : T forSome { type T } = 42
  2. val w = x match { case y : u => ((z : u) => z)(y) }

and

  1. val x : List[List[T]] forSome { type T } = List(List(42))
  2. val w = x match { case y : List[List[u]] => ((z : u) => z)(y.head.head) }

In both cases it reports that it cannot find the type u. In the second case, it could be attributed to erasure, as there is no way dynamically to guarantee that the contents of List are in turn also a List. However, the first seems reasonable, so it should probably be reported as a bug.

Comments

Higher-rank, impredicative polymorphism in Scala

One project that I spent some time thinking about prior arriving in Lausanne was whether I might be able to put together a Scala library for manipulating data-structures with binding based around the use of parametricity to help enforce the adequacy of function spaces (ala Boxes Go Bananas). However, one problem is that Scala does not have higher-rank polymorphism like GHC. The initial thought was, "well, Scala has higher-rank existential types, so adding the dual case should be pretty straightforward to add to the typechecker". However, it turns out it is not so straightforward to add universal quantification to the implementation of the subtyping algorithm and ensure that constraints can be solved unambiguously. It still may make sense to try and add them in some fashion.

Later, while working on Featherweight Scala, it occurred to me that subtyping is very likely to be undecidable in Scala because its language of types is essentially as expressive as full F<:. Benjamin agreed that there existed a straightforward reduction to languages with only bounded existential quantification rather than bounded universal quantification, but did not know offhand if there is a paper that gives it.

So I spent a bit of time thinking about encoding universal quantification using existential quantification, and as alluded to in TAPL (the answer to exercise 24.3.3), it can be done, but there is no completely local encoding of universals into existentials. To obtain the classical equivalences between the negation of universal quantification and existential quantification (∀α.τ implies ¬∃α.¬τ) in a constructive setting you have to use the double-negation encoding, which essentially means CPS converting your program. The other classical equivalence under negation, ∃α.τ implies ¬∀α.¬τ, is constructively valid which is why it is existential quantification is macro-expressible in languages with universal quantification.

Since I am not aware of any papers that illustrate the encoding of universals into existentials, I figured I would explain it here. The encoding of the universal type pretty much follows from the equivalence:

|∀α.τ| = (∃α.|τ|→0)→0

Here I am using 0 for the void or empty type and using the standard constructive encoding of negation:

|¬τ| = |τ| → 0

The term level encodings are not so difficult, but does require a little thought:

|Λα.e : ∀α.τ|k = k (λx:∃α.|τ|→0.let (α,k') = unpack x in |e : τ|k')

The term encoding has the form |e : τ|k, where τ is the type of the term and k is a continuation threaded through the encoding. The first thing to note is that because type abstractions are values, we always immediately pass them to the continuation. Given that,
if we look at the type we need to give the encoding of type abstraction, it is a function that that takes an existentially quantified continuation, and never returns. The only way to never return is to use the continuation. This tells us just about everything else we need to know about the encoding.

Because the continuation is existentially quantified, it is not possible to invoke it as is, so we must unpack it first. This is how we simulate the introduction of a type variable without using type abstraction. The next problem is that in order to call the continuation, we need to apply it to something with the correct type. The continuation takes values of type |τ|, possibly referencing a free type variable α, which is fortunately what the encoding of the type abstraction's body gives us. Therefore, we can use the unpacked continuation k' as the continuation argument of the recursive call to the encoding.

Given that we know how to encode type abstractions, encoding type applications is straightforward:

|e[τ] : τ'|k = |e : ∀α.τ'{α/τ}|(λv:(∃α.τ'{α/τ}→0)→0.v (pack(τ,k) as ∃α.(τ'{α/τ}→0)))

We encode the term to be applied and pass it a new continuation, that packs up the original continuation and applies it to function to which the term evaluates. I am writing {α/τ} to mean replace τ with α. I am using curly braces rather than the usual square brackets to avoid confusion with the square brackets that is commonly used for type application.

While I am almost certain that the encoding above is correct, it would be good at some point to prove it. This is the sort of proof for which Twelf is very well suited, so that is probably the route I would take.

Okay, so that is the theoretical half out of the way. Now, given the above, can we implement higher-rank impredicative polymoprhism in Scala? Yes, with a minor caveat.

First, I'll define an abstract class that defines the type of bounded universally quantified values, and methods for creating and destructing them.

  1. abstract class Universal {
  2. type Univ[Bound,Body[_]]
  3.  
  4. def createUniv[Bound,Body[_]]
  5. (impl : ((Body[A] => Nothing) forSome { type A <: Bound }) => Nothing) :
  6. Univ[Bound,Body]
  7.  
  8. def applyUniv[Bound,Body[_],A<:Bound](arg : Univ[Bound,Body]) : Body[A]
  9. }

This should be fairly straightforward given the encoding described above. The only tricky bit is the use of a higher-kinded type parameter (

  1. Body[_]
) to give the body of the universal type. The other important point to note is that it is not necessary to completely CPS convert the implementation because Scala provides primitives for non-local control transfers.

One possible implementation of the above abstract class is the following:

  1. class UniversalImpl extends Universal {
  2. type Univ[Bound,Body[_]] =
  3. ((Body[A] => Nothing) forSome { type A <: Bound }) => Nothing
  4.  
  5. def createUniv[Bound,Body[_]]
  6. (impl : ((Body[A] => Nothing) forSome { type A <: Bound }) => Nothing) :
  7. Univ[Bound,Body] = impl
  8.  
  9. def applyUniv [Bound,Body[_],A<:Bound](univ : Univ[Bound,Body]) : Body[A] = {
  10. case class Control(arg : Body[A]) extends Throwable
  11. val res = try {
  12. univ((arg:Body[A]) => throw new Control(arg))
  13. } catch {
  14. case Control(arg) => arg
  15. case e => throw e
  16. }
  17. res
  18. }
  19. }

The implementation of the abstract type and the code for

  1. createUniv
are trivial. The implementation of
  1. applyUniv
is a little more interesting. Here, we create a local case class
  1. Control
, extending
  1. Throwable
so that it may be thrown as an exception, that will hold a value of the desired result type. We then just pass the representation of the type abstraction a continuation that throws a new instance of
  1. Control
. We immediately catch it and return the value stored within. If we happen to catch some other sort of
  1. Throwable
we just re-throw it.

And that's it. It is worth looking at a few examples of how this might be used. The first thing that is necessary is to create a concrete implementation of Universal:

  1. val u : Universal = new UniversalImpl

Given

  1. u
, we can create an instance of the polymorphic identity function:

  1. type Id[T] = T => T
  2. val id =
  3. u.createUniv[AnyRef,Id](
  4. (k: (Id[A] => Nothing) forSome { type A }) =>
  5. k(x => x))
  6. val idString = u.applyUniv[AnyRef,Id,String](id)
  7. val idStringList = u.applyUniv[AnyRef,Id,List[String]](id)
  8. println(idString("Foo"))
  9. println(idStringList(List("Foo", "Bar", "Baz")))

The first thing that needs to be done is to define a type function for representation the body of the universally quantified type. For the polymorphic identity function we call it

  1. Id[T]
. The rest is pretty straightforward. It ought to be possible to make the above code a little less verbose if Scala allowed type parameters to methods to be curried: it should be possible for it to infer that the first two arguments to
  1. u.applyUniv
are
  1. AnyRef
and
  1. Id
from the argument
  1. id
. However, because it will not be able to infer the last type parameter, we have to give all three. It might also be desirable in some case to not have to give a type definition to define the body of the a universal type; this could be achieve by extending Scala with support for anonymous type functions.

Now for that caveat I mentioned. When we defined the type abstraction,

  1. u.createUniv[AnyRef,Id](
  2. (k: (Id[A] => Nothing) forSome { type A }) =>
  3. k(x => x))

a significant difference between how this code is written, and how it would have been written in terms of my original explanation of the encoding, is that there is no explicit unpacking of the existential. All existential unpacking in Scala is implicit. This is nice in some ways, but it means that we have no way to give a name to type that the existential is hiding. Therefore, when constructing a function to pass to the continuation,

  1. k(x => x)

it must be the case that Scala can infer the domain of this function's type, because it is not possible to write a type annotation for

  1. x
without having a name for the existentially hidden type. I think in most cases this should not be possible, as Scala knows the type that
  1. k
is expecting as an argument, but there may be some corner cases I have not considered.

(Does anyone know how to prevent WordPress from completely screwing up less than and greater than inside of <pre> tags?)

Comments (4)

« Previous entries Next Page » Next Page »