E. Allen, J. Hilburn, S. Kilpatrick, V. Luchangco, S. Ryu et al., Type Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance, Conference on Object Oriented Programming Systems, Languages and Applications (OOPSLA, 2011.
DOI : 10.1145/2076021.2048140

URL : http://www.mpi-sws.org/~skilpat/papers/multipoly.pdf

J. Bezanson, Abstraction in technical computing, Ph.D. Dissertation. Massachusetts Institute of Technology, 2015.

J. Bezanson, A. Edelman, S. Karpinski, and V. B. Shah, Julia: A Fresh Approach to Numerical Computing. SIAM Rev, vol.59, p.1, 2017.

A. Bonnaire-sergeant, R. Davies, and S. Tobin-hochstadt, Practical optional types for Clojure, European Symposium on Programming, 2016.

F. Bourdoncle and S. Merz, Type Checking Higher-order Polymorphic Multi-methods, Symposium on Principles of Programming Languages (POPL, 1997.

N. Cameron, S. Drossopoulou, and E. Ernst, A Model for Java with Wildcards, European Conference on Object-Oriented Programming, 2008.

G. Castagna, K. Nguyen, Z. Xu, and P. Abate, Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction, Symposium on Principles of Programming Languages (POPL, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00880744

G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet et al., Polymorphic Functions with Set-theoretic Types: Part 1: Syntax, Semantics, and Evaluation, Symposium on Principles of Programming Languages (POPL, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00907166

G. Castagna and B. C. Pierce, Decidable Bounded Quantification, Symposium on Principles of Programming Languages (POPL, 1994.

C. Chambers, T. Gary, and . Leavens, Typechecking and Modules for Multi-methods, Conference on Object-oriented Programming Systems, Languages and Applications (OOPSLA, 1994.

J. Chambers, Object-Oriented Programming, Functional Programming and R. Statist. Sci, vol.2, 2014.

K. Claessen and J. Hughes, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00, pp.268-279, 2000.

C. Clifton, G. T. Leavens, C. Chambers, and T. Millstein, MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java, Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA, 2000.

L. Demichiel and R. Gabriel, The Common Lisp Object System: An Overview, European Conference on Object-Oriented Programming, 1987.

J. Duregård, P. Jansson, and M. Wang, Feat: Functional Enumeration of Algebraic Types, Proceedings of the 2012 Haskell Symposium (Haskell '12, pp.61-72, 2012.

A. Frisch, G. Castagna, and V. Benzaken, Semantic Subtyping, Symposium on Logic in Computer Science (LICS, 2002.
URL : https://hal.archives-ouvertes.fr/hal-00152690

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types, J. ACM, vol.55, p.24, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00336120

F. Zappa-nardelli, J. Belyakova, A. Pelenitsyn, B. Chung, J. Bezanson et al.,

R. Grigore, Java Generics Are Turing Complete, Symposium on Principles of Programming Languages (POPL, 2017.

A. Kennedy and B. C. Pierce, On Decidability of Nominal Subtyping with Variance, Workshop on Foundations and Developments of Object-Oriented Languages, 2007.

V. Litvinov, Constraint-based Polymorphism in Cecil: Towards a Practical and Static Type System, Addendum to the Conference on Object-oriented Programming, Systems, Languages, and Applications, 1998.
DOI : 10.1145/346852.346948

V. Litvinov, Constraint-Bounded Polymorphism: an Expressive and Practical Type System for Object-Oriented Languages, 2003.

K. Mazurak and S. Zdancewic, Type Inference for Java, vol.5, 2005.

C. Benjamin and . Pierce, Bounded Quantification is Undecidable, Symposium on Principles of Programming Languages (POPL, 1992.

A. Randal, D. Sugalski, and L. Toetsch, Perl 6 and Parrot Essentials, 2003.

D. Smith and R. Cartwright, Java Type Inference is Broken: Can We Fix It, Conference on Object-oriented Programming Systems, Languages and Applications (OOPSLA, 2008.

R. Tate, A. Leung, and S. Lerner, Taming Wildcards in Java's Type System, Conference on Programming Language Design and Implementation (PLDI, 2011.

, The Julia Language. 2018. Manual: Diagonal Types, 2018.

J. Vouillon, Subtyping Union Types, Computer Science Logic (CSL, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00012706

S. Wehr and P. Thiemann, On the Decidability of Subtyping with Bounded Existential Types, Programming Languages and Systems (ESOP), 2009.

F. Zappa-nardelli, J. Belyakova, A. Pelenitsyn, B. Chung, and J. Bezanson, Julia Subtyping: a Rational Reconstruction-Project Web-Page, 2018.

S. Zdancewic, Type Inference for Java 5, 2006.

, Since types are themselves values, it is legitimate to invoke typeof on them, and the types DataType, Union, and UnionAll play the role of kinds. Indeed, the auxiliary function is_kind(t) returns true if t is DataType, or Union

, We write typeof(t, G) as a shorthand for there exists t ? such that typeof(t, G) = t ?. We have seen that Julia's frontend implicitly performs several simplifications when processing types; for instance, T where T is replaced by Any, or Union{Int, Int} is replaced by Int; these simplifications must be taken explicitly into account when formalizing the typeof relation. The auxiliary function simplify (t) performs the following simplification steps: ?, Since the typeof function plays a role in the definition of subtyping, we provide its formalization in Fig. 4

, ? remove redundant Union types

, ? remove duplicate and obviously redundant types from Union{t 1

, t n , a type t i is obviously redundant whenever there exists a type t j which is its supertype given an empty variable environment. These simplifications are guided by pragmatic considerations rather than semantic issues. As such they tend to vary between Julia versions