Lambda the Ultimate

Given the choice to go with type erasure as the "implementation" choice for generics in Java 5 (and look how well that turned out), I would hope that they don't actually attempt putting this in Java.

I don't see how erasure causes a problem for type constructor polymorphism.

Especially considering that Scala has erasure and type-constructor polymorphism.

As far as I know, Scala does not implement polymorphism by type erasure.

It does. You can prove it with a simple type case (here I use an unbounded existential type parameter but that's not essential to the demonstration).

scala> def test(x : List[_]) = x match {
     |    case _ : List[Int] => "it's ints!"
     |    case _ : List[String] => "it's strings!"
     | }
<console>:5: warning: non variable type-argument Int in type pattern List[Int] is unchecked since it is eliminated by erasure
          case _ : List[Int] => "it's ints!"
                   ^
<console>:6: warning: non variable type-argument String in type pattern List[String] is unchecked since it is eliminated by erasure
          case _ : List[String] => "it's strings!"

<console>:4: warning: match is not exhaustive!
missing combination   $colon$colon

       def test(x : List[_]) = x match {
                               ^
test: (x: List[_])java.lang.String

scala> test(List('a', 'b', 'c'))
res1: java.lang.String = it's ints!

Ah, my mistake. Though such typecases are "impure" in some people's eyes, I sometimes find them useful to implement a kind of ad-hoc polymorphism, e.g. in Virgil, which does not (yet) have a typeclass mechanism, but has parametric types and does not erase them. This means that the compiler must specialize the code when compiling for the JVM. Full specialization of course causes problems with polymorphic recursion, unfortunately.

I think in Scala anytime erasure hurts you it's because you've violated parametricity. As you say that's sometimes useful. In Java erasure also hurts due to interference with other parts of the language. To answer your other question, that was the Scala library List but any type constructor would do.

What about allocating an array of a parametric type? Unlike parametrized classes, arrays in Java can be thought of as a type constructor that actually does reify its type parameters at runtime.

Note also that parametricity also interacts with inheritance--you can "hide" types by creating an unparameterized superclass and casting to the parameterized subclass. Doing so may not technically be a violation of parametricity. I also sometimes find this useful, e.g. (Virgil syntax, which I hope you can work out through context):

class Val {
}

class Box<T> extends Val {
  field x: T;
  new(x: T) { this.x = x; }
}

...
class Interpreter {
  method unbox<T>(v: Val) -> T {
    // cast and access value
    return Box<T>.!(v).x;
  }
  method add(v1: Val, v2: Val) -> Val {
    // note type inference for unbox() calls and Box.new() call
    return Box.new(unbox(v1) + unbox(v2));
  }
}

(Note that there is no language level boxing in Virgil--these are all simply user classes.)

Here's another example that reuses the Box and Val classes:

class Other {
  method castOrNull<T>(v: Val) -> Box<T> {
    // check if cast would succeed
    if (Box<T>.?(v)) return Box<T>.!(v);
    else return null; // cast would fail, return null
  }
}

This kind of pattern has started to show up in lots of places in my compiler, and I find it pretty convenient. The first example can be done in Java, but the second example absolute requires reified types (or specialization).

That's an interesting point about parameterized subclasses and extracting values of a certain type using something like Maybe or Null. So I take it back: there are some parametriticy preserving ways to use full run time type information.

As for arrays in Scala, they are a bit complicated. For more than you ever wanted to know about how Scala deals with them see this document describing both the old and new system for arrays.

You're right, that is more than I wanted to know about Scala arrays :-) The conclusion I came to some time back was that if you want real parametric types with all the capabilities, you have two choices: type parameters are either implicit reified parameters, or type parameters are completely specialized away. As far as I know, Haskell (at least GHC) takes the former approach, and C++ obviously takes the latter approach. The CLR also specializes, but the VM does this underneath (type parameters are explicit in class files). Type erasure like Java is broken in too many ways to count.

If your language is going to have a VM, then I think the C# approach is best. If your language is going to target a real machine, then I think a mix of reification and specialization is the best approach, though I have yet to come across an implementation that does both.

I think you're wrong about GHC. Type classes are "implicit reified parameters" (although they're often specialized away), but plain old type parameters are erased. Maybe I misunderstand what you're saying, though.

Why would we not consider Box<T>.! and Box<T>.? to violate parametricity? Before reading any of this, I would have certainly considered casts or "can cast queries" as parametricity violations.

The conclusion I came to some time back was that if you want real parametric types with all the capabilities, you have two choices: type parameters are either implicit reified parameters, or type parameters are completely specialized away.

If run-time casts are among the capabilities you want, then this would seem to be true, but I don't see why it should be true otherwise. Do you have other examples or arguments? (As I'm working on a language with type erasure, I'd love to understand your reasoning here!)

I don't consider polymorphic casts of this type to be a violation of parametricity*, but there is another instance where problems arise. Even if you don't use runtime casts, if your types don't have a uniform representation in the machine you are translating to (e.g. primitives vs. objects on the JVM), you will need some runtime type information in order to, for example, allocate an array with the appropriate representation, or allocate an object that has a field of the parametric type. Worse, at the machine level, even passing a value of a parametric type might require a different register (or set of registers) depending on its type and the calling conventions established by your compiler or the ABI of your platform.

However, you are right in that most of the problems that manifest for programmers rather than implementors seem to stem from runtime type tests of one kind or another. For example, if you have inheritance and overriding in your language, you can try simulate casts by writing is/as methods, but even with the hidden type parameter, you still end up needing a polymorphic cast inside!

class A {
  method isB<X>() -> bool { return false; }
  method asB<X>() -> B<X> { return null; }
}
class B<T> extends A {
  method isB<X>() -> bool {
    // yes, we are a B<T>, but are we a B<X> ???
    return B<X>.?(this);
  }
  method asB<X>() -> B<X> {
    // hide the cast in here....
    return B<X>.!(this);
  }
}

So maybe I should amend my earlier conclusion. If you have a nonuniform representation of types in your implementation, or if you have runtime type tests of any kind, you will have to either reify or specialize to get the full power of parametric types.

* The possibility that a type test could fail or a cast throw an exception is independent of whether parametric types are involved.

I think much of my confusion in this subthread has been from the application of "parametricity" to an OOP setting. Parametricity is about types of functions reflecting the operations those functions perform on their parameters. If every value in the language is an object supporting "type casting" (really a form of constructor matching) then you'll still have some sort of "parametricity theorem", but the free theorems will be extremely weak (probably useless).

I favor not having any operations built in to every value, and letting values come equipped with extra tagging information in special situations if needed. Anyway, I agree with most of the stuff you wrote. This is just clarifying my position and explaining my confusion.

If every value in the language is an object supporting "type casting" (really a form of constructor matching) then you'll still have some sort of "parametricity theorem"

I don't see how. Casts and reflection break parametricity straight out, no way around that. The analogy with constructor matching is misleading, because with constructors there is no persistent 1-to-1 correspondence to types.

Well, it's not clear to me what parametricity means in a general setting. How are types in some arbitrary type system considered relations?

The construction I have in mind is to construct a type system "outside" of the original (possibly typed) language, for which function types and quantifiers mean what we want them to mean. Then we can get a parametricity theorem in this more general setting, and as long as types in the original langauge have corresponding types in the enriched type system, we can pull back our free theorems.

In order to assign a more traditional type to a value in the language, you have to have modeled all computation that can be performed in the language. For example, you have to model casts as operations on tagged data. You could probably also model side-effects functionally and get parametricity results for impure languages this way.

I await your objections :)

Well, it's not clear to me what parametricity means in a general setting.

Good question! FWIW, we tried to give some answers in our ICFP'09 paper.

How are types in some arbitrary type system considered relations?

Usually, you want the relational interpretation to be at least a sound approximation of observational equivalence. That is, it should never relate two objects that can be told apart by some program context. On the other hand, you need every well-formed object to be related to itself.

A (logical) relation is parametric if the case for polymorphic types is defined such that you can nevertheless always pick an arbitrary relation as representative for the quantified type. If you can still prove soundness of the relation then this implies that polymorphic types are really abstract.

A polymorphic function whose result depends on the outcome of some cast is not even related to itself under such a definition. Consequently, a parametric relation can't be sound in the presence of such casts.

I'm not sure I fully understand your suggestion or how it would change the situation. It seems like you are proposing to encode the non-parametric language in a parametric one. That can be done, but then parametricity of the host language does not necessarily imply anything interesting about the object language. Also, to transfer any results you might need to know that your encoding is fully abstract, a property that generally is extremely hard to prove.

A (logical) relation is parametric if the case for polymorphic types is defined such that you can nevertheless always pick an arbitrary relation as representative for the quantified type.

Well, taking this to define the relation corresponding to e.g. List<T> in an OOP language with casting does look like it will break parametricity. I'm suggesting: don't do that. It seems that with a modified definition that restricts what relations we're quantifying over (and with similar modifications elsewhere), that we could preserve the statement of the parametricity theorem. I'm fuzzy on the details, though, and I can see why you would object to calling such a thing "parametricity".

I don't understand what you are trying to achieve. That is the distinguished meaning of "parametricity". What you propose is like redefining "non-smoking" to mean "no smoking, but igniting cigarettes is allowed", i.e. it simply renders the word meaningless.

As for the "parametricity theorem", there isn't really any such theorem. What Wadler calls the parametricity proposition is simply the so-called Fundamental Property or Fundamental Theorem of the logical relation - i.e., that every well-formed term is related to itself. In his case the relation was parametric, but you will have such a theorem for any suitable logical relation, parametric or not (see our aforementioned paper for an example of a non-parametric one). But of course, if the relation is non-parametric, you don't get any "free theorems" out of it.

I'm just defending my speculation that you can get free theorems in the same spirit as "Theorems for Free!" even if parameterization in your language isn't completely "free". The speculation is that, heuristically, instead of interpreting a type like List<T> as something akin to (forall a. List a), you interpret it as something like (forall a. Castable a => List a). I mentioned at the outset that resulting free theorems would probably be weak to the point of useless. Maybe such things shouldn't be called "parametricity", but it's in the same vein.

Thanks for the link, btw. I've only read part of it, but so far it's interesting.

While I understand your argument, I favor Andreas's underlying position that we shouldn't undermine the meaning of our words by allowing them to apply vacuously or when they fail to make a useful distinction. When someone says 'parametric', I expect them to mean it in some useful manner, lest we discuss the pinkness of invisible unicorns.

In that same vein, 'type safety' and 'type inference' shouldn't be used for systems that have only one type, and 'capability model' shouldn't be applied to pure functional expressions that forbid communication effects.

The resulting theorems would no doubt be complex, weak, and practically useless, but they would not be strictly trivial. I don't disagree that 'parametricity theorem' is a bad name for this.

I suspect I'll need to see a non-trivial theorem before I'll agree they exist.

You used 'forall a.Castable a => List a'. It is unclear what, precisely, 'Castable' means to you. (How does it relate to Haskell's "Dynamic" or "Typeable" classes?)

But I assume your qualifying use of the intentionally vague phrases "something akin to" and "something like" means I am to substitute 'Castable' with whatever kin come to mind.

Reflective programming comes to mind. So let's use that: forall a. Reflective a => List a, where 'Reflective a' at its limit would mean access to arbitrary properties of the type, the specific values, and potentially even the version-history of the type and the origin of those values (fexpr-like access to context (lexical and dynamic environment), expression (operands and operands' operands), reflective stacks).

If you do not feel I am too broadly interpreting the momentary hand-waving you included in your earlier post, then of which non-trivial parametricity theorems do you speak that will apply to Castable and its various kin?

If every operation is possible on every parameter, you don't get any nontrivial theorems. So with a strong enough reflection, you'd necessarily have no free theorems. If you're only allowed casts, it looks like you could say something about how a function behaves with respect to fresh types. Does that count? :)

Without casting there's only one value with type forall a.List a, []. With cast :: forall a b : a -> Maybe b I can create all kinds of values

helloWorldOrNil :: forall a. List a
helloWorldOrNil = fromMaybe [] $ cast "hello world!"

What theorems does that leave me with?

But parametricity is easy if the only type is Univ. You just don't get any theorems...

Yeah, making cast total gives you "forall a b.a -> Maybe b" which is some seriously weak tea.

If you have parametric type constraints and a subtype relation <: you can do a little better:

forall A B | B <: A. A -> Maybe B 

Of course then the subtype relation must cover type parameters as well, or you get into further binds down the road.

Once your language has a top type (like, for most purposes, Object in Java), that type is as general.

From that you can build

forall a b exists t | a <: t ^ b <: t . a -> Maybe b

And, as Andreas says, a top type trivially satisfies the existence of t.

BTW, is the List class in this example the List imported from Java, or part of the Scala libraries?