tear-offs: clarify / make explicit how tear-offs will be treated

[chalin]

The proposal should clarify / make explicit how tear-offs will be treated. Maybe a separate section covering tear-offs of generic functions would be appropriate.

---

Examples of the questions to be answered are given below. Consider the following code:

class C<T> {
  Map<K,T> m<K>(T1 a1, …, Tn an) { ... }
}

C<A> c = new C<A>(); // for some type A

Which of the following tear-off expressions are legal?

• c.m#
• c.m<B># for some type B.

The first one is the most interesting case. Relevant questions include: for c.m# what are its

• static type,
• value,
• runtime type?

Static type of c.m#?

• (T1, …, Tn) -> Map<dynamic,A>, or
• <K>(T1, …, Tn) -> Map<K,A>

Value of c.m#?

• (T1 a1, …, Tn an) => c.m<dynamic>(a1, …, an), or
• <K>(T1 a1, …, Tn an) => c.m<K>(a1, …, an) by a slight abuse of notation.

Either of the two static type candidates above could work for the runtime type.

[leafpetersen]

This is addressed (albeit not including the new tear-off syntax). The static typing is addressed under the "Expression typing" section, and the semantic behavior is discussed under the "Generic instantiation expressions (functions)" and "Generic instantiation expressions (method closurization)" sections. There are examples of tear-offs in the introductory sections (though again, not using the new syntax).

I'll consider adding some explicit commentary or a section on tear-offs to make this clearer. I should probably also flesh out the syntactic interactions with the new tear-off syntax.

To address the concrete questions:

Which of the following tear-off expressions are legal?

• c.m#
• c.m<B># for some type B.

The first is legal in the proposal as it stands, but issues have been raised around the fact that introduces implicit coercions into Dart (there is some discussion of this in the text). This may be eliminated in favor of making this a static and/or dynamic error. If legal, this proposal makes it entirely equivalent to c.m<dynamic>#

The second is fully legal.

Static type of c.m#?

• (T1, …, Tn) -> Map<dynamic,A>, or
• <K>(T1, …, Tn) -> Map<K,A>

The former. The latter would require us to introduce objects of generic function type, which the current proposal avoids. In order to do anything especially useful with the latter, we would also probably want generic function types. Basically, this moves us out of the strictly second-class polymorphism realm that this proposal sticks to.

Value of c.m#?

• (T1 a1, …, Tn an) => c.m<dynamic>(a1, …, an), or
• <K>(T1 a1, …, Tn an) => c.m<K>(a1, …, an) by a slight abuse of notation.

The former, again. The latter would be a generic function object, with a reified generic function type.

[chalin]

I'm sorry, you are right that the various sections of the proposal already made clear how tear-offs are being dealt with. I was partly thrown off by some of the terminology (as mentioned in #10), and by some of the broader statements made, for example, in this opening paragraph of the proposal details section:

Generic function types are second class in the type system, and do not need to be reified at runtime. Consequently: there is no syntax for a generic function type; type parameters may not be instantiated with generic function types; functions and methods may not be abstracted over generic functions.

I believe that above excerpt should be replaced with something like:

Currently in Dart, all type parameters of raw generic class types are implicitly instantiated with dynamic. In order extend this uniformly to generic functions, the rules of this proposal only allow closurization of instantiated generic functions. When no type arguments are provided, generic functions are implicitly instantiated with dynamic. Thus, while non-generic function types are denotable (via closurization expressions), because of the rules of this proposal, generic function types are not denotable---i.e., no Dart expression can be of a generic function type. Despite this, generic function types are reified, since passing type arguments to a generic method is a runtime operation.

I explain why below.

---

Let's work through the original excerpt.

Generic function types are second class

As defined in this proposal, GFTs are not denotable (i.e., no Dart expression can have a type that is a GFT) and hence GFTs are not even citizens (if a GFT cannot be denoted, then it cannot be assigned, passed as an argument, etc) so the qualification of "second class" doesn't apply. Maybe you meant "generic functions are second class"? But generic functions are first class: Dart functions are first class and making them generic does not result in a demotion of citizenship. I think I understand the manner in which you meant a kind of "second class"-ness: i.e., due to GFTs not being denotable and the unconventional nature of the reification of GFTs, as I explain below.

Generic function types ... do not need to be reified.

A reified type is one in which all the type's information is preserved at runtime, and available, say, via reflection. As is pointed out in this article, "passing type arguments to a constructor of a generic type is a runtime operation." I expect that the same must be true of passing type arguments to a generic functions. In that case, the type parameters of generic functions need to be represented in some form at runtime; this is what is being said in the reification section of the proposal, if I understand correctly. Thus, GFTs are reified, though, possibly not in a conventional manner.

If GFTs are not reified, then there will be some form of erasure. So are you claiming that, e.g., it will not be possible to use reflection to access the type parameters of a generic function?

I think that the key point is not whether GFTs are reified, but rather the how the proposal renders GFTs as non-denotable. The proposal interprets a "raw" generic function tear-off expression as being implicitly instantiated with dynamic for all type parameters, just like for raw generic classes. Hence, it forces a generic function to be (explicitly or implicitly) instantiated before closurization. (The result of this closurization is a regular function type and it is reified like any other type.)

Apologies if this comes across as being pedantic, but broad summarizing statements like the first one quoted above often help guide one's first impressions; and sometimes first impressions are hard to shake out, even if the proposal details tell a different story. Hopefully I have understood the proposal text well enough so that the statements above make some sense.

Let me know what you think.

[leafpetersen]

We're still not quite on the same page. The term "second class" is a term of art for this style of polymorphism in some communities - maybe confusing, but it also captures very well the restrictions in place here.

Let's write a universal function type as <T>.U -> V meaning that T is a type parameter to a universal type, which may appear free in U or V, and write universal functions as V f<T>(U x) => e meaning f is a universal function with type parameter T which may appear in the argument type U or the return type V. Then we have that universal function types are second class because they may not appear as sub-terms of other types (neither U nor V may be universal types), and because they may not be passed as type arguments to universal functions (f<<S>.S->S>) is always an invalid instantiation). The latter restriction preserves the former restriction under reduction. In this sense, universal function types are second class. To use the most precise terminology, this proposal is restricted to prenex polymorphism: types are split into mono-types (first-class, may be used anywhere) and poly-types (universal types which are second-class, may not be used as type arguments, and may not appear as sub-components of other types).

Similarly, universal functions themselves are second class in this proposal, because they may not be passed around as first class values. Only their instantiations may be passed around as first class values. Some concrete examples may help. Note: for these examples, assume that all implicit instantiation with dynamic has already been de-sugared.

// Id is a name for the type of polymorphic identity 
Id = <T>.T -> T

// id is the polymorphic identity function
T id<T>(T x) => x

// valid
int x = id<int>(3)

// valid, int is a mono-type, and Id<int> is a mono-type
List<Id<int>> intId = <Id<int>>[id<int>]

// not valid!  This would be valid with first class polymorphism,
// and listOfIds would be a list containing polymorphic functions.
// In this proposal, this is not legal.  Note that we are assuming
// that implicit instantiations have been de-sugared, so List<Id> 
// below does not mean List<Id<dynamic>> (which would be legal, 
// but which would mean something different), and similarly 
// <Id>[id] does not mean <Id<dynamic>>[id].
List<Id> listOfIds = <Id>[id]

// not valid!  This would be valid with first class polymorphism,
// but is not valid here.
int x = listOfIds[0]<int>(3)

Note that one of the points of confusion here is that Dart has a notion of implicit instantiation. So at the syntax level, you can in Dart currently write things like:

typedef T Id<T>(x:T)

List<Id> listOfIds = ....

Semantically however, this does not correspond to instantiating the List type with the polymorphic identity type (which would require a richer type system). Instead, it simply means that Id is implicitly instantiated with dynamic to produce a mono-type, which is then used to instantiate List.

This then brings us to the second point, about reification of generics. In this proposal (and in any useful proposal) the parameters to generic functions will be reified. That is the generic function:

List<T> singleton<T>(x:T) => <T>[x]

will always produce a list whose dynamic reified type is List<T> for whatever T was passed in as the type argument. This is essential for making things integrate with checked mode.

However, because this proposal is limited to prenex polymorphism, universal function types themselves are never reified. The implementation does not have to ever represent universal function types as reified type objects. If the listOfIds construction was valid from the example above, then universal function types would need to be reified so that the List object would have the correct reified type. But for the prenex fragment as given, this is not required.

Of course, all of this changes if the language team feels that we should implement a richer type system in which polymorphic functions (and types) can be used in a more first-class fashion. There's a bit of discussion in the proposal about the implications of this. I don't think it's too big of a deal, but it does introduce some implementation complexity (since currently no types with binding structure need to be reified).

[chalin]

The term "second class" is a term of art for this style of polymorphism in some communities

Oops, sorry! I wasn't aware of that, but it makes sense to have such a term. Unfortunately I took "second class" to be a mention of citizenship. Thanks for pointing that out.

List<T> singleton<T>(x:T) => <T>[x]
will always produce a list whose dynamic reified type is List for whatever T was passed in as the type argument.

By List in "whose dynamic reified type is List for whatever T" do you mean List<dynamic> or List<T>?

[leafpetersen]

Aargh, markdown fail - if you leave off the back quotes around the generic instantiation syntax, then markdown drops the type arguments (so List <T> renders as List). Fixed inline, but just to be clear:

By List in "whose dynamic reified type is List for whatever T" do you mean List or List

Should be "will always produce a list whose dynamic reified type is List<T> for whatever T was passed in as the type argument". So singleton<int> will always produce something whose runtime type is List<int>.

[chalin]

Firstly an apology. My understanding of the theory underlying polymorphism was only enough to allow me to loose myself in left field, it seems. Thanks for your explanations. It has been instructive, but sorry for the extra burden that entailed.

I dusted off my copy of Pierces Types and Programming Languages, and read through some of Greg Morrisett's course notes on polymorphism. That helped.

So Dart's generic classes are already constrained to predicative prenex polymorphism with F-bounded quantification, right? Hence, the proposal adds support for generic functions in a manner that is consistent with the current support for classes?

I used to (erroneously) think that Dart's classes were first class citizens , since Type t = int is legal; I hadn't put that much more thought into it. But then one can't write Type t = List<int>, although using the raw type is fine. Regardless one can't to much with the Type t after its been assigned to. So I guess that classes (and methods) are second class citizens and second class polymorphically too. Thanks again.