Typedefs and generic function types - some clarification and/or updates needed

[chalin]

Executive summary

Dart currently has support for generic function type (GFT) aliases via typedefs. Hence some statements in the proposal might not be quite accurate: e.g.,

• Lack of syntax for GFTs (though there is lack of syntax for generic functions).
• GFT's cannot be used to instantiate type parameters.

If these statements are still considered accurate then at a minimum, the proposal should make clear that the unqualified use of the term "generic function type" (GFT) excludes GFT aliases, i.e., those syntactic entities inside typesdefs that look like GFTs.

Details

Here is an excerpt from the "Proposal" subsection (emphasis mine):

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.

Syntax. In a sense, there is syntax for generic function types (though not for generic functions). It is defined as part of the Dart grammar non-terminal functionTypeAlias:

functionTypeAlias:
    functionPrefix  typeParameters? formalParameterList ;
functionPrefix:
    returnType? identifier

If you drop the terminating semicolon then the resulting production defines GFTs.

Example. Here is an example of the syntax adapted from a A Tour of the Dart Language section on typedefs

typedef int Compare<T>(T a, T b);

class SortedCollection<T> {
  Compare<T> compare;
  SortedCollection(this.compare);
}

Reification. GFT aliases are indeed not reified:

int sort(int a, int b) => a - b;
SortedCollection c = new SortedCollection<int>(sort);

void main() {
  print(sort.runtimeType);      // -> (int, int) => int
  print(c.compare.runtimeType); // -> (int, int) => int
}

Arguments to type parameters. GFT aliases can be used as arguments to type parameters:

typedef int CompareInt(int a, int b);

class SortedCollection2<T, U extends Compare<T>> {
  U compare;
  SortedCollection2(this.compare);
}

void more() {
  SortedCollection2 c2 = new SortedCollection2<int,CompareInt>(sort);
  //...
  int sortString(String a, String b) => a.length - b.length;
  SortedCollection2 c2s = new SortedCollection2<String,Compare<String>>(sortString);
  //...
}

Typedefs. I think that some mention should be made in the proposal concerning typedefs and their current use in defining GFT aliases. I assume that there will be no unexpected "feature interactions" between this proposal and typesdefs (a statement to this effect could be made explicitly).

typedef S T2S<S,T>(T x);
typedef Option<S> OptionMap<S,T>(T2S<S,T> f);

abstract class Option<T> {
  Option<S> map<S>(T2S<S,T> f);  // Ok
  OptionMap<S,T> map<S>;         // Illegal, ... or maybe not?
  T get val;
}

[leafpetersen]

I avoided going into this in the proposal, but perhaps I should add some discussion. Here's where my thinking was when I was working through this.

First, some background (sorry if this is obvious, but just to get our terminology on the same page). Typedefs in Dart are not actually generic function types (universal types) even though they look a lot like them. What they are is type functions (or type constructors). That is, they are functions from Type to Type, not types themselves. The difference is small, but crucial. The point is that a universal type is a type (or a type schema or... something depending on what type system you live in), whereas a type constructor (Dart typedef) is a thing which can be given some arguments and will produce for you a type as a result. In the case of Dart, they are limited to producing function types, which is one of thing things that makes them so tantalizingly close to being universal function types.

So to be precise, the original two statements that this issue is questioning:

• Lack of syntax for GFTs (though there is lack of syntax for generic functions).
• GFT's cannot be used to instantiate type parameters.

are in fact accurate: you cannot in Dart write the type of a generic function (only a generic which produces a function type); and you cannot instantiate a type parameter with a generic function type (you can only instantiate the typedef and use the result to instantiate a type parameter).

I don't make this distinction to be pedantic - there are two different notions there, and the difference is really important. It is also true though, that type constructors provide all of the basic functionality needed to build universal types. So if we ignore backwards compatibility, it would work perfectly well to take the interpretation that:

• A typedef introduces a constructor function
• An instantiation of a typedef produces the appropriate type
• An uninstantiated use of a typedef is interpreted as denoting the appropriate universal type

So then we would have that typedef T Id<T>(T x) means that Id is a type function; Id<int> f; means that f has type int -> int; and Id g; means that g is a generic function of type Forall<T>.T->T, which could then be called as g<int>(3). If we wanted to allow generic function types (universal types) to be first class and reified, then List<Id> would denote the type of lists of polymorphic identity functions, whereas List<Id<int>> would denote the type of lists of functions from integers to integers.

This is all grand, except for that pesky "ignore backwards compatibility part". Unfortunately, Id g; already means something in Dart: it means Id<dynamic> g;. So taking the interpretation I suggest above would be a fairly large breaking change. A function signature void accept(Id f) would previously have meant that accept took any function of the appropriate arity without complaint (that is, it expected a dynamic->dynamic), but would now mean that it expected only things of the appropriate generic type. Similarly, the query (f is Id) would previously have returned true for any function of the appropriate arity, but would now presumably return false unless f happened to be the polymorphic identity function.

Assuming that we didn't want to bite the bullet on the breaking change, this could be worked around fairly easily. One approach would be to simply have different syntax for introducing a type function versus a generic function type:

// Id is a type function from types to types
typedef T Id<T>(T x);
// GId is a type (of generic functions)
typedef generic T GId<T>(T x);

Another approach would be to have syntax for lifting an existing typedef up to a universal type: e.g.

typedef T Id<T> (T x);

// Forall is a new keyword, and is a higher-kinded type operator
// which lifts a type function up to a universal type
// Forall<Id> ==> Forall<T>.T -> T
Forall<Id> g = ....;

The lifting could be done by picking a new keyword as above (minor breaking change), or by using some new syntax or tokens (/Id/, or <<Id>>, or &Id, or hopefully something better) that didn't conflict with existing syntax.

In any case, since I decided to push this proposal in the direction of second-class generics, the entire question of syntax for generic function types is fairly moot for the time being. If the committee feels that a more powerful form polymorphism is desired I can revisit this.

To address your last question about interactions between existing Dart typedefs and generic functions... I don't currently believe that there are any such interactions. To your concrete example:

typedef S T2S<S,T>(T x);
typedef Option<S> OptionMap<S,T>(T2S<S,T> f);

abstract class Option<T> {
  Option<S> map<S>(T2S<S,T> f);  // Ok
  OptionMap<S,T> map<S>;         // Illegal
  OptionMap mapTearOff = map; // Legal if we allow implicit instantiation, means mapTearOff is OptionMap<dynamic, dynamic>
  OptionMap mapTearOff = map<dynamic>; // Legal, means mapTearOff is OptionMap<dynamic, dynamic>
  T get val;
}

Hopefully that addresses the bulk of this issue? Based on this and any follow up discussion I'll try to distill out something to add to the proposal text to clarify this as needed.

[chalin]

Firstly I would like to emphasize that the core of the proposal seems fine.

As you have suggested, one of the points raised by this issue has to do with terminology. There is an object language vs. meta language clash with respect to the term "generic function type".

Let's look at common usage (object language terminology) first. In Chapter 2 of Dart Up and Running typedef is defined as follows:

A typedef, or function-type alias, gives a function type a name.

Also, the first hit when Googling "dart function type" is this article by Gilad which states that:

a typedef defines a function type.

Now I'll write -type- to mean a Dart (i.e., object language) type, and ^type^ to mean a meta / type-theoretic type (think of the ^ as pointing up for the more abstract concept).

Since typedefs can be generic, they support the definition of generic function -types- (-GFTs-). You were correct earlier in stating that a -GFT- corresponds to a type constructor / operator in our meta theory. Reserving the unqualified term "generic function type" to mean ^GFT^ in the proposal is quite fine, as long as typedefs are always referred to as function type aliases in the proposal. I'll submit a PR with a small section for settling terminology; let me know what you think.

[leafpetersen]

Agreed that the terminology is unclear - put another way, the phrase "generic function type" can be parsed as "generic (function type)" (that is, functions types which are generic, the sense in which dart has GFTs), or as "(generic function) type" (that is, the type of generic functions, the sense in which dart does not have GFTs). Thanks for the PR - I may just take a more global pass to sort out the terminology though, rather than making the reader keep a terminology look aside table in their head. Any suggestions as to a better term for "(generic function) type" that won't cause confusion? Universal function type or polymorphic function type are two obvious candidates.

[chalin]

Universal function type was the first that came to mind. Since nowhere in the current proposal is GFT taken to mean a typedef, I figured it was simplest at this point just to add a note about terminology.