Erik Ernst eernstg

Dispatching Parameters

Author: eernst@

Status: Under discussion.

This document is an informal specification of the dispatching parameter feature in Dart. That feature allows a function parameter to implicitly serve as the receiver for member accesses (e.g., calling instance methods) in the body of the function, similar to the ability of the object denoted by

This document is now obsolete, please refer to the current version.

Optional new

Author: eernst@.

Version: 0.1 (2017-08-15)

Status: Under discussion

This document is now obsolete, please refer to the current version.

Optional const

Author: eernst@.

Version: 0.1 (2017-08-10)

Status: Under discussion

Anonymous Extension Methods

Author: eernst@

Status: Under discussion.

This document is an informal specification of the anonymous extension method feature in Dart. This feature allows for writing a function in an expression whose semantics makes it similar to an instance method on the result of an

This document is now obsolete, please refer to the current version.

Feature: Generalized Void

Author: eernst@

Status: Under implementation.

This document is an informal specification of the generalized support in

This document is now obsolete, please refer to the current version.

Feature: Generic Function Type Alias

Status: Under implementation.

This document is an informal specification of a feature supporting the definition of function type aliases using a more expressive syntax than the one available today, such that it also covers generic function types. The feature also introduces syntax for specifying function types directly, such

This document is now obsolete, please refer to the current version.

Feature: Generic Method Syntax

This document is an informal specification of the support for generic methods and functions which has been implemented in dart2js with option --generic-method-syntax, starting with commit acc5f59. In SDK 1.21 this feature is available by default (i.e., also without the option) in the virtual machine and the analyzer, as well as in dart2js.

The motivation for having this feature is that it enables partial support for generic methods and functions, thus providing a bridge between not having generic methods and having full support for generic methods. In particular, code declaring and using generic methods may be type checked and compiled in strong mode, and the same code will now be acceptable in standard (non-

	// Copyright (c) 2017, the Dart project authors. Please see the AUTHORS file
	// for details. All rights reserved. Use of this source code is governed by a
	// BSD-style license that can be found in the LICENSE file.

	grammar Dart;

	@parser::header{
	import java.util.Stack;
	}

	Require Import List.
	Require Import voidness.

	(* ---------- Dart types ---------- *)

	(* Object *)
	Definition ct_Object : ClassTypes := (Object, nil) :: nil.
	Definition dt_Object := dt_class ct_Object.

	(* A<Object> *)

	Require Import Coq.Program.Basics.
	Require Import List.

	Inductive Name : Set := Object \| A \| B \| Iterable \| List.

	Inductive DartType : Set :=
	\| dt_void : DartType
	\| dt_dynamic : DartType
	\| dt_class : list (Name * list DartType) -> DartType (* Incl. all supertypes *)
	\| dt_function : DartType -> list DartType -> DartType