Partial polymorphic type inference is undecidable, 26th Annual Symposium on Foundations of Computer Science, pp.339-345 ,

Making the future safe for the past: Adding genericity to the java programming language, Proc. OPPSLA'98, 1998. ,

A semantics of multiple inheritance, Information and Computation, vol.76, issue.2-3, pp.138-164, 1988. ,

DOI : 10.1016/0890-5401(88)90007-7

An implementation of FSub, Digital Equipment Corporation Systems Research Center, 1993. ,

Two extensions of Curry's type inference system, Logic and Computer Science, pp.19-76, 1990. ,

A new type assignment for ??-terms, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.5, issue.1, pp.139-156, 1978. ,

DOI : 10.1007/BF02011875

Functional characterization of some semantic equalities inside ??-calculus, Proceedings of the 6th Colloquium on Automata, Languages and Programming, pp.133-146, 1979. ,

DOI : 10.1007/3-540-09510-1_11

Higher-order unification via explicit substitutions: the case of higher-order patterns, Joint international conference and symposium on logic programming, pp.259-273, 1996. ,

URL : https://hal.archives-ouvertes.fr/inria-00077203

Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982. ,

DOI : 10.1145/582153.582176

Relaxing the Value Restriction, Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS), 2002. ,

DOI : 10.1007/978-3-540-24754-8_15

Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse d'état, 1972. ,

Characterization of typings in polymorphic type discipline, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.61-70, 1988. ,

DOI : 10.1109/LICS.1988.5101

Extending ML with semi-explicit higher-order polymorphism, Journal of Functional Programming, vol.155, pp.134-169, 1999. ,

DOI : 10.1007/BFb0014546

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.456.3425

Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems, vol.15, issue.2, pp.253-289, 1993. ,

DOI : 10.1145/169701.169692

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.388.430

How good is local type inference?, 1999. ,

Rank-2 type systems and recursive definitions, 1995. ,

What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.42-53, 1996. ,

DOI : 10.1145/237721.237728

A polar type system, Electronic Notes in Theoretical Computer Science, 2000. ,

Practical type inference for arbitrary-rank types, Journal of Functional Programming, vol.17, issue.01, 2004. ,

DOI : 10.1017/S0956796806006034

Type reconstruction with first-class polymorphic values, SIGPLAN '89 Conference on Programming Language Design and Implementation, 1989. ,

A direct algorithm for type inference in the rank-2 fragment of the second-order lambda -calculus, ACM Conference on LISP and Functional Programming, 1994. ,

Principality and decidable type inference for finite-rank intersection types, ACM Symposium on Principles of Programming Languages (POPL), pp.161-174, 1999. ,

The Objective Caml system, documentation and user's manual -release 3.05, 2002. ,

Polymorphic type inference and abstract data types, An earlier version appeared in the Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, pp.1411-1430, 1992. ,

DOI : 10.1145/186025.186031

Polymorphic type inference and abstract data types, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1411-1430, 1994. ,

DOI : 10.1145/186025.186031

A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, pp.348-375, 1978. ,

Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992. ,

DOI : 10.1016/0747-7171(92)90011-R

Coercion and type inference, In ACM Symp. on Priciples of Programming Languages, pp.175-185, 1983. ,

Polymorphic type inference and containment. Information and Computation, pp.211-249, 1988. ,

Purely Functional Data Structures, 1998. ,

DOI : 10.1017/CBO9780511530104

Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.54-67, 1996. ,

DOI : 10.1145/237721.237729

Type inference with constrained types, Theory and Practice of Object Systems, vol.X, issue.1, pp.35-55, 1999. ,

DOI : 10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4

Colored local type inference, ACM SIGPLAN Notices, vol.36, issue.3, pp.41-53, 2001. ,

DOI : 10.1145/373243.360207

Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming , LFP '88, pp.153-163, 1988. ,

DOI : 10.1145/62678.62697

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.1446

On the undecidability of partial polymorphic type reconstruction, Fundamenta Informaticae, vol.19, issue.12, pp.185-199, 1992. ,

Programming with Intersection Types and Bounded Polymorphism Available as School of Computer Science technical report CMU-CS, pp.91-205, 1991. ,

A type assignment for the strongly normalizable ?-terms ,

Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.561-577, 1980. ,

A framework for type inference with subtyping, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP'98), pp.228-238, 1998. ,

Synthèse de types en présence de sous-typage: de la théorie à la pratique, 1998. ,

Local type inference, Proceedings of the 25th ACM Conference on Principles of Programming Languages, pp.1-44, 1998. ,

Extending ML type system with a sorted equational theory, Institut National de Recherche en Informatique et Automatisme, p.153, 1992. ,

Programming objects with ML-ART an extension to ML with abstract and record types, Theoretical Aspects of Computer Software, pp.321-346, 1994. ,

DOI : 10.1007/3-540-57887-0_102

Towards a theory of type structure, Proc. Colloque sur la Programmation, pp.408-425, 1974. ,

Une extension de la theorie des types en ?-calcul, In Lecture Notes in Computer Science No, vol.62, pp.398-410, 1982. ,

Second-order unification and type inference for Churchstyle polymorphism, Conference Record of POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.279-288, 1998. ,

DOI : 10.1145/268946.268969

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.3618

The Flow Caml System: documentation and user's manual, Institut National de Recherche en Informatique et en Automatique (INRIA), 2003. ,

Typability and type checking in the second order ?-calculus are equivalent and undecidable, Ninth annual IEEE Symposium on Logic in Computer Science, pp.176-185, 1994. ,

Type Inference for System F with and without the Eta Rule, 1996. ,

The essence of principal typings, Proc. 29th Int'l Coll ,

Simple imperative polymorphism, Lisp and Symbolic Computation, pp.343-355, 1995. ,

Then nf(?) = ? by definition By Property 1.5.6.ii (page 51), we have ? ? ftv(?) By well-formedness, we must have ? ? dom(Q) ,

we have a restricted derivation of (Q) ? ? ? ,

If nf(? ) is ?, (Q) ? ? ? by Property 1.5.6.i (page 51), and (12) holds by Equiv-R. In both cases, we have a restricted derivation of (12) If ? is in T , then (Q) ? ? (13) holds by Eq-Mono and I-Equiv, Otherwise, (13) holds by I-Hyp ,

1 ) ? 2 ? ? (? ? 1 ) ? (2) holds by R-Context-R. This equivalence is thrifty since nf(? 2 ) and nf(?) are both ? ,

We have a thrifty derivation of ? 2 ? nf(? 2 ) by induction hypothesis, thus we get a thrifty derivation of ? ? ? (? ? 1 ) nf ,

This derivation is thrifty We conclude by observing that nf(?) is nf(? 2 )[? 1 /?]. ? Case ? / ? ftv(? 2 ): Then nf(?) is nf(? 2 ), and ? ? ? 2 by Eq-Free, thus we get a thrifty derivation of ? ? nf(? 2 ) by induction hypothesis and R-Trans. ? Otherwise, nf(?) is ? (? nf(? 1 )) nf(? 2 ) By induction hypothesis Hence, pp.1-1 ,

we get a thrifty derivation of ? ? nf(?) ,

If (Q) ? 1 ? ? 2 is thrifty, and (Q) ? 2 ? ? holds but (Q) ? 1 ? ? does not hold, then there exists a thrifty derivation of (Q) ,

Alias are similar to cases StSh-Hyp, StSh-Up, and StSh-Alias of Property ii. ? Case S-Nil: immediate. ? Case S-Rigid: immediate. w(?) + X × w(? ) + A × w A (? ). Hence, w(? 1 ) ,

If ? is neither ? nor ? , we get the result by A-Hyp If ? is ?, we have ? 1 = ?, and (Q, ? ?, ? = ? , Q 0 ) ? 1 ? ? holds by A-Hyp, thus (Q, ? ?, ? = ? , Q 0 ) ? 1 ? ? holds by R-Trans, Eq-Mono and A-Equiv. If ? is ? ,

We have (Q) ? ? ? (1) and (Q, ? ?, Q 0 ) ? 1 ? ? 2 . As explained above, we only need to consider cases A-Hyp and I-Hyp ,

If ? is not ?, the result is by A-Hyp. Otherwise, we have ? 1 = ? and is =. We have (Q, ? ? , Q 0 ) ? ? ? (2) from (1) and Property 1, pp.5-8 ,

? ? (3) holds by A-Hyp. Hence, (Q, ? ? , Q 0 ) ? ? ? holds by A-Equiv ,

We have ? 2 = ?. If ? is not ?, we get the result by A-Hyp ,

We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is rigid. Thus, we get the result by I-Hyp ,

We have (Q) ? ? (1) and (Q, ? ? ? ,

We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is flexible. Thus, we get the result by A-Hyp ,

We have ? 2 = ?. If ? is not ?, we get the result by I-Hyp. Otherwise, ? 1 is ?. By Property 1.7.2.iii (page 59) and (1), (Q, ??? , Q 0 ) ? ? (2) holds. Hence, pp.and I-Hyp ,

We have ? 2 = ?. We cannot have ? = ?, since the binding of ? is flexible. Thus, we get the result by A-Hyp ,

We have ? 2 = ?. If ? is not ?, we get the result by I-Hyp. Otherwise, ? 1 is ?. By A-Hyp ,

or (?, ?) with (? ? ) ? Q: In this case, unify simply returns unify (Q, ?, ? ), while unify is more elaborate. We have to consider the two following sub- cases: Subcase ? ? dom, we have Q(? ) =, p.54 ,

we get ? (Q b ) ? ? ?. Hence, (6) gives (Q) ? ? . By Lemma 2.1.6, it leads to (Q) ? ? ? . This is a contradiction with the hypothesis that (2) does not hold. Hence, unify cannot succeed, and this is the expected result. Otherwise, (2) holds, and unify returns Q. From (2), we have (Q) ? ? ? (8) We have to show that unify returns a rearrangement of Q. From (1), Q is of the form (Q a , ? ?, Q b ) and ? ? ftv(? (Q b ) ? ) (9). Hence, we can derive (Q) ? (Q b ) ? ? by I-Drop . From (8), we get (Q) ? (Q b ) ? ? (10) By Property 2 ? Case Let: We have (Q) ? a 1 : ? 1 and (Q) ?, x : ? 1 a 2 : ?. By induction hypothesis, we have (Q) ?, ? a 1 : ? 1 and (Q) ?, x : ? 1 , ? a 2 : ?, which can be written (Q) ?, ? , x : ? 1 a 2 : ?. Hence, by Rule Let, we get the expected result. ? Case Gen: The premise is (Q, ?? a ) ? a : ? (1), and ? is ? (?? a ) ? . Besides, ? / ? ftv(?) Let ? be a fresh variable (that is By Lemma 6.1.1 applied to (1) with the renaming Hence, by induction hypothesis, Applying Gen, we get (Q) ?, ? a : ? (? ? a ) ? [? /?], that is (by alpha-conversion) (Q) ?, ? a : ?, which is the expected result. Proof of Lemma 6 ,

By hypothesis By Corollary 6.1.3 (page 153), we get (QQ , ? ? ?) ?, x : ? 0 a : ?. Hence, the following derivation: (QQ , ? ? ?) ?, x : ? 0 a : ? (QQ , ? ? ?) ? ? I-Hyp (QQ , ? ? ?) ?, x : ? 0 a : ? (QQ , ? ? ?) ? ?(x) a : ? 0 ? ? (Q) ? ?(x) a : ? (Q , ? ? ?) ,

The premise is (Q, ? ?, Q ) ?, x : ? 0 a 0 : ? 0 (9) and dom(Q ) # ftv(?) (10). Besides, ? is ? (Q , ? ? ? 0 ) ? 0 ? ? (11). Hence ,

we get (Q) ? ?(x) a 0 : ? (? ? ,

Moreover, we have (Q, ? ?) ? 1 ? (Q ) ? 2 ? ? 1 (15) and (Q, ? ?) ? 2 ? (Q ) ? 2 (16). Besides, ? is ? (Q ) ? 1 . By (3), (13) and Rule Gen, we get (Q) ? a 1 : ? (? ?) ? 1 (17). Besides, the size of (17) is the size of (13) plus one. By induction hypothesis, p.1 ,

By (18), 22), and (23), and Rule App , we get (Q) ? a 1 a 2 : ? (? ? This corresponds to ,

the size of (24) is one plus the size of (18) and the size of (20). Hence, it is smaller than or equal to one plus the size of (13) plus the size of (14), that is, the size of ,

The premises are (Q, ??) ? a : ? 0 (25). and (Q, ??) ? 0 ? ,

By induction hypothesis, (Q) ? a : ? 0 (27) holds, with ? 0 ? ? (? ?) ? 0 (28), and the size of (27) is smaller than or equal to the size of (25), we get (Q) ? 0 ? (? ?) ? ,

The premises are (Q, ? ?) ? a 1 : ? 1 (35) as well as (Q, ? ?) ?, x : ? 1 a 2 : ? (36) By Gen and (35), we get (Q) ? a 1 : ? (? ?) ? 1 . By induction (Q) ? 1 ? 1 holds, Hence, by Rule Strengthen, we have (Q) ?, x : ? 1 a 2 ,

we get (Q 0 Q ) ? ? ? 1 , that is Similarly, we can derive (Q 0 Q ) ? ? ? 0 . Hence, (Q 0 ) ? (Q ) ? ? (Q ) ? 0 (20) holds by R- Context-R. We have (Q 0 ) ? (Q ) ? 0 ? ? (P 1 ) ? 0 from (19) By alpha-conversion, we have (Q 0 ) ? (Q ) ? 0 ? ? (Q 1 ) ? 0 (21), ) we get (Q 0 ) ? (Q ) ? ? 0 ,