Пишу книгу: Readings in Java Type System

Добрый день.
Квартиру купил, сына родил, компанию создал — пора написать книгу.
Поскольку я теперь профессионально занимаюсь Java Core (преподаю, составляю программы обучения, руковожу компанией, занимающейся образованием), то это определило выбор темы — основы Java.
Поскольку хочется заниматься все же чем-то “академическим” — это определило “смещение темы” — Система Типов, а не учебник по Java.
Поскольку написать 500 страниц не хватит ни настойчивости, ни времени, ни мотивации, то это и определило стиль — Readings (сборник чужих статей, собранных в главы, с авторским введением к каждой статье). Примером может служить — “Readings in Database Systems”.
.
Дополнительная причина — летом 2013 выходит Java 8 с серьезно расширенной системой типов (type annotations, extentions methods, lambdas, ...) - хотелось бы предоставить набор характерных примеров и статей по теме.
.
Эта книга о том, что такое тип в Java 8 и какие алгебраические операции и алгебраические структуры определены на множестве типов.
1. JAVA TYPE SYSTEM BASICS
“A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.” == “Система типов — это гибко управляемый синтаксический метод доказательства отсутствия в программе определенных видов поведения при помощи классификации предложения языка по разновидностям вычисляемых ими значений” [Types and Programming Languages. Benjamin C. Pierce]
Что такое тип в Java? Как типы соотносятся с классами? Можно ли конструкторы типов свести к объявлению классов? Java 8 задает бесконечное количество типов, счетное оно или нет? Типы времени компиляции и типы времени исполнения — в чем разница?
.
1.0 типы времени компиляции и типы времени исполнения
В Java различают типы времени компиляции и типы времени исполнения. Тип времени исполнения имеет область видимости — множество типов загрузившихся тем же ClassLoader.
“Sometimes a variable or expression is said to have a ‘run-time type’. This refers to the class of the object referred to by the value of the variable or expression at run-time, assuming that the value is not null.
The correspondence between compile-time types and run-time types is incomplete for two reasons:
1. At run-time, classes and interfaces are loaded by the Java virtual machine using class loaders. Each class loader defines its own set of classes and interfaces. As a result, it is possible for two loaders to load an identical class or interface definition but produce distinct classes or interfaces at run-time. Consequently, code that compiled correctly may fail at link time if the class loaders that load it are inconsistent.
...
2. Type variables (§ 4.4) and type arguments (§ 4.5.1) are not reified at runtime. As a result, the same class or interface at run-time represents multiple parameterized types (§ 4.5) from compile-time. Specifically, all compile-time invocations of a given generic type declaration (§ 8.1.2, § 9.1.2) share a single run-time representation.” [JLS 4.12.6]
Глава находится отдельно здесь.
.
1.1 static / dynamic type system
“The Java programming language is a statically typed language, which means that every variable and every expression has a type that is known at compile time.” [JLS 4]
.
1.2 strong / weak type system
“The Java programming language is also a strongly typed language, because types limit the values that a variable (§ 4.12) can hold or that an expression can produce, limit the operations supported on those values, and determine the meaning of the operations. Strong static typing helps detect errors at compile time.” [JLS 4]
.
1.3 Универсальные и экзистенциальные типы.
“The relationship of wildcards to established type theory is an interesting one, which we briefly allude to here. Wildcards are a restricted form of existential types. Given a generic type declaration G< T extends B >, G< ? > is roughly analogous to Some X <: B. G< X >” [JLS7 4.5.1]
.
1.4 Номинальные, структурные и Intersection/Compositional типы.
.
1.5 Anonimous inner classes как слабая версия замыканий.
.
1.6 Полиморфизм
“Monomorphic programming languages may be contrasted with polymorphic languages in which some values and variables may have more than one type. Polymorphic functions are functions whose operands (actual parameters) can have more than one type. Polymorphic types are types whose operations are applicable to values of more than one type.” [Luca85]
Parametric polymorphism is obtained when a function works uniformly on a range of types: these types normally exhibit some common structure.”
Parametric polymorphism is so called because the uniformity of type structure is normally achieved by type parameters ...”
“Our classification of polymorphism ... refines that of Strachey by introducing a new form of polymorphism called inclusion polymorphism to model subtypes and inheritance. Parametric and inclusion polymorphism are classified as the two major subcategories of universal polymorphism ...”
“Universally polymorphic functions will normally work on an infinite number of types (all the types having a given common structure), while an ad-hoc polymorphic function will only work on a finite set of different and potentially unrelated types.”
“In terms of implementation, a universally polymorphic function will execute the same code for arguments of any admissible type, while an ad-hoc polymorphic function may execute different code for each type of argument.”
“There are two major kinds of universal polymorphism, i.e., two major ways in which a value can have many types. In parametric polymorphism, a polymorphic function has an implicit or explicit type parameter, which determines the type of the argument for each application of that function. In inclusion polymorphism an object can be viewed as belonging to many different classes which need not be disjoint, i.e. there may be inclusion of classes. These two views of universal polymorphism are not unrelated, but are sufficiently distinct in theory and in practice to deserve different names.”
“There are also two major kinds of ad-hoc polymorphism. In overloading the same variable name is used to denote different functions, and the context is used to decide which function is denoted by a particular instance of the name. We may imagine that a preprocessing of the program will eliminate overloading by giving different names to the different functions; in this sense overloading is just a convenient syntactic abbreviation. A coercion is instead a semantic operation which is needed to convert an argument to the type expected by a function, in a situation which would otherwise result in a type error. Coercions can be provided statically, by automatically inserting them between arguments and functions at compile time, or may have to be determined dynamically by run-time tests on the arguments.”
[Luca85]
Итого в Java 8 есть 2 примера универсального полиморфизма (generics, subtyping) и два типа специального (overloading, coercion). Все три (кроме overriding) работают в compile time, overriding работает в runtime, второе название — динамическая диспетчеризация. Ограничения (какие?) динамической диспетчеризации приводят к появлению Double/Multiple dispatching и pattern Visitor (точно?).
Итого, прогресс достигается за счет определения операций не на отдельных типах, а на неким образом определенных семействах типов (в случае универсального полиморфизма — на бесконечных).
Inclusion полиморфизм обогащает систему типов структурой теории множеств с операцией включения и пересечения.
А именно:
номинальный подход приводит к введению нового именованного типа как подмножества уже существующего:

class Y extends X {}
или подмножества пересечения существующих
interface AB implement A, B {}
и проверки включения в момент компиляции
(пример?)
или выполнения
boolean aIsB = a instanceof B;
boolean aIsB = a.getClass().isAssignableFrom(b.getClass());
A asA = a.getClass().cast(b);
void f(B b) {A asA = (A) b;} 
ограниченная версия структурного подхода (intersection types) приводит с созданию типа с ограниченной областью видимости как пересечения:
public <T extends A & B> void f(T arg);
Ввиду работы type erasure возможны проверки исключительно во время компиляции.
.
1.7 ATD
.
Вопрос: какой тип переменной ex?
try {...} catch (RuntimeException | Error ex) {...}
.
Вопрос: какой тип литерала null? Есть ли у него постоянный тип или он зависит от контекста? Каков этот тип в примере ниже?
class C {
    void f(Number x) {}
    void f(Double x) {}
    void f() {f(null);}
}
.
[Luca85] Luca Cardelli, Peter Wegner, “On understanding types, data abstraction, and polymorphism”, 1985
.
2. OOP
James Gosling, Bill Joy, Guy Steele, Gilad Bracha, “The Java Language Specification, Java SE 7 Edition”, 2007
Brian Goetz, “Interface evolution via virtual extension methods”, 2011
“JSR-000335 Lambda Expressions for the Java Programming Language 0.5.1 Early Draft Review 2”
.
3. GENERICS
3.1 generics
Java Generics — реализация параметрического полиморфизма в Java. Параметрический полиморфизм впервые в полной мере появился в ML (точно?). Теоретической основой для generics + wildcards послужили universal/existential types (точно?). System F?.
3.2 wildcards
“The relationship of wildcards to established type theory is an interesting one, which we briefly allude to here. Wildcards are a restricted form of existential types. Given a generic type declaration G< T extends B >, G< ? > is roughly analogous to Some X <: B. G< X >.
.
Historically, wildcards are a direct descendant of the work by Atsushi Igarashi and Mirko Viroli. Readers interested in a more comprehensive discussion should refer to On Variance-Based Subtyping for Parametric Types by Atsushi Igarashi and Mirko Viroli, in the Proceedings of the 16th European Conference on Object Oriented Programming (ECOOP 2002). This work itself builds upon earlier work by Kresten Thorup and Mads Torgersen (Unifying Genericity, ECOOP 99), as well as a long tradition of work on declaration based variance that goes back to Pierre America’s work on POOL (OOPSLA 89).
.
Wildcards differ in certain details from the constructs described in the aforementioned paper, in particular in the use of capture conversion (§ 5.1.10) rather than the close operation described by Igarashi and Viroli. For a formal account of wildcards, see Wild FJ by Mads Torgersen, Erik Ernst and Christian Plesner Hansen, in the 12th workshop on Foundations of Object Oriented Programming (FOOL 2005).” [JLS7 4.5.1]
.
Базовый словарь: parameterized classes, parameterized methods, parametric polymorphism, wildcards, type erasure, wildcard capture, raw types, type variable, type argument, dummy type variable, unbounded wildcard, bounded wildcards, covariance, contravariance, bridge methods.
Расширенный словарь: type inference, use-site variance, declaration-side variance, existential types, universal types, ?sound type, ?infinite type, ?virtual types,
Основная литература:
Gilad Bracha, “Generics in the Java Programming Language”, 2004
Gilad Bracha, Neal Gafter and others, “Adding Wildcards to the Java Programming Language”, 2004
Расширенная литература:
Luca Cardelli, Peter Wegner, “On understanding types, data abstraction, and polymorphism”, 1985
John Mitchell, Gordon Plotkin, “Abstract Types Have Existential Type”, 1988
Atsushi Igarashi, Mirko Viroli “On variance-based subtyping for parametric types”, 2002 (точно?)
.
4. ANNOTATIONS
.
5. Project Lambda
.
6. AOP

Семантика
Операционная семантика.
Денотационная семантика.
Аксиоматическая семантика.

Допустимые теги: blockquote, code, em, pre, i, li, ol, strike, strong, u, ul, a.
Ctrl + Enter
Допустимые теги: blockquote, code, em, pre, i, li, ol, strike, strong, u, ul, a.
Ctrl + Enter

Сколько ж это надо отбашлять, чтобы все твой топики резко вверх подтянулись ...

Прикинь размер того, что уже написал на ДОУ. А ещё в блогах... Банально, в тысячах знаков. 500 страниц — фигня по сравнению с этим.

Единственный барьер — пишешь не интересно. По крайней мере джуны не осилят. Объясню почему: пытаешься лгать избегать личного мнения подавать информацию наукообразно. Скажу точнее: обходишь стороной самые важные аспекты, отгораживаешься терминологией и клише.

Обычный человек (не учёный и не бюрократ) скажет КГ/АМ.

Цель языка программирования — обучить компьютер понимать человека. Это на 100% гуманитарная технология, ориентированная на людей, на их понимание, их восприятие, их память, их возможности комуникации. Если ты не учишь людей, а лишь констатируешь факты — кому нужна твоя книга? Кто знает — знает, а кто не знает — ничего и не поймёт. Если на курсах то же самое — мне жаль тех, кто заплатил деньги и потратил зря время.

Попробуй всё же написать книгу. Если получится — только тогда всерьёз занимайся курсами. Если нет — пробуй пока не получится, бумага всё стерпит. Либо найми человека, который сможет перевести «с русского на русский», и тогда сам прочитай. Сейчас пишешь как программист — надеешься что по ту сторону экрана компьютер с компилятором и мегатоннами данных, дабы всё это переварить. Но реально там человеки. Знания которых отличаются от твоих чуть более чем полностью.

// Жаль нет программы, которая бы заменила слова и выражения, не входящие в 6000 употребимых — на «бла-бла-бла».

написать 500 страниц не хватит ни настойчивости, ни времени, ни мотивации
Зачем вообще тогда что то писать ? срубить денег ? попиарить курсы ?
Надеюсь большинство авторов использует не такой подход...иначе чего требовать от начинающих программистов начитавшихся «таких» книжек...

Полагаю, Вы просто не посмотрели ту книгу, на которую я бросил ссылку.
Это один из ведущих учебников для старшекурсников Стенфордского Университета по Базам Данных.

Все равно с таким настроением:

написать 500 страниц не хватит ни настойчивости, ни времени, ни мотивации
лучше вообще ничего не писать...

А сколько книг написали Вы?

Столько же сколько и Вы — ни одной.
В моем понимании книга должна быть книгой, написана с интересом и душой, тогда в ней будет толк...Сборник чужих статей в одну публикацию как сочинение в школе — переписал понемногу из критики и вуаля...все! готово! тока над душой не стойте...

Что требуется от сообщества? (Зачем я это прочитал?)

(Зачем я это прочитал?)
, руковожу компанией, занимающейся образованием

Ищу идейных товарищей: предложить другой материал, покритиковать, ...
Я сюда буду добавлять (уже добавляю) ссылки, текст.

Как переводчик более чем 40 книг по IT и практикующий программист, одобряю! Выходит масса (многостраничной, дорогой) литературы, представляющей собой сокращенный пересказ документации API, но очень мало таких, по которым можно эффективно учиться и учить.

Рад познакомится:)
Возможно, у меня будет интересное предложение относительно издания книги исключительно в электронном виде. Собственно, интересно Ваше мнение:
1) насколько перспективно издать книгу исключительно на английском языке и только в электронном виде (Amazon)? Цены, как я понимаю, порядка 29$-69$, интересен типичный «тираж».
2) интересно ли вам участие (верстка или помощь с поиском верстальщика, работа c Amazon, корректура на английском) в таком проекте при существенной доле прибыли (технические редакторы у меня есть — сильные академические computer science специалисты из Москвы/Питера)? Или Вы могли бы кого-нибудь посоветовать?

Боюсь, что разочарую вас, Иван. Дело в том, что я переводил с английского на русский для издательств Киева и Москвы, а не наоборот. По пунктам: (1) — ничего не могу сказать, не знаком с тамошним рынком. (2) — чукча не верстальщик и не носитель языка (английского). Могу свести с редактором из Вильямс Пресс (он же работает в Диалектике). Когда-то у него была идея заказать кому-то написание книги вроде вашей. Мой skype: mukhin.nick.

Понял, спасибо.

Лучше найми его в качестве копирайтера. Хотя бы ради эксперимента, на пару тысяч знаков. Или на вводный курс. Как пишет — посмотри коменты на ДОУ. Хорошо написанная книга продаётся в разы лучше! Плохо написанную продаёт только обложка (коих уже выпущены сотни).

Квартиру купил, сына родил, компанию создал — пора написать книгу.

Держите нас в курсе.

Подписаться на комментарии