## Appendix C: Bibliography

Pierce, Benjamin C.. (2002). Types and Programming Languages.

Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex. (2015). The Java Language Specification. Java SE 8 Edition. Retrieved from http://docs.oracle.com/javase/specs/jls/se8/jls8.pdf

Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex. (2012). The Java Language Specification. Java SE 7 Edition. Retrieved from http://docs.oracle.com/javase/specs/jls/se7/jls7.pdf

Nielson, Flemming and Nielson, HanneRiis. (1999). Type and Effect Systems. Retrieved from http://dx.doi.org/10.1007/3-540-48092-7_6

Crary, Karl and Weirich, Stephanie and Morrisett, Greg. (2002). Intensional polymorphism in type-erasure semantics. Retrieved from http://journals.cambridge.org/article_S0956796801004282

Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip. (2001). Featherweight Java: a minimal core calculus for Java and GJ.

Cameron, Nicholas and Drossopoulou, Sophia and Ernst, Erik. (2008). A Model for Java with Wildcards. Retrieved from http://dx.doi.org/10.1007/978-3-540-70592-5_2

Cameron, Nicholas. (2009). Existential Types for Variance — Java Wildcards and Ownership Types. Retrieved from http://www.doc.ic.ac.uk/~ncameron/papers/cameron_thesis.pdf

Summers, Alexander J. and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia. (2010). Towards a semantic model for Java wildcards.

Wehr, Stefan and Thiemann, Peter. (2008). Subtyping Existential Types. Retrieved from http://www.informatik.uni-freiburg.de/~wehr/publications/Wehr_Subtyping_existential_types.pdf

Igarashi, Atsushi and Nagira, Hideshi. (2007). Union Types for Object-Oriented Programming. Retrieved from http://www.jot.fm/issues/issue_2007_02/article3/

King, Gavin. (2013). The Ceylon Language. Red Hat, Inc.. Retrieved from http://ceylon-lang.org/documentation/1.0/spec/pdf/ceylon-language-specification.pdf

Laurent, Olivier. (2012). Intersection types with subtyping by means of cut elimination.

Steen, Hallvord and Aubourg, Julian and van Kesteren, Anne and Song, Jungkee. (2014). XMLHttpRequest Level 1.

Kuizinas, Gajus. (2014). The Definitive Guide to the JavaScript Generators. Retrieved from http://gajus.com/blog/2/the-definetive-guide-to-the-javascript-generators

Fowler, Martin. (2004). Inversion of Control Containers and the Dependency Injection pattern. Retrieved from http://martinfowler.com/articles/injection.html

Prasanna, Dhanji R. (2009). Dependency Injection: Design Patterns Using Spring and Guice.

Zhu, He and Jagannathan, Suresh. (2013). Compositional and Lightweight Dependent Type Inference for ML. Retrieved from http://dx.doi.org/10.1007/978-3-642-35873-9_19

Hudli, Shrinidhi R. and Hudli, Raghu V.. (2013). A Verification Strategy for Dependency Injection.

Betts, Dominic and Melnik, Grigori and Simonazzi, Fernando and Subramanian, Mani. (2013). Dependency Injection with Unity.

Knol, Alex. (2013). Dependency injection with AngularJS.

1. A brief introduction can be found at http://www.cs.cornell.edu/~ross/publications/mixedsite/tutorial.html. In general, we refer the reader to [Pierce02a]
2. One can interpret this similar to delegate methods, that is, instead of writing r.binding().getType(), a method r.getType()\{return binding().getType(); is defined.
4. See for definitions of metatype properties.
5. That is, for application developers not providing a library or a public API available to other vendors, member access modifiers behave almost similar to modifiers known from Java.
6. See N4JS Specific Classifiers for definitions of metatype properties. Note that $r.receiver$ always refers to a type declaration in the context of an expression as the receiver type of $r$. The declaring type of the member declaration is considered to be the receiver type of the member reference rather than the type that originally declares the member declaration.
7. Note the Java-like access restriction for members of visibility protected or protected@Internal to code that is responsible for the implementation of that object. [Gosling15a(p.S6.6.2, p.p.166)]
8. string, boolean, number, any, null
9. This conflicts with the implicit parameter arguments introduced by the transpiler when wrapping the script/module into a definition function.
10. In the N4JS IDE, type annotations are highlighted differently than ordinary code.
11. The notation $|T|$ used in [Gosling12a] conflicts with the notation of cardinality of sets, which we use in case of union or intersection types for types as well. The notation used here is inspired by [Crary02a], in which a mapping is defined between a typed language $\lambda$ to an untyped language $\lambda$o.
12. Although raw type usage is prohibited, the N4JS validator interprets raw types according to the first case, which may lead to consequential errors.
13. in the Java 8 spec and compiler, they are called type variables, which are types as well
14. The rationale for having this limited implementation of type is that API designers already want to start providing hints where later only 32-bit integers will be used. For the time being, this is checked neither statically nor at runtime!
15. This is a consequence of the syntax definition.
16. For type theory about union types, [Pierce02a(p.15.7)] and [Igarashi07a], other languages that explicitly support the notion of union type include Ceylon [King13a(p.3.2.4/5)]
17. This is different from Ceylon ( [King13a(p.3.2.3)]), in which the union is defined to be the same type as A. Although the meaning of same is not clear, it is possibly used as a synonym for equivalent.
18. See Example Type Examples, Class Hierarchy for class definitions.
19. For type theory about intersection types, see [Pierce02a(p.15.7)] and [Laurent12a], other languages supporting explicit notion of intersection type include Ceylon [King13a(p.3.2.4/5)].
20. This rule is a generalization of the subtyping rules given in [Laurent12a] Table 2, ${\cap }_{l}^{1}$ and ${\cap }_{l}^{2}$
21. This rule is a generalization of the subtyping rules given in [Laurent12a] Table 2, ${\cap }_{r}$
22. In Ceylon, for a given union type $U={T}_{1}|{T}_{2}$ and intersection type $I={T}_{1}&{T}_{2}$ (with ’|’ is union and ’&’ is intersection), ${T}_{1}\phantom{\rule{1.0mm}{0ex}}<\text{:}\phantom{\rule{1.0mm}{0ex}}U$ and ${T}_{2}\phantom{\rule{1.0mm}{0ex}}<\text{:}\phantom{\rule{1.0mm}{0ex}}U$ is true, and ${T}_{1}\phantom{\rule{1.0mm}{0ex}}<\text{:}\phantom{\rule{1.0mm}{0ex}}I$ and ${T}_{2}\phantom{\rule{1.0mm}{0ex}}<\text{:}\phantom{\rule{1.0mm}{0ex}}I$ is true. We should define that as well (if it is not already defined). Cf [King13a(p.3.2.4/5)]
23. See Example Type Examples, Class Hierarchy for class definitions.
24. see "Covariance and contravariance with unions and intersections" at http://ceylon-lang.org/documentation/1.1/tour/generics/
25. The classifier type is, in fact, the type type or metatype of a type. We use the term classifier type in the specification to avoid the bogus type type terminology.
26. The phenomenon is described in IDEBUG-263
27. E.g., for given class A{ foo(A):A{}} class B{ foo(B):B{}}, a class C could be defined as class C{ foo(union{A,B}):intersection{A,B}{}}. In this case it would then be a syntactical problem (and even worse - a conceptual problem) of how to call the super methods defined in A and Bfrom C.
28. $accessorPair\left({m}_{1},{m}_{2}\right)$ is defined as follows: $\left(\mu \left({m}_{1}\right)=\text{getter}\wedge \mu \left({m}_{2}\right)=\text{setter}\right)\vee \left(\mu \left({m}_{1}\right)=\text{setter}\wedge \mu \left({m}_{2}\right)=\text{getter}\right)$
29. not yet implemented
30. In order to emulate method overloading, union types are to be used.
31. [ECMA15a(p.p214)], ClassBody : ClassElementList indicates that it is possible to have the same name for instance and static members.
32. version 4.0
33. This cannot be done w/o null/undefined analysis
34. This is required, because in Javascript a getter shadows a corresponding setter defined further up in the prototype chain; likewise a setter shadows a corresponding getter.
35. Thus, the type of one accessor is not used to infer the type of the other one. E.g., from set x(string s), we cannot infer get x() to return string — instead, the getter is inferred to return any.
36. The technical reason for this rule is the way properties are stored in JavaScript. Take for an example subclass-write access : class C { static f="a";} with class D extends C { }. Now the data field f on C can also be queried using D (var q=D.f;) but writing (D.f="b";) would introduce a newly created property f on class D, which differs from the one defined on C. It would do this without explicitly overriding the inherited property. Subsequent reads to D.f would route to this ’accidentally’ introduced property. Such a behavior would not be expected and therefore has been disallowed. Note that this write restriction applies to data-fields and to field setters.
37. There had been the idea of preventing static members of being consumed. However, this would break the type subtype relation.
38. C could either be a class or an interface.
39. As defined in Function Type for function types.
40. This kind of typing is used by TypeScript only. By defining a structural typed classifier or reference, it basically behaves as it would behave – without that modifier – in TypeScript.
41. We enforce programmers of N4JS to use nominal typing, therefore, it is not possible to bypass that principle by declaring a type as structural for normally defined classes (except those explicitly derived from N4Object).
42. Since this is already prevented by the parser (the tilde is interpreted as an unary operator), error messages are likely to look a little strange.
43. Note that due to this relaxed definition (compared with definition-site structural types) it is possible to pass an N4Object instance to a function of method with a declared structural type parameter.
44. This is already constrained by the grammar.
46. Even in this case, the function will actually be called with the callback method which is then created by the transpiler. However, the callback is not given in the N4JS code).
47. i iterates over all boundaries
48. i iterates over all type args
49. Only Function implements the ECMAScript specification property hasInstance. Thus instanceof expressions are rewritten by the compiler for other types. Note that a reference to a class returns the constructor type, which actually is a function itself.
50. Includes interfaces, since an interface type reference is a subtype of object type reference: $\text{type}\left\{\text{Interface}\right\}<:\text{type}\left\{\text{Object}\right\}$
51. See [ECMA15a], Chapter 12.3.5 "The Super Keyword"; note the use of HomeObject instead of thisValue; also see this blog - http://www.2ality.com/2011/11/super-references.html.
52. $e{\in }^{*}c$ is the transitive version of $e\in c$, that is, it $e$ directly or indirectly contained in $c$.
53. available at: http://www.2ality.com/2013/06/iterators-generators.html
54. For more details on module specifiers, see Qualified Names.
55. Further reading on DI Basics: [Fowler04b; Prasanna09a], Verification [Zhu13a; Hudli13a], Frameworks [Lesiecki08a; Betts13a; Knol13a; Dagger]
56. Usually, only the DIC itself is created like that, e.g., var dic = N4Injector.of(DIC).create(DIC);
57. Note that other frameworks may define other constraints, e.g., arbitrary keys.
58. Cf. a blog post about micro types - http://www.markhneedham.com/blog/2009/03/10/oo-micro-types/, and tiny types - http://darrenhobbs.com/2007/04/11/tiny-types/
59. This restriction has two reasons: Firstly, user-defined types with implementations would require to ’bootstrap’ the polyfill, which is impossible to do automatically without serious constraints on bootstrap code in general. Secondly, instead of filling user-defined types, they can be subclasses. Mechanisms such as dependency injection could then solve almost all remaining problems.
61. Global basically means that the module defines no namespace on its own. Thus the annotation is a script/module related annotation.