Liquid Intersection Types
Full text
Liquid Intersection Types Mário José Parreira Pereira Mestrado em Ciência de Computadores Departamento de Ciência de Computadores 2014 Orientador António Mário da Silva Marcos Florido, Professor Associado, Faculdade de Ciências da Universidade do Porto Co-orientadora Sandra Maria Mendes Alves, Professor Auxiliar, Faculdade de Ciências da Universidade do Porto
Todas as correções determinadas pelo júri, e só essas, foram efetuadas. O Presidente do Júri, Porto, ______/______/_________
ÀBárbara,aoVitor,aoPadrinhoeàMãe.ÀmemóriadomeuPai... 5
Agradecimentos Um ano de trabalho depois, uma tese depois... O resultado contido neste documento não seria possível sem a contribuição de um conjunto especial de pessoas, a quem desejo ser capaz de agradecer da forma que merecem. Em primeiro lugar quero deixar o meu enorme agradecimento aos meus orientadores, Professor Mário Florido e Professora Sandra Alves. Sinto-me verdadeiramente um privilegiado, por todo o apoio que recebi ao longo do meu trabalho, por todas as fantásticas reuniões semanais e por todo o muito conhecimento que me transmitiram. Ao Professor Mário, por toda a paciência com que sempre me recebeu, pelo desafiante tema proposto e por toda a orientação ao longo de tantos artigos e teses explorados. À Professora Sandra, pelas aulas de Fundamentos de Linguagens de Programação que me levaram ao fascínio pela área de sistemas de tipos, por toda a simpatia com que sempre me explicou qualquer conceito ou prova menos bem compreendida e por último toda a minúcia com que reviu esta tese. Muito, muito obrigado a ambos. Aos meus grandes amigos: ao Nuno Leitão, por uma amizade que já vem desde o tempo do 1ociclo, que foi um colega de universidade espectacular mas que sobretudo é um amigo ímpar; ao Nuno Santos, que igualmente desde a escola primária me atura e que continua actualmente a ser sempre um amigo indispensável; ao Nuno Pereira, pelos bons momentos que a sua (às vezes) boa disposição proporciona; ao João Machado, pelo exemplo de força e coragem que tem sido para mim ao longo destes mais de quatro anos de batalha, mas que nunca perdeu o bom humor e é sempre mais do que um privilégio poder desfrutar da sua companhia; ao Filipe Oliveira, que acabou por vir também fazer o seu mestrado na inigualável Faculdade de Ciências da Universidade do Porto, a sua determinação, vontade e trabalho árduo têm sido uma verdadeira inspiração para mim; ao João Neves, com quem é sempre um prazer conversar, nem que seja pela sua sempre boa disposição e originalidade com que aborda cada situação do dia-a-dia; ao Vasco Ramos, por todos os anos de convivência e por tantas boas aventuras já partilhadas. 7
Queria deixar um agradecimento muito particular e muito especial ao Professor Simão Melo de Sousa. Por ser um verdadeiro “padrinho académico”, por me ter sempre incentivado a trabalhar em áreas mais fundamentais da ciência de computadores e por todas as óptimas e estimulantes conversas que me tem proporcionado ao longo de todos estes anos. É um prazer enorme poder colaborar com o Professor, e que espero que se mantenha uma constante nos desafios vindouros dos próximos anos. Ao grupo Release da Universidade da Beira Interior, que apesar de já não ser um membro efectivo da família, sempre me acolheram como tal e pelos convites para participar no seu ciclo de tertúlias. Um obrigado particular ao Professor João Paulo Fernandes, ao Professor Paul Crocker, à Eunice Raquel, Tiago Pereira e ao Luís Horta. Atodaaminhafamília,portodooapoio,carinhoeincentivoquesempremetêm dado ao longo dos anos. Um agradecimento especial ao tio Paulo, tia Paula, Diogo e Gustavo por toda a ajuda e acolhimento ao longo destes dois anos de Porto. À Xana, que tão bem me recebeu em Paris e por ser sempre uma companheira tão especial para mim. E claro, nunca esquecendo a família adoptiva, ao Jorge, Carla e Bernardo omeueternoobrigado. Aumadasminhasmaioresinspiraçõesdevida,aomeuqueridoPadrinhoPaulo Fiadeiro não me é fácil arranjar palavras suficientes para agradecer como merece. Tanta paciência, tanta boa disposição ao longo da minha vida e claro, por ter sido quem me ensinou a escrever as primeiras linhas de código, eternamente o meu sincero e sentido obrigado. ÀminhaqueridaecarinhosanamoradaBárbara,portodaacompanhiaefelicidade que tem sido estes quase quatro anos a dois. Sempre disposta a dar-me a última palavra de incentivo, sempre a primeira a chegar nos momentos menos bons e por toda a compreensão pela ausência que às vezes o trabalho possa ter provocado. Só posso desejar que possas estar lá por muito mais tempo ao meu lado, sempre com o mesmo sorriso e maneira querida de resolver todos os problemas. Iloveyou. Ao Vitor, meu querido irmão e primeiro grande amigo de vida. Não tenho qualquer memória do que é ser filho único, do que é não te ter sempre ao meu lado e isso torna-me imensamente feliz. Muito daquilo que faço e me tenho vindo a interessar está intimamente ligado a todas as conversas que temos, a toda a ajuda que nunca te negaste a dar-me e sobretudo pela inteligência sensacional com que sempre me soubeste impressionar. Só me resta torcer para que continues a gostar das tuas explorações das áreas fundamentais da computação, para que mais um sonho se possa tornar realidade em breve. 8
Olhar para o culminar deste trabalho, significa invariavelmente agradecer profundamente à minha verdadeira Mãe Coragem. Nenhum obstáculo para ti foi grande osuficientequenãooconseguissesultrapassar;nenhumapropinafoiexcessivao suficiente para fazer vacilar a tua vontade. Por tanto e cada vez mais, obrigado por tudo Mãe, obrigado por nunca desesperares com as minhas loucuras e por sempre me ensinares que o melhor caminho é o do trabalho. Porque nenhuma parte desta tese é tão difícil de escrever como este parágrafo, por mais desafios científicos que me possam apresentar, é a ti Pai que dedico todo este trabalho. Aausênciaeaslágrimasqueagorameinundamosolhossãoligeiramentecompensadas com a alegria e orgulho que apenas posso imaginar que terias neste momento. O meu maior obrigado vai direitinho para ti, meu ídolo e referência para o que ainda falta percorrer nas minhas aventuras. Que eu seja sempre um motivo de orgulho para ti, mesmo agora que o teu abraço tão grande está tão distante de mim... 9
Abstract Refinement types can be used to improve the expressiveness of type systems for functional programming languages. These kind of systems present the type language augmented with logical annotations, so that the functional behavior of programs can be directly specified on the type language. This thesis presents a new type system featuring refinement predicates jointly with the accuracy offered by intersection types discipline, the Liquid Intersection Types system. This system can be used to derive very precise types, leading to detailed descriptions of how programs behave. Despite the risk of undecidable problems posed by general refinement type systems and intersection types, we keep our system decidable by forcing three main restrictions: •expressions appearing in refinement types of particular terms must exclusively be conjunctions of qualifiers taken from a global programmer-supplied set of logical qualifiers; •we use in our system a conservative (decidable) subtyping judgment; •intersection types within our system are only for types of the same form i.e., we can only intersect refinement of the same ML type differing on the associated refinement expressions. Along with the type system, we propose an algorithm for inferring Liquid Intersection Types for a given program. This algorithm relies on the Damas-Milner inference engine to infer ML types, which will allow to generate intersection types containing all the sound combinations of qualifiers supplied. To be able to experimentally validate our results, we conceived the tool lisette. This tool allows to test the proposed inference mechanism over a program written in an ML-like programming language. 17
Resumo Tipos refinados podem ser usados para melhorar a expressividade de sistemas de tipos para linguagens funcionais. Este conjunto de sistemas de tipos apresenta a linguagem de tipos aumentada com anotações lógicas, de tal forma que o comportamento funcional de programas pode ser directamente especificado na linguagem de tipos. Esta dissertação apresenta um novo sistema de tipos com refinamentos e a precisão oferecida pela disciplina de tipos com intersecções, o sistema Liquid Intersection Types. Este sistema pode ser utilizado para derivar tipos bastante precisos, resultando em descrições detalhadas do comportamento de programas. Apesar do risco de problemas indecidíveis associados ao uso de tipos com refinamentos e tipos com intersecções gerais, mantemos o nosso sistema decidível implementando três restrições principais: •expressões constantes nos refinamentos dos tipos de alguns termos em particular devem ser exclusivamente compostos por conjunções de qualificadores retirados de um conjunto global, introduzido pelo programador, de qualificadores lógicos; •autilizaçãononossosistemadeumjulgamentodesub-tipagemconservativo (decidível); •onossosistemaapresentaapenasintersecçõesdetiposcomamesmaformai.e., podemos apenas intersectar refinamentos do mesmo tipo ML que defiram nos refinamentos associados. Em conjunto com o sistema de tipos, propomos também um algoritmo para a inferência de Liquid Intersection Types para um dado programa. Este algoritmo usa o mecanismo de inferência de Damas-Milner para inferir tipos ML, os quais permitirão gerar tipos com intersecções contendo todas as combinações correctas dos qualifiers fornecidos. De forma a ser possível validar experimentalmente os nossos resultados, construímos aferramentalisette. Esta ferramenta permite testar o mecanismo de inferência proposto para um programa escrito numa linguagem de programação estilo ML. 19
Chapter 1 Introduction 1.1 Contextualization Since the rise of the ML type system and practical inference approaches [Dam84], there has been a constant demand for more expressive type systems. It is desirable that such systems could not only capture the typing properties of terms, but also additional information about programs. As examples we have type-and-effect systems [NN99] and refinement type systems [FP91]. Refinement types [KF10] state complex program invariants, by augmenting type systems with logical predicates. A refinement type of the form {⌫:B|}stands for the set of values from basic type Brestricted to the filtering predicate (refinement) . A subtyping relation exists for refinement types, which will generate implication conditions: ;⌫:B`) `{⌫:B|}<:{⌫:B| } One idea behind the use of such type systems is to perform type-checking using SMTs (Satisfability Modulo Theories) solvers [Sho84], discharging conditions as the above ) .However,theuseofarbitrarybooleantermsasrefinementexpressionsleads to undecidable type systems, both for type checking and inference. Liquid Types [RKJ08, VRJ13] present a system capable of automatically infer refinement types, by means of two main restrictions to a general refinement type system: refinement predicates of some terms are conjunctions of expressions exclusively taken from a global, user-supplied set (denoted Q)oflogicalqualifiers(simplepredicates 21
22 CHAPTER 1. INTRODUCTION over program variables, the value variable ⌫and the variable placeholder ?); and a conservative (hence decidable) notion of subtyping. Despite the interest of Liquid Types, some situations arise where the inference procedure infers poorly accurate types. For example, considering Q={⌫0,⌫0} and the term neg ⌘x. x,LiquidTypesinferforneg the type x:{0⌫^0 ⌫}!{0⌫^0⌫}1. This type cannot be taken as a precise description of the neg function’s behavior, since it is not expressed that for a positive (resp. negative) argument the function returns a negative (resp. positive) value. With our system we will have for neg the type (x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0}). We introduce Liquid Intersection Types, a refinement type system with the addition of intersection types [BCDC83, CDC80]. Our use of intersection in conjunction with refinement types is motivated by a problem clearly identified for Liquid Types: the absence of most-general types, as in the ML tradition. Our use of intersection for refinement types draws some inspiration from [FP91], since this offers a way to use jointly detailed types and intersections. Though, integrating this expressiveness with refinement types and keeping the qualifiers from Qsimple (which must be provided by the programmer) implies the design of a new type system. Besides the new type system, another contribution of this work is a new inference algorithm for Liquid Intersection Types. Using our algorithm allows a programmer to reap the expressiveness benefits of Liquid Intersection Types, needing only to provide the set Qand without the need to annotate the source code with typing information. This algorithm is the core of the lisette tool, a prototype resulting in the implementation of the theoretical work described in this thesis. 1.2 Thesis organization and contributions In the second chapter we introduce concepts and results that form the basis of our contributions. In particular, we revisit the road from untyped -calculus until polymorphic type system, with emphasis on the simply-typed -calculus, ML type system and a form of intersection types. We give particular attention to the type safety property of these systems as well as the soundness and completeness of the respective inference algorithms. In chapter three we focus on the specific family of refinement type systems. These 1Throughout this thesis we write {}instead of {⌫:B|}whenever Bis clear from the context.
1.2. THESIS ORGANIZATION AND CONTRIBUTIONS 23 systems are the main inspiration for our Liquid Intersection Type system, and so we present in detail some of their most relevant features. We give particular attention to the system of Liquid Types. Chapter four presents the Liquid Intersection Type system, detailing its type and terms language, semantics and typing rules. We conclude this chapter with the detailed proof of the subject reduction property for our system. Chapter five is concerned to the presentation of the algorithm to infer Liquid Intersection Types for a given term and the supplied set Q.Wepresentsomeexamplesofhow our algorithm works and proof a soundness result for it. We also give a description of the devised prototype, the lisette tool. We detail on how this tool computes and show the result of running lisette over a small example. Finally, in the last chapter of the thesis we summarize our conclusions of the work done, review the objectives initially proposed for this work and outlook some possible lines of future work. We give in the appendix the source code of the most relevant parts of the inference algorithm, as well as the mechanism for solving generated constraints, all implemented as part of lisette. The work done in this thesis was partially presented in [PAF14a] and [PAF14b].
Chapter 2 Background 2.1 The untyped -calculus We use -calculus [Chu33] as the underlying computational language throughout this thesis. The -calculus is the theoretical core of most modern programming languages and is widely recognized as the perfect setting for the study of type systems. We shall present some basic concepts about -calculus (namely its syntax and semantics). 2.1.1 Syntax Definition 2.1.1 (-terms) We assume an infinite set Vof variables. The set ⇤of -terms is defined as follows: 1. x2⇤if x2V 2. (MN)2⇤if M,N 2⇤ 3. (x.M)2⇤if M2⇤,x2V Terms built as in the previous third point are called -abstractions,corresponding to anonymous functions in some programming languages. For instance, (x.x)corresponds in Haskell to \x -> x. The application (MN)(second point) stands for the application of the function represented by Mto the argument N. 25
32 CHAPTER 2. BACKGROUND Abs Abs Abs App Va r `f:⌧1!⌧2 Va r `g:⌧0!⌧1 Va r `x:⌧0 `gx:⌧1 App `f(gx):⌧2 f:⌧1!⌧2;g:⌧0!⌧1`x.f (gx):⌧0!⌧2 f:⌧1!⌧2`g. x. f (gx):(⌧0!⌧1)!⌧0!⌧2 ;`f. g. x. f(gx):(⌧1!⌧2)!(⌧0!⌧1)!⌧0!⌧2 Figure 2.2: Type derivation for the composition of functions. where =f:⌧1!⌧2;g:⌧0!⌧1;x:⌧0. This derivation is valid for any ⌧0,⌧1and ⌧2. For a given term Mand a context ,ifnotype⌧exists such that `M:⌧holds then we say Mcannot be typed under . Moreover, if for any we cannot give a ⌧ such that `M:⌧then the term cannot be typed in the simply typed -calculus. For instance, the term (x.xx)cannot be typed, as there are no and ⌧for which one can build a typing derivation validating `(x.xx):⌧. For the presented set of typing rules there is at most one such rule that can be applied to type a term. This implies that the shape of the derivation is completely determined by the structure of the term being typed, and so we say the typing rules are syntax directed. Consequently, we can state an inversion lemma explaining how sub-terms of awell-typedtermcanalsobetyped. Lemma 2.2.1 (Inversion for typing rules) Suppose that `M:⌧. •If M⌘xthen x2dom()and (x)=⌧; •If M⌘M1M2then `M1:⌧0!⌧and `M2:⌧0,forsome⌧0; •If M⌘x.N then ⌧is of the form ⌧1!⌧2and ;x:⌧1`N:⌧2. Proof. By induction on the derivation of `M:⌧. In a syntax directed system proofs about its inference rules are very much simplified, since we know for sure the rule applied to type check some term. Also, any proof by induction on a derivation `M:⌧presents equivalent arguments to a proof by structural induction on M.
2.2. SIMPLY-TYPED -CALCULUS 33 2.2.3 Properties The use of type systems gives us strong guarantees about the execution of programs. This is captured by Milner’s slogan “well-typed expressions do not go wrong”. Yet very informal, this slogan already indicates the relation between the type system of a calculus (“well-typed expressions”) an how terms compute (“do not go wrong”). We revisit here the principal results that guarantee type safety for simply typed - calculus, choosing the call-by-value variant for the dynamic semantics. 2.2.3.1 Structural properties Concerning the structure of the typing context and how variables stored in it can be used to type check terms, there are some important properties that worth to be mentioned. Simply typed -calculus satisfies the following three structural properties: Lemma 2.2.2 (Weakening) If 1; 2`M:⌧then 1;x:⌧0; 2`M:⌧,forany x62 dom(1; 2)and any ⌧. Proof. By induction on the derivation of 1; 2`M:⌧. Lemma 2.2.3 (Exchange) If 1;x1:⌧1;x2:⌧2; 2`M:⌧then 1;x2:⌧2;x1:⌧1; 2`M:⌧. Proof. By induction on the derivation of 1;x1:⌧1;x2:⌧2; 2`M:⌧. Lemma 2.2.4 (Contraction) If 1;x1:⌧0;x2:⌧0; 2`M:⌧then 1;x3:⌧0; 2`[x3/x1][x3/x2]M:⌧. Proof. By induction on the derivation of 1;x1:⌧0;x2:⌧0; 2`M:⌧. The property of weakening states that the addition of new, unnecessary variables to the typing context does not invalid a term to type check. The second property, exchange, indicates that the order in which one adds variables to a context does not affect the type checking process. In fact, if a term can be type checked under then it can be type checked under any permutation of .Finally,thepropertyofcontraction says that if a term can be type checked using two identical hyphotesis in the context, then it can also be type checked using just a single hyphotesis.
34 CHAPTER 2. BACKGROUND Although some of the previous properties may seem obvious, formally stating them eliminates some informal reasoning in proofs. Also, there exists some interesting type systems that do not satisfy one, two or even any of these three properties. This systems are known as substructural type systems, with an example of such systems being linear types [Wad90]. 2.2.3.2 Dynamic semantics We choose the call-by-value strategy to describe how terms in simply typed -calculus shall execute. We give a contextual presentation, based on the reduction system previously shown for the untyped -calculus: (x.M)v![v/x]M Context M!N E[M]!E[N] Values are represented by vand in the simply typed -calculus values are the - abstractions and variables: v::= x.M |x Any reduction step may occur inside a call-by-value evaluation context,definedbythe following grammar: E::= [ ] |EM |vE 2.2.3.3 Type safety The property of type safety is proved by showing that each step of reduction preservers typing (moreover, it preserves the same type) and by showing that well-typed terms cannot get stuck. The first part is described as subject reduction (or preservation) and the other one is called progress. This syntactic approach to prove safety of type systems is due to [WF92]. Lemma 2.2.5 (Substitution lemma) If ;x:⌧0`M:⌧and `N:⌧0then `[N/x]M:⌧. Proof. By induction on the derivation ;x:⌧0`M:⌧. Theorem 2.2.1 (Subject reduction) If `M:⌧and M!Nthen `N:⌧.
2.2. SIMPLY-TYPED -CALCULUS 35 Proof. By induction on `M:⌧,makinguseofasubstitutionlemmaatthecase M⌘(x.M0)v. Lemma 2.2.6 (Canonical forms) If ;`v:⌧and ⌧is an arrow type, then vis a -abstraction. Theorem 2.2.2 (Progress) If ;`M:⌧(Mis a closed well-typed term) then either Mis a value or there exists Nsuch that M!N. Proof. By induction on ;`M:⌧,makinguseofthelemmaofcanonicalforms. 2.2.4 Type inference The problem of given a term Mfind out a ⌧such that `M:⌧is traditional referred as type inference or type reconstruction. The process of type inference is a common and crucial feature of most modern functional programming languages, since it allows to check if a program is well-typed without requiring the programmer to supply (almost or none) any type annotations. 2.2.4.1 Type substitutions Atypevariable,asthenameitselfindicates,canbesubstitutedbyothertypes. Definition 2.2.1 (Type substitution) Atype substitution S(·)is an idempotent function, i.e. 8⌧.(S(S(⌧)) = S(⌧),oftheform⌧i/↵i,forsomesetoftypevariables↵i and types ⌧i.S(⌧)is the type obtained by substituting all variables ↵jfor ⌧jin ⌧. Any substitutions S1and S2can be composed in the usual way. Definition 2.2.2 (Type substitution composition) Let S1and S2be type substitutions. The composition S1S2is defined as: 8↵.(S2S1)(↵)=S2(S1(↵)) The previous definitions can now be used to define type instance: Definition 2.2.3 (Type instance) Atype⌧0is an instance of a type ⌧iffthere is a substitution Ssuch that S(⌧)=⌧0.
36 CHAPTER 2. BACKGROUND The notion of instance can also be applied to typing contexts, by lifting type substitutions in the natural way: Definition 2.2.4 (Type instance for contexts) Atypingcontext0is an instance of iffthere is a substitution Ssuch that S() = 0, where S() = (;if =; S(0); x:S(⌧)if= 0;x:⌧ 2.2.4.2 Unification The concept of unification plays a central role in the whole process of type inference, as we will briefly present. Unification is used to relate two, possibly, distinct types through substitution. Definition 2.2.5 (Unifier) An unifier between types ⌧1and ⌧2is a type substitution such that S(⌧1)=S(⌧2). Definition 2.2.6 (Most general unifier) We say Sis the most general unifier of ⌧1and ⌧2if for any other unifier S1of ⌧1and ⌧2there is a substitution S2such that S1=S2S. As an example, consider the types ⌧1=↵!↵and ⌧2=↵1!↵2as well as the substitutions S1=[(↵3!↵4)/↵,(↵3!↵4)/↵1,(↵3!↵4)/↵2] and S2=[↵/↵1,↵/↵ 2] Both S1and S2are unifiers for ⌧1and ⌧2,butonlyS2is the most general unifier. The most general unifier can be computed using Robinson’s algorithm [Rob65] for the case where terms to be unified are types. This algorithm will return the most general unifier or fail in case one does not exist. Definition 2.2.7 (Robinson’s most general unifier) Let ⌧1and ⌧2be two simple
2.2. SIMPLY-TYPED -CALCULUS 37 types. The function mgu(⌧1,⌧ 2)is defined as: mgu(↵,⌧)=8 > < > : [⌧/↵]if ↵62 FV(⌧) Id if ↵=⌧ fail if otherwise mgu(⌧1!⌧2,↵)=mgu(↵,⌧1!⌧2) mgu(⌧1!⌧2,⌧ 3!⌧4)=let S=mgu(⌧1,⌧ 3)in mgu(S(⌧2),S(⌧4)) S 2.2.4.3 Principal types Several -terms can have more than one type. For instance, the term xy.y can be assigned the type ↵1!↵2!↵2or the type ↵1!(↵2!↵3)!(↵2!↵3). This way, it makes sense to define a notion of principal type,thatis,atypethatsomehow can represent all the other assignable types to a term. Definition 2.2.8 (Principal type) Let Mbe a -term and ⌧a simple type. The type ⌧is said to be M’s principal type iff •there exists a such that `M:⌧; •for any other derivation 00 `M:⌧0there is a sub-set 0of 00 such that 0is an instance of ,obtainedusingasubstitutionSand ⌧0is an instance of ⌧,usingS as well. The principal type of a term is useful for describing the possible set of types assigned to a term. Many inference algorithms (as the ones we present here) are concerned with computing the principal type of the given term. This is commonly accomplished by using Robinson’s most general unifier. 2.2.4.4 Hindley-Milner’s algorithm We present a type inference algorithm due to Hindley [Hin69] and latter rediscovered by Milner [Mil78]. This algorithm defines a function T(·)that given a term Mreturns acontextand a type ⌧such that `M:⌧.
38 CHAPTER 2. BACKGROUND Definition 2.2.9 (Hindley-Milner algorithm T)Let be a typing context, Ma -term and ⌧a simple type. The function T(M)=(,⌧)is defined as follows: T(x)=({x:↵},↵),↵is a fresh variable T(M1M2)=let T(M1)=( 1,⌧ 1)in let T(M2)=( 2,⌧ 2)in let S=mgu(⌧1,⌧ 2!↵)(↵fresh) in (S(1; 2),S(↵)) T(x.M1)=let T(M1)=(,⌧ 2)in if (x)=⌧1then (x,⌧ 1!⌧2) else (,↵!⌧2)(↵fresh) where mgu(·,·)is Robinson’s unification algorithm. As an example of how the algorithm performs, consider the term M⌘(xy.x)(z.z). Applying T(·)to Mwe have: T(x)=({x:↵1},↵ 1) )T(y.x)=({x:↵},↵ 2!↵1) )T(xy.x)=({} ,↵ 1!↵2!↵1) Also: T(z)=({z:↵3},↵ 3) )T(z.z)=({} ,↵ 3!↵3) The last step is to infer the type of the application (xy.x)(z.z).So,weneedto compute the substitution S=mgu(↵1!↵2!↵1,(↵3!↵3)!↵4): S=mgu(↵1!↵2!↵1,(↵3!↵3)!↵4) =let S1=mgu(↵1,↵ 3!↵3)=[↵3!↵3/↵1]in mgu(S1(↵2!↵1),S1(↵4)) S1= =mgu(↵2!(↵3!↵3),↵ 4)S1= =[↵2!(↵3!↵3)/↵4][↵3!↵3/↵1] Finally, we have: T((xy.x)(z.z)) = (S({}),S(↵4)) = ({},↵ 2!↵3!↵3) The algorithm Twas proved sound and that for each -term Mit infers a simple type ⌧such that ⌧is the principal type of M.
2.3. POLYMORPHISM 39 2.3 Polymorphism As we have previously seen, for some terms, we can assign distinct types. For instance, the identity function (x.x)has type ↵!↵and so one can instantiate ↵with int or float !float, resulting in the following derivations: Abs x:int `x:int ;`x.x :int !int x:float !float `x:float !float ;`x.x :(float !float)!(float !float) Abs The ability of a term to simultaneously admit different types is called polymorphism. Polymorphism [Rey74] is essential in programming: for any programming language without this feature, one needs to define different functions for each possible type, even if these functions behave equally. There are two different notions of polymorphism that worth to be mentioned: •parametric polymorphism: commonly found in most modern programming languages, is a form of polymorphism where a term can be typed generally, with different types being instances of a common polymorphic type; some representative systems of this class of polymorphism are System F[Rey74, Gir72] and let-polymorphism or ML-style polymorphism [Mil78]. •ad-hoc polymorphism: a term can exhibit different behavior when applied to different types; the most popular form of ad-hoc polymorphism is overloading, where a single function name is associated with many implementation, with the compiler (or run-time system) being responsible for choosing the appropriate implementation. We present here two different systems implementing some form of polymorphism: the Damas-Milner type system [DM82] and intersection types [CDC80]. The first one belongs to the parametric polymorphism and is the basis of modern type systems, while in the latter variables can be explicitly assigned more than one type by means of very expressive type language. 2.3.1 Damas-Milner type system 2.3.1.1 Syntax The type systems of modern functional languages such as Standard ML, OCaml and Haskell are inspired by Damas-Milner type system,orsimplyML. This system offers a
40 CHAPTER 2. BACKGROUND restricted form of polymorphism and so avoiding the undecidability of type inference in System F. Within ML, type variables can only be substituted by quantifier-free types and polymorphic types cannot appear at the left of the ’!’operator. The ML system extends the term language of simply typed -calculus with a let operator, used to factor out multiple occurrences of the same sub-expression. The ML term language is then defined as follows: M,N ::= x|MN |x.M |let x=Min N Concerning type language, in ML polymorphic types are described using type schemes: ⌧::= ↵|⌧1!⌧2simple types ::= ⌧|8↵.0type schemes Atypeschemerepresentsthesetoftypesthat,givenatermMand a context ,can be inferred for Munder . Definition 2.3.1 (Generic instance) Let ⌧be a simple type and atypescheme. We say ⌧is a generic instance of iff=⌧or, considering a simple type ⌧0,= 8↵1,··· ,↵ n.⌧0and 9⌧1,··· ,⌧ nsuch that ⌧=[⌧i/↵i]⌧0. Definition 2.3.2 (Generic instance, type schemes) Let and 0be type schemes. We say 0is a generic instance of ifffor all ⌧instance of 0,⌧is also a generic instance of . 2.3.1.2 Dynamic semantics Regarding evaluation, an evaluation context for handling reduction of let-in terms is given: E::= [ ] |EM|vE|let x=Ein M Anewreductionruleisaddedtotheonesofsimplytyped-calculus: let x=vin M![v/x]M
2.3. POLYMORPHISM 41 ML-Gen ML-Abs ML-Var x:↵`x:↵ ;`x.x :↵!↵ ;`x.x :8↵.↵!↵† ML-App ML-Inst ML-Var i:8↵.↵!↵`i:8↵.↵!↵ i:8↵.↵!↵`i:(↵!↵)!(↵!↵) ML-Var i:8↵.↵!↵`i:8↵.↵!↵ i:8↵.↵!↵`i:↵!↵ ML-Inst i:8↵.↵!↵`ii :↵!↵‡ ML-Let ;`x.x :8↵.↵!↵†i:8↵.↵!↵`ii :↵!↵‡ ;`let i=(x.x)in ii :↵!↵ Figure 2.3: Derivation for let i=(x.x)in ii :↵!↵. 2.3.1.3 Type system The typing rules for Damas-Milner system are inductively defined as follows: ML-Var `x:(x) Ml-Abs ;x:⌧1`M:⌧2 `x:⌧1.M :⌧1!⌧2 ML-App `M:⌧1!⌧2`N:⌧1 `MN :⌧2 ML-Let `M:;x:`N:⌧ `let x=Min N:⌧ ML-Inst `M:8↵. `M:[⌧/↵] ML-Gen `M:↵not free in `M:8↵. As an example of a type derivation using the previous rules, consider the derivation for the term let i=(x.x)in ii in Figure 2.3. Note that (i.ii)(x.x)⌘let i= (x.x)in ii (they reduce to the same term), although we cannot assign a type to (i.ii)(x.x),sincethesub-term(i.ii)is not typable, even in the context of the ML type system. 2.3.1.4 Type inference As well as for simply typed -calculus, we shall present an inference algorithm for Damas-Milner system. We first define the notion of closure of a type ⌧with respect to a context : Definition 2.3.3 (Type closure) Let Vbe a set of variables, atypingcontext and ⌧a simple type. The closure of ⌧with respect to V,denotedV(⌧),isthetype
48 CHAPTER 3. REFINEMENT TYPES capable of describing what is the functional behavior of a term. We present here two different classes of systems with refined types: first, a system where the refinements are at the level of algebraic data-types; then a system where type language is augmented with logical predicates to filter the set of value a type can represent. For the latter, we will give particular attention to a system that is particularly suited for inference of such refinement types. 3.1 Refined algebraic data-types 3.1.1 Motivation The first form of refinement type system is described in [FP91]. The idea behind this type system is to conceive a system of subtypes for an ML-like language which preserves the decidability of type checking and inference of the ML type discipline, while providing a means for specification and inference of more precise type information. As a motivating example, consider the following function (written in Standard ML) that returns the last cell in a list: datatype ↵list = nil | cons of ↵⇤↵list fun lastcons (last as cons(hd, nil )) = last |lastcons(cons(hd,tl))=lastconstl No compile time-error would be issued for this code, although it is known that for an empty list the function lastcons would be undefined. The use of refinement types can prevent such run-time errors, by issuing a compile-time error whenever this function may be applied to an empty list. Similarly, for the following code: case lastcons y of cons(x, nil) )print x the compiler would send a warning, since it considers the pattern matching is incomplete. But, since we know for sure lastcons will only return singleton lists, no other case in the function lastcons would make sense. Refinement types can also be helpful for eliminating unreachable cases. Designing a system so expressive could easily lead to undecidable problems. In order to prevent such risk, the programmer must explicitly supply information of subtype distinctions. For the previous examples, one needs to instruct the compiler to distinguish
3.1. REFINED ALGEBRAIC DATA-TYPES 49 singleton lists from general lists: datatype ↵list = nil | cons of ↵⇤↵list rectype ↵singleton = cons (↵,nil) An inference process for this kind of refinement types was presented in [FP91] and can be thought of as performing abstract interpretation over a programmer-specified finite lattice of refinements of each ML type. Clearly, for maintaining decidability of inference, finiteness is an important issue to consider. For the previous example of singleton lists, type inference would have to perform abstract interpretation over the following lattice: ↵list ↵singleton _↵?nil ↵singleton ↵?nil ? where ?nil stands for the type assigned to empty lists. This type is important for the type inference process since it can distinguish singleton lists only if the element’s tail is nil. Abstract interpretation would infer the following type for the constructor cons: cons :(↵⇤↵?nil)!↵singleton ^ (↵⇤↵singleton)!↵list ^ (↵⇤↵list)!↵list 3.1.2 Type language Refinement types are built from traditional ML types and recursive types using the constructors 0^0(intersection) and 0_0(union). Both operators are used in a restricted way: only intersection and union of refinement types of the same ML type are accepted.
50 CHAPTER 3. REFINEMENT TYPES The grammar defining refinement types is the following: refty ::= refty ^refty |refty _refty | refty !refty |?| <refty >mltyname | <refty >reftyname | reftyvar :: mltyvar where the syntactic classes used are mltyname datatype constructors name, such as list mltyvar ML type variables, ranged by ↵ reftyvar refinement type variables, ranged by r↵,r reftyname refinements of datatypes name, such as singleton Datatype lattices can be viewed as the behavior of intersection and union of refinements of an ML type as well as a representation of the subtype relationship. As in most systems featuring subtyping, refinement types respect the contravariance of functions arguments: 1!⌧12!⌧2if ⌧1⌧2and 21.Although,todefineageneral subtyping relation for refinement types, it is convenient to convert types to a class of normal form types. For such purpose, we use the following rewriting rules: ⇢^(_⌧))(⇢^)_(⇢^⌧) (⇢_)!⌧)(⇢!⌧)^(!⌧) where ⇢,and ⌧represent refinement types. Also, if it holds that ⇢=_⌧then ⇢ should always be written as _⌧. Applying these rules, refinement types will follow the grammar unf ::= inf |unf _unf inf ::= <unf >reftyname |inf ^inf | inf !unf |reftyvar :mltyvar with unf meaning union normal form and inf intersection normal form. We can give now a definition for the subtype ordering ⌧, where and ⌧are unf refinements of the same ML type. Two cases arise: either their common ML type is a datatype or it is a function type. For the former, the subtype relationship is determined by the partial order of the constructed lattice. When the common ML type is a function type, the unf refinement types are a union of inf refinement types iand jand the they are compared using the following rule: 1_..._n0 1_..._0 m if for each ithere is a 0 jsuch that i0 j
3.1. REFINED ALGEBRAIC DATA-TYPES 51 which depends on how inf refinements of functional types are compared. Consider an inf refinement for a function type and its argument. The refinement type for the value of the function application can be computed as follows: if the function has type =(⇢1!⌧1)^...^(⇢n!⌧n)and the argument has type ⇢,thenthetype of their application is ^ {i|⇢⇢i} ⌧i and is denoted as apptype(,⇢). This definition can be used in the subtyping problem for inf refinements of functional types. The relation 0, where =(⇢1!⌧1)^...^(⇢n!⌧n) and 0=(⇢0 1!⌧0 1)^...^(⇢0 m!⌧0 m) is defined as meaning, for all ⇢in {⇢1,...,⇢ n,⇢ 0 1,...,⇢ 0 m}, apptype(,⇢)apptype(0,⇢) Finally, the system of refinement types also supports polymorphism, through a restricted form of bounded quantification. Type schemes are defined as follows: reftyscheme ::= inf | 8↵.reftyscheme | 8r↵:: ↵.reftyscheme The second and third clauses of the previous grammar deserve further explanation. The second case stands for the quantification over ML type variables, very similar to quantification in the ML type system. Such types can be considered as infinite intersections of ML types: considering the ML type 8↵.↵!↵ this can be understood as the intersection of ↵!↵ for all possible instantiations of ↵. The third clause represents quantification over a refinement type variable. For this case, once the ML type variable is instantiated with an ML type, we can only instantiate r↵with refinements of that ML type. As an example, given the refinement type 8↵.8r↵:: ↵.r↵!r↵
52 CHAPTER 3. REFINEMENT TYPES for the identity function, if we instantiate ↵to ↵list,instantiatingtherefinement type variable would result in the refinement type ↵list !↵list ^ ↵singleton !↵singleton ^ ?nil !?nil ^ ?!? The process of instantiation implies that for a refinement type scheme there are only finitely many types in the intersection, since an ML type has only finitely many refinements. This is very important when it comes to preserve decidability of the type system. Refinement type schemes appear, during inference, when a let expression is under analysis. This is very much similar to the inference process of the ML type system. 3.1.3 An example We present a more involving example of how refinement type inference works. Consider the ML datatype to represent natural numbers in binary codification: datatype bitstr = e|zof bitstr | oof bitstr where eis used to construct an empty bitstring, zappends a zero as the least significant digit and oappends a one as the least significant digit. One desirable property at compile-time is that a bitstring never has a zero as the most significant digit. To achieve this goal, we introduce two refinement types of bitstr: rectype std = e|stdpos and stpos = o(e)| z(stdpos) | o(stdpos) where std is type of bitstrings in standard form (no zero in the most significant place) and the type stdpos stands for positive natural numbers in this standard form. Using this two rectype declarations, for the addition function fun add em=m |addne=n |add(zn) (zm) = z(add n m) |add(on) (zm) = o(add n m)
3.1. REFINED ALGEBRAIC DATA-TYPES 53 |add(zn) (om) = o(add n m) |add(on) (om) = z(add (add (oe)n)m) the refinement type system can infer the following type: ?e!?e!?e^ ?e!stdpos !stdpos ^ ?e!std !std ^ ?e!bitstr !bitstr ^ stdpos !?e!stdpos ^ stdpos !stdpos !stdpos ^ stdpos !std !stdpos ^ stdpos !bitstr !bitstr ^ std !?e!std ^ std !stdpos !stdpos ^ std !std !std ^ std !bitstr !bitstr ^ bitstr !?e!bitstr ^ bitstr !stdpos !bitstr ^ bitstr !std !bitstr ^ bitstr !bitstr !bitstr which uses ?e to represent the type of empty bitstrings. This type confirms that whenever two standard form bitstrings are given as parameters to add,thisfunction returns a standard form bitstring. 3.1.4 Type inference Type inference procedure is presented in Figure 3.1. This inference procedure relies on a first step to infer the proper ML type and then on a second pass of abstract interpretation to infer the refinements of previously computed ML type. The target language of this inference process is defined via the following grammar: exp ::= x|exp exp | x.exp | exp :refty | let x=exp in exp | fix x.exp As in [FP91], we use the following convention for symbols in the inference algorithm:
54 CHAPTER 3. REFINEMENT TYPES Inst `x:C:: Lif (x)=Sand C:: Lis an instance of S Appl `e:_iCi:: L1!L2`e0:_jC0 j:: L1 `ee0:_i,j apptype(Ci,C j)::L2 Abs ,x:Ci:: L1`e:Di:: L2for each Cithat is a refinement of L1 `x.e :^i(Ci!Di)::L1!L2 Let `e1:_iCi:: L1(,x:(close(,C i:: L1)) `e2:Di:: L2)for each Ci `let x=e1in e2:_iDi:: L2 Restrict `e:D:: LDD0 `(e:D0):D0:: L Fix1 `LOOP(f,y.e,?,L) Fix2 `LOOP(f,y.e,C1,L),f :C1:: L`y.e :C2:: L `LOOP(f,y.e,C2,L) Fix3 `LOOP(f,y.e,C,L),f :C:: L`y.e :C:: L `fixf.y.e :C:: L Figure 3.1: Type inference as a deductive system.
3.2. LOGICAL REFINEMENTS 55 e, e0expressions x, f ML variables Crefinement type in inf Drefinement type in unf LML type typing context Srefinement type scheme The notation `e:D:: Lis used to indicate that under the typing context ,the expression ehas refinement type Dwhich is in turn a refinement of the ML type L. The inference process uses the auxiliary judgment LOOP to compute successive approximations to the refinement type of recursive functions until it reaches a fixpoint. This operation always terminates, since the number of refinements for an ML type is finite. In the rule Let,weusethefunctionclose(,C :: L). This function behaves much like the type closure presented for Damas-Milner type system: it returns a type scheme which is the generalization of the free type variables in Cand Lthat are not free in . Considering the traditional call-by-value operational semantics for ML, the following theorem states that the inference process of Figure 3.1 is sound: Theorem 3.1.1 (Soundness of refinement type inference) If `M:D:: L and ereduces to v,then`v:D0:: Lfor some D0D. Proof. By induction on the reduction relation. 3.2 Logical refinements An other form of refinement type system consists in augmenting the type language so types can be annotated with logical assertions. Consider for instance the following OCaml program that computes the division of two integer values: let div xy=x/y;; The OCaml inference engine infers for div the type int !int !int
56 CHAPTER 3. REFINEMENT TYPES Although the previous type states that for any two integer arguments the function div will return an integer value, it is well known that this function is not defined when y=0. Using a more expressive type system, instead of assigning the second argument of div the type int, we could specify that this function is defined only when the second argument is a value belonging to Z\{0}. Arefinementtypeoftheform{x:B|}stands for the set of terms Mof basic type B(such as integers or booleans), such that the formula [M/x]holds. As an example, we could represent the integer values from 0 to 5 as {x:int |x0^x5} The div function can now be assigned the type x:int !{y:int |y6=0}!int We present a refinement type system closely following the one presented in [Fla06, KF10]. 3.2.1 Syntax The set of terms considered for this system will be the set of -terms extended with constants: M,N ::= x|x:S. M |MN |c v::= x:S. M |c The type language is the great novelty of this kind of type systems: S, T ::= x:S!T|{x:B|} B::= Int |Bool Dependent function types [Car88] are introduced using the syntax x:S!T,meaning that Sis the domain type of the function and that the formal parameter xmay occur inside the co-domain type T.Anequivalentsyntaxis⇧x:S. T. Base refinement types are types of the form {x:B|}
3.2. LOGICAL REFINEMENTS 57 where xis a bound variable of basic type Bthat can appear inside the refinement predicate .Forsimplicity,weconsiderinthislanguagethatBranges over the basic types Int and Bool.Acomputationalunderstandingofbasicrefinementtypesisthat the type {x:B|}denotes the set of constants cof type Bthat satisfy the expression i.e., for which the term [c/x]evaluates to true. Basic types can then be though of as the basic refinement type {x:B|true} The set of constants cincludes arithmetic operators (as primitive functions), literal and boolean integers and symbols for if-then-else structures and a fixpoint operator. The types of constants are very precise and should clearly encode their semantics, like the following: true :{b:Bool |b} ,:b1:Bool !b2:Bool !{b:Bool |b,(b1,b2)} n:{x:Int |x=n} +:n:Int !m:Int !{z:Int |z=n+m} +n:m:Int !{z:Int |z=n+m} =:n:Int !m:Int !{b:Bool |b,(n=m)} ifT:Bool !T!T!T fixT:(T!T)!T Abasic constant is a constant whose type is a base refinement type. For example, the type of an integer ndenotes the singleton set {x:Int |x=n}. Aprimitive function type is a constant with functional type. An example is the addition operator +, with type n:Int !m:Int !{z:Int |z=n+m} 3.2.2 Operational semantics The operational semantics for terms is defined via the reduction relation M!N, meaning that Mreduces to Nin a single reduction step. The relation !⇤is the reflexive-transitive closure of !. The reduction rules are those of the simply type -calculus, except for the application of a constant to a term: E- (x:S. M)v![v/x]M E-Prim cM !JcK(M) E-Compat M!N C[M]!C[N]
64 CHAPTER 3. REFINEMENT TYPES M,N ::= x|c|x.M |MN |if Ethen Melse N| let x=Min N|let rec f=x.M in N| [⇤↵]M|[⌧]M v::= x|x.M Q::= true |q|Q^Q B::= Int |Bool T(B)::={⌫:B|B}|x:T(B)!T(B)|↵ S(B)::=T(B)|8↵.S(B) ⌧,::= T(true),S(true) T,S ::= T(E),S(E) ˆ T, ˆ S::= T(Q),S(Q) Figure 3.3: Syntax for Liquid Types. As for the previously seen general refinement type system, the set of basic types are integers and booleans. The possible refinements of a Liquid Type are represented by the syntactical category Q, which is either a single qualifier from Q(represented by q), a conjunction of qualifiers or the refinement true. The syntactical categories T(B)and S(B)stand for, respectively, types and types schemes skeletons. Types that can emerge during the process of type-checking are obtained by instantiating Bwith different sets of refinement expressions: ⌧and stand for, respectively, types and type schemes containing all refinements equal to true, and so represent ML types and type schemes; Binstantiated to E(which denotes arbitrary boolean expressions) results in general refinement types, represented by Tand S;LiquidTypesandLiquidTypes schemes are obtained when one uses only conjunctions of qualifiers from Qand are represented in Figure 3.3 by ˆ Tand ˆ S. The set of constants is much similar to the one described for the general refinement type system. Each constant has a refinement type that precisely captures their semantics. 3.3.2 Operational semantics The operational semantics for Liquid Types resembles very much the one presented for the general refinement type system. The reduction rules are presented in Figure 3.4. The main difference lies on the use of J·K:LiquidTypessystemconsideritasan
3.3. LIQUID TYPES 65 E- (x.M)v![v/x]M E-Prim cM !JcK(M) E-If-True if true then Melse N!M E-If-False if false then Melse N!N E-Let let x=vin M![v/x]M E-Compat M!N C[M]!C[N] Figure 3.4: Liquid Types system small-step operational semantics. embedding of terms into the decidable logic of equality,uninterpreted functions and linear arithmetic [Nel80]. This embedding is done by encoding literals and primitive functions to corresponding terms in the logic, and encoding other terms (such as - abstractions or applications) with uninterpreted functions. Evaluation contexts are defined as follows: C::= [ ] |CM|vC|if Cthen Melse N|let x=Cin M 3.3.3 Type system Typing rules for Liquid Types system are presented in Figure 3.5. Three different judgments are presented: •Well-formedness `S,statingthattherefinementtypeschemaSis wellformed under the type environment ; •Subtype judgment `S1<:S2,statingthattherefinementtypeschemeS1 is a subtype of scheme S2under ; •Liquid type judgment `QM:S,statingthat,usingthequalifiersQ,term Mhas type scheme Sunder . Some points from the typing judgment worth a particular explanation. The rule LTVar-B is used when the type of the variable is a basic refined type. In this case, we ignore the refinement expression Eand end up using only ⌫=x. The rule LT-App presents a substitution on the type of the application. This substitution conforms to the dependent types theory, and forces the formal parameter of the function to be substituted inside the refinement expressions of Tby the concreted parameter N.
66 CHAPTER 3. REFINEMENT TYPES LT-Sub `QM:S1`QS1<:S2`QS2 `QM:S2 LT-Var-B (x)={⌫:B|E} `Qx:{⌫:B|⌫=x} LT-Var (x)not a base type `Qx:(x) LT-App `QM:(x:Tx!T)`QN:Tx `QMN :[N/x]T LT-Fun ;x:ˆ Tx`QM:ˆ T`Q(x:ˆ Tx!ˆ T) `Qx.M :(x:ˆ Tx!ˆ T) LT-Const `Qc:ty(c) LT-Let `QM:S1;x:S1`QN:ˆ T`ˆ T `Qlet x=Min N:ˆ T LT-If `QE:bool ;E`QM:ˆ T;¬E`QN:ˆ T`ˆ T `Qif Ethen Melse N:ˆ T LT-Gen `QM:S↵62 `[⇤↵]M:8↵.S LT-Inst `QM:8↵.S `Qˆ TShape(ˆ T)=⌧ `Q[⌧]M:[ˆ T/↵]S Dec-<:-Base Valid(JK^JE1K)JE2K) `{⌫:B|E1}<:{⌫:B|E2} Dec-<:-Fun `T0 x<:Tx;x:T0 x`T<:T0 `(x:Tx!T)<:(x:T0 x!T0) <:-Var `↵<:↵ <:-Poly `S1<:S2 `8↵.S1<:8↵.S2 WT-Base ;⌫:B`E:bool `{⌫:B|E} WT-Var `↵ WT-Fun ;x:Tx`T `(x:Tx!T) WT-Poly `S `8↵.S Figure 3.5: Typing rules for Liquid Types.
3.3. LIQUID TYPES 67 Finally, rule LT-Inst presents the function Shape(·), which takes a Liquid Type as argument and returns the corresponding the ML type, i. e. the same type but with refinement expressions equal to true. To avoid the undecidability problems of checking subtyping between refinement types, Liquid Types system uses the rule [Dec-<:-Base]. A base refinement type {⌫:B|E1} is a subtype of {⌫:B|E2}if the predicate Valid(JK^JE1K)JE2K)returns true. Operationally, this rule indicates that under the type assumptions of and E1the predicate E2holds. The embedding of a typing context into the decidable logic is defined as follows: JK⌘^{E|E2}^^{J[x/⌫]EK|x:{⌫:B|E}2} As an example, the subtyping relation x:int;y:int;x>y`{⌫=x}<:{x ⌫^y⌫}holds as the following implication is valid in the decidable logic: ((true ^true ^x>y)^(⌫=x)) )(x⌫^y⌫) 3.3.4 Properties To state type safety of the Liquid Types system, we assume variables are bound at most once in any typing context, using the traditional ↵-renaming of bound variables if necessary. Directly stating subject reduction for the judgment `QM:Swould fail since the conservative subtyping relation makes it hard to prove a substitution lemma. So, the proof of safety for Liquid Types proceeds in two steps: first, we define an exact version of the type system with judgment `M:S, whose rules use an undecidable subtyping notion (defined via consistent substitutions, as in the rules of Figure 3.2); then, we state weakening, narrowing and substitution lemmas for the undecidable system, obtaining subject reduction and progress results for that system; finally, we show that the decidable type system over approximates the undecidable one i.e., if `QM:Sthen `M:S. A slightly different definition for the type of constants is needed in order prove the results of subject reduction and progress. Also, we define a relation between the encoding of subtyping implications into the decidable logic and subtype checking using consistent substitutions: Definition 3.3.1 (Type of constants) For each c2Constant: •chas a well-formed type, formally ;`ty(c);
68 CHAPTER 3. REFINEMENT TYPES •If ty(c)is x:T1!T2,thenforallvaluesvsuch that ;`v:T1,JcK(v)is defined and, ;`JcK(v):[v/x]T2; •If ty(c)is {⌫:B|M},thenM⌘⌫=c. Definition 3.3.2 (Embedding) The embedding J·Kis defined as a map from expressions and environments to formulas in a decidable logic such that for all ,M,N,if `M:bool,`N:bool,Valid(JK^JMK)JNK),then`M)N. Theorem 3.3.1 (Overapproximation) If `QM:S,then`M:S. Proof. By induction on derivation `QM:S,usingdefinition3.3.2. Theorem 3.3.2 (Subject reduction) If `M:Sand M!N,then`N:S. Proof. By induction on the derivation `M:S,usingthesubstitutionlemma. Theorem 3.3.3 (Progress) If ;`M:Sand Mis not a value, then there exists a Nsuch that M!N. Proof. By induction on the derivation ;`M:S. 3.3.5 Liquid Type inference The Liquid Types inference algorithm proceeds in three steps: 1. since every refinement type is a refinement of the correspondent ML type, Liquid Types invoke Damas-Milner inference to infer the types of sub terms and create templates for the (still) unknown refinement expressions; 2. following the typing rules of Figure 3.5 a set of constraints is generated, which will have a solution only if the term has a valid Liquid Type derivation. 3. finally, the algorithm uses the set Qto solve the constraints, using a similar technique to predicate abstraction. Atemplate is a Liquid Type refining a valid ML type but where the refinement predicates are replaced with liquid type variables, representing unknown expressions. For instance, for the term x. xrepresenting the negation function, Damas-Milner type inference would infer the type int !int.LiquidTypeswouldgeneratethe
3.3. LIQUID TYPES 69 Cons(,x)=ifHM(Shape(),x)=Bthen ({⌫:B|⌫=x},;) else ((x),;) Cons(,c)=(ty(c),;) Cons(,M 1M2)=let(x:Fx!F,C1)=Cons(,M 1)in let (F0 x,C2)=Cons(,M 2)in ([M2/x]F,C1[C 2[{`F0 x<:Fx}) Cons(,x.M)=let(x:Fx!F)=Fresh(HM(Shape(),x.M)) in let (F0,C)=Cons(;x:Fx,M)in (x:Fx!F,C[{`x:Fx!F}[ {;x:Fx`QF0<:F}) Cons(,if Mthen N1else N2)=letF= Fresh(HM(Shape(),if Mthen N1else N2)) in let (,C1)=Cons(,M)in let (F2,C2)=Cons(;M,N1)in let (F3,C3)=Cons(;¬M,N2)in (F,C1[C 2[C 3[{`F}[ {;M`F2<:F}[{;¬M`F3<:F}) Cons(,let x=Min N)=letF= Fresh(HM(Shape(),let x=Min N)) in let (F1,C1)=Cons(,M)in let (F2,C2)=Cons(;x:F1,N)in (F,C1[C 2[{`F}[{;x:F1`F2<:F}) Cons(,[⇤↵]M)=let(F,C)=Cons(,M)in (8↵.F, C) Cons(,[⌧]M)=letF= Fresh(⌧)in let (8↵.F0,C)=Cons(,M)in ([F/↵]F0,C[{`F}) Figure 3.6: Liquid Type constraints generation algorithm.
70 CHAPTER 3. REFINEMENT TYPES Weaken(`{⌫:B|✓·k},A)= A[k7! {q|q2A(k)}and Shape(); ⌫:B`✓·q:bool}] Weaken(`{⌫:B|⇢}<:{⌫:B|✓·k})= A[k7! {q|q2A(k)}and JA()K^JA(⇢)K)J✓·qK}] Weaken() = Failure Solve(C,A)= if exists c2Csuch that A(c)is not valid then Solve(C,Weaken(c, A)) else A Infer(,M,Q)= let (F,C)=Cons(,M)in let A= Solve(Split(C),k.Inst(,M,Q)) in A(F) Figure 3.7: Constraint solving algorithm. template x:{⌫:int |k1}!{⌫:int |k2}, where k1and k2serve as placeholders for future refinement expressions. Constraint generation algorithm is presented in Figure 3.6. This algorithm traverses terms in a syntax-directed manner, generating subtyping and well-formedeness constraints. Well-formedeness constraints are of the form `F,statingthatthepossible refinement expressions of template Fshould only contain program variables bounded by .Subtypingconstraintsareoftheform`F1<:F2, which ensure that the subtype relation for templates F1and F2can be checked using appropriate subsumption rules. The algorithm divides the set of terms into those whose types can be computed from the typing context and types of sub-terms, and those whose types can only be constructed from freshly generated templates. For the first category we include variables, constants, function applications and polymorphic generalizations. The second one contains -abstractions, if-then-else constructor, let-bindings and polymorphic instantiations. These last terms represent the ones for which one needs to previously call Damas-Milner inference, using function HM(·),andgeneratefresh templates, using the function Fresh(·)(Fresh(·)can be lifted to typing contexts). Constraint solving algorithm is presented in Figure 3.7. A central notion to this algorithm is that of Liquid Type Assignment:aLiquidTypeAssignmentAover a set of logical qualifiers Qis a map from liquid type variables to conjunctions of predicates from Q.UsingthenotionofLiquidTypeAssignment,wedescribenowhowthesolving
3.3. LIQUID TYPES 71 process works: •for all generated templates, liquid types are assigned the conjunction of all qualifiers from Q⇤,denotedasInst(,M,Q)and defined as {q|q2Q?and FV(q)✓{⌫}[Var()[Var(M)} where Var()and Var(M)are the set of variables from and M,respectively. •the Solve(·,·)function repeatedly picks a constraint that is not satisfied by the current assignment of qualifiers from Q?to liquid type variables, and calls Weaken(·,·)to remove the qualifiers that prevent the constraint from holding. Weakening works via the following criteria: –for unsatisfied constraints of the form `{⌫:B|✓·k},Weaken(·,·) removes from the assignment for kall the qualifiers qsuch that the ML type of ✓·q(the result of applying the substitution ✓to q, following the conclusion of rule [LT-App]) cannot be checked to be bool under context Shape(); ⌫:B; –for `{⌫:B|⇢}<:{⌫:B|✓·k},Weaken(·,·)removes from the assignment for kall the logical qualifiers qsuch that the implication JA()K^JA(⇢)K) J✓·qKis not valid in the decidable logic; –if the constraint is of the form `{⌫:B|⇢}<:{⌫:B|M},thenallthe inference process fails. We show how the inference algorithm proceeds to infer the type of the max. The target program is let max xy= if x>ythen xelse y and the selected set of qualifiers is Q={0⌫,?⌫,⌫<?,⌫<len ?} The algorithm begins by invoking Damas-Milner inference engine, which returns the type int !int !int.Forthistype,Fresh(·)generates the template x:{⌫: int |kx}!y:{⌫:int |ky}!{⌫:int |k}, where kx,k yand kare liquid types variables representing the unknown refinements for the formals x, y and the body of max, respectively. We will write x:kx!y:ky!kfor simplicity.
72 CHAPTER 3. REFINEMENT TYPES The second step of the algorithm is to generated the set of subtyping and wellformedness constraints. As the body of max is an if-then-else expression, Liquid Types system generates the following constraints: x:kx;y:ky;(x>y)`{⌫=x}<:k(3.1) x:kx;y:ky;¬(x>y)`{⌫=x}<:k(3.2) Constraint (3.1) (respectively (3.2)) states that when xand yhave the types kxand ky,respectively,andx>yholds (resp. ¬(x>y))shouldbeasubtypeoftheif body (resp. else), k. Finally, the liquid types are assigned the conjunctions of qualifiers in Q?;being iteratively removed those that make any constraint unsatisfiable. For the case of max,wecanonlyassignkxand kythe refinement true,sincenoneofthegenerated constraints limits their acceptable types. For k,thealgorithm(possiblyusingan automatic theorem prover) infers that the strongest solution for kthat satisfies both constraints is x⌫^y⌫. The Liquid Type inferred for max is then max :x:{⌫:int |true}!y:{⌫:int |true}!{⌫:int |(x⌫)^(y⌫)} To conclude the presentation of Liquid Type system, we state the correctness and completeness of Liquid Types inference algorithm. Theorem 3.3.4 (Termination) Infer(,M,Q)terminates. Proof. Follows by the termination property of Damas-Milner inference and the fact the set Qis finite. Definition 3.3.3 (Minimum solution of liquid assignment) For two liquid assignments Aand A0,wesaythatAA0if for all liquid variables k,thesetoflogical qualifiers A(k)contains the set of logical qualifiers A0(k).ForC,asetofconstraints, A⇤is the minimum solution over Qif •A⇤(C)is valid; •for each Aover Q,ifA(C)then A⇤A. Theorem 3.3.5 (Constraint generation) For every typing context and term M such that Cons(,M)=(F,C),`QM:Siffthere is an assignment Aover Qto liquid type variables such that A(F)=Sand A(C)is valid.
3.3. LIQUID TYPES 73 Proof. Only if ()): by induction on the derivation `QM:S. If ((): by structural induction over M. Theorem 3.3.6 (Constraint solving) For every set of constraints Cand qualifiers Q, 1. if Solve(C,k.Q)returns A,thenAis the minimum solution for Cover Q; 2. if Solve(C,k.Q)returns Failure,thenChas no solution over Q. Proof. 1. By induction over n, where nis the number of iterations of the loop in Solve(·,·); 2. Supposing Solve(·,·)fails, but that there is a valid solution Afor Cover Q,we know there is a minimum solution A⇤over Qand AA0. The only situation Solve(·,·)may fail is when the constraint is of the form `Qb)e, where bis either an expression or a liquid variable with a substitution, and JA()K^JA(b)K6) JeK Now, as AA⇤,wehave JA()K)JA⇤()K JA(b)K)JA⇤(b)K and therefore, JA⇤()K^JA⇤(b)K6) JeK This contradicts the definition of minimum solution, and so there is no valid solution for Cover Q. Corollary 3.3.1 (Soundness of inference) If Infer(,M,Q)=S,then`QM:S. Corollary 3.3.2 (Completeness of inference) If Infer(,M,Q) = Failure,then there is no Ssuch that `QM:S. Corollaries 3.3.1 and 3.3.2 follow as corollaries of theorems 3.3.5 and 3.3.6 and the definition of minimum solution.
80 CHAPTER 4. LIQUID INTERSECTION TYPES Liquid Intersection Type checking `\ QM: Sub `\ QM:1`\12`\2 `\ QM:2 Intersect `\ QM:⌧1`\ QM:⌧2⌧1\⌧2:: T `\ QM:⌧1\⌧2 Va r - B (x)=⌧1\...\⌧n⌧i:: B(8i:1in) `\ Qx:{⌫:B|⌫=x} Va r (x)not a base type (x)::T `\ Qx:(x) App `\ QM:(x:⌧x!⌧)`\ QN:⌧x `\ QMN :[N/x]⌧ Fun ;x:ˆ⌧x`\ QM:ˆ⌧`\ˆ⌧ˆ⌧:: T `\ Qx.M :(x:ˆ⌧x!ˆ⌧) Const `\ Qc:ty(c) Let `\ QM:;x:`\ QN:ˆ⌧`\ˆ⌧ `\ Qlet x=Min N:ˆ⌧ Gen `\ QM:↵62 `\ Q[⇤↵]M:8↵. Inst `\ QM:8↵.`\ˆ⌧Shape(ˆ⌧)=T `\ Q[T]M:[ˆ⌧/↵] Subtyping `\12 -Base Valid(JK^(JE1K^...^JEnK))(JE0 1K^...^JE0 mK)) `\{⌫:B|E1}\...\{⌫:B|En}{⌫:B|E0 1}\...\{⌫:B|E0 m} -Intersect-Fun `\(x:⌧x!⌧1)\(x:⌧x!⌧2)(x:⌧x!⌧1\⌧2) -Elim `\⌧1\⌧2⌧i i2{1,2} -Fun `\⌧0 x⌧x;x:⌧0 x`\⌧⌧0 `\x:⌧x!⌧x:⌧0 x!⌧0 -Var `\↵↵ -Intersect `\⌧⌧1`\⌧⌧2 `\⌧⌧1\⌧2 -Poly `\12 `\8↵.18↵.2 Well formed types `\ WF-B ;⌫:B`\E:bool `\{⌫:B|E} WF-Var `\↵ WF-Fun ;x:⌧x`\⌧ `\x:⌧x!⌧ WF-Poly `\ `\8↵. WF-Intersect `\⌧1`\⌧2 `\⌧1\⌧2 Figure 4.3: Typing rules for Liquid Intersection Types.
4.3. TYPE SYSTEM 81 be derived for a program. The subtyping relation presents some typical rules for a system with intersection types. These allow to capture the relations at the level of intersections in types, with no concern for the refinements of the two types being compared. On the other side, comparing two refined base types reduces to the check of an implication formula between the refinement expressions. Our system uses a decidable notion of implication in the rule [-Base], by embedding environments and refinement expressions into the decidable logic. The embedding of environments is defined as JK,^{(J1K^...^JnK)[x/⌫]|x:{⌫:B|1}\...\{⌫:B|n}2} Given that every implication expression generated in rule [-Base] is decidable, it is then suitable to be discharged by some automatic theorem prover, like an SMT solver. So, type-checking in our system can be seen as a typing-and-proof process. We show an example of a derivation for the term x. x,usingQ={⌫0,⌫0}. With =x:{⌫0},consider: D0 1: Const `\ Q:(y:int !{⌫=y}) Sub Va r - B (x)={⌫0} `\ Qx:{⌫=x} -Base Valid(x0^⌫=x)>) `\{⌫=x}int `\ Qx:int `\ Qx:{⌫=x} and: D1: D0 1 Valid(x0^⌫=x)⌫0) `\{⌫=x}{⌫0}-Base `\ Qx:{⌫0} Sub `\ Qx. x:(x:{⌫0}!{⌫0}) Fun We can also derive `\ Qx. x:(x:{⌫0}!{⌫0}), with 0=x:{⌫0}: D0 2: Const 0`\ Q:(y:int !{⌫=y}) Sub Va r - B 0(x)={⌫0} 0`\ Qx:{⌫=x} -Base Valid(x0^⌫=x)>) 0`\{⌫=x}int 0`\ Qx:int 0`\ Qx:{⌫=x}
82 CHAPTER 4. LIQUID INTERSECTION TYPES and: D2: D0 2 Valid(x0^⌫=x)⌫0) 0`\{⌫=x}{⌫0}-Base 0`\ Qx:{⌫0} Sub `\ Qx. x:(x:{⌫0}!{⌫0}) Fun Finally we have: D1D2 `\ Qx. x:(x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0}) Intersect We explain in more detail some important aspects of the previous derivation: •instead of {⌫:B|E}we simply write {E}, whenever Bis clear from the context; •the type int stands for refinement-free integers values, i.e. {⌫:int |>},andso that is why >shows up in some uses of the subsumption rule. •for the presented type checking example, the following implications should be verified: x0^⌫=x)> x0^⌫=x)⌫0 x0^⌫=x)> x0^⌫=x)⌫0 All of them are easily discharged using any automatic theorem prover; •we omit the well-formedness and well-founded sub-derivations, since they are trivially constructed. We present a more involving example of a type derivation in our system. As stated in Section 3, for the term x.x ⇤xit would be of much interest to have a derivation showing that no matter which value is given to this function, it always returns a positive or zero value. So, we show how to use our system to derive the type (x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0})for x.x ⇤x.Usingagain Q={⌫0,⌫0}and with =x:{⌫0},consider: D000 3: Va r - B (x)={⌫0} `\ Qx:{⌫=x} Valid(x0^⌫=x)>) `\{⌫=x}> -Base `\ Qx:int Sub
4.3. TYPE SYSTEM 83 and D00 3: Const `\ Q⇤:(z:int !y:int !{⌫=z⇤y})D000 3 `\ Q⇤x:(y:int !{⌫=x⇤y}) App† and D0 3: D00 3 Va r - B (x)={⌫0} `\ Qx:{⌫=x} Valid(x0^⌫=x)>) `\{⌫=x}> -Base `\ Qx:int Sub `\ Qx⇤x:{⌫=x⇤x} App‡ and D3: D0 3 Valid(x0^⌫=x⇤x)⌫0) `\x⇤x:{⌫=x⇤x}{⌫0}-Base `\ Qx⇤x:{⌫0} Sub `\ Qx.x ⇤x:(x:{⌫0}!{⌫0}) Abs We call the attention to the uses of rule [App] marked with †and ‡.Forboththese cases it is possible to realize how substitution in refinement predicates works: for the case †the type of ⇤xis (y:int !{v=x⇤y}),thatis,wesubstitutedinthetypeof the constant 0⇤0the term zfor x;onthecase‡,wehaveforx⇤xthe type {⌫=x⇤x}, which results from substituting in the type {⌫=y⇤x}the term yfor x. Similarly to the previous, we can derive `\ Qx.x⇤x:(x:{⌫0}!{⌫0}).Taking 0=x:{⌫0},wehave: D000 4: Va r - B 0(x)={⌫0} 0`\ Qx:{⌫=x} Valid(x0^⌫=x)>) 0`\{⌫=x}> -Base 0`\ Qx:int Sub and D00 4: Const 0`\ Q⇤:(z:int !y:int !{⌫=z⇤y})D000 4 0`\ Q⇤x:(y:int !{⌫=x⇤y}) App
84 CHAPTER 4. LIQUID INTERSECTION TYPES and D0 4: D00 4 Va r - B 0(x)={⌫0} 0`\ Qx:{⌫=x} Valid(x0^⌫=x)>) 0`\{⌫=x}> -Base 0`\ Qx:int Sub 0`\ Qx⇤x:{⌫=x⇤x} App and D4: D0 4 Valid(x0^⌫=x⇤x)⌫0) 0`\x⇤x:{⌫=x⇤x}{⌫0}-Base 0`\ Qx⇤x:{⌫0} Sub `\ Qx.x ⇤x:(x:{⌫0}!{⌫0}) Abs Finally, we can intersect the two derived types and derive the desired type: D3D4 `\ Qx.x ⇤x:(x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0}) Intersect 4.4 Properties In order to prove soundness properties of our system we follow the approach of [RKJ08, VRJ13]. The decidable notion of implication checking employed by the subtyping rules is a problem when it comes to prove a substitution lemma. So, instead we prove subject reduction for a version of our system with undecidable subtyping and unrestricted expressions in refinement predicates. The typing judgment in this system will be denoted by `\M:,andtheinferencerulesarepresentedinFigures4.4 and 4.5. Then, we show that any derivation in the decidable system has a counter-part in the undecidable one. Definition 4.4.1 (Constants) Each constant c has a type ty(c)such that: 1. ;` \ty(c); 2. if c is a primitive function then it cannot get stuck, if `\cvthen JcK(v)is defined and if `\cM:and JcK(M)is defined then `\JcK(M):; 3. if ty(c)is {⌫:B|}then ⌘⌫=c.
4.4. PROPERTIES 85 Refinement Intersection type checking `\M: Sub `\M:1`\12`\2 `\M:2 Intersect `\M:⌧1`\M:⌧2⌧1\⌧2:: T `\M:⌧1\⌧2 Va r - B (x)=⌧1\...\⌧n⌧i:: B(8i:1in) `\x:{⌫:B|⌫=x} Va r (x)not a base type (x)::T `\x:(x) App `\M:(x:⌧x!⌧)`\N:⌧x `\MN :[N/x]⌧ Fun ;x:⌧x`\M:⌧`\⌧⌧:: T `\x.M :(x:⌧x!⌧) Const `\c:ty(c) Let `\M:;x:`\N:⌧`\⌧ `\let x=Min N:⌧ Gen `\M:↵62 `\[⇤↵]M:8↵. Inst `\M:8↵.`\⌧Shape(⌧)=T `\[T]M:[⌧/↵] Implication `\E)E0 Imp `\E:bool `\E0:bool 8⇢.(|=⇢and ⇢(E)⇤ >implies ⇢(E0)⇤ >) `\E)E0 Subtyping `\12 -Base ;⌫:B`\E1^...^En)E0 1^...^E0 m `\{⌫:B|E1}\...\{⌫:B|En}{⌫:B|E0 1}\...\{⌫:B|E0 m} -Intersect-Fun `\(x:⌧x!⌧1)\(x:⌧x!⌧2)(x:⌧x!⌧1\⌧2) -Elim `\⌧1\⌧2⌧i i2{1,2} -Fun `\⌧0 x⌧x;x:⌧0 x`\⌧⌧0 `\(x:⌧x!⌧)(x:⌧0 x!⌧0) -Var `\↵↵ -Intersect `\⌧⌧1`\⌧⌧2 `\⌧⌧1\⌧2 -Poly `\12 `\8↵.18↵.2 Figure 4.4: Refinement Intersection typing rules
86 CHAPTER 4. LIQUID INTERSECTION TYPES Well formed types `\ WF-B ;⌫:B`\:bool `\{⌫:B|} WF-Var `\↵ WF-Fun ;x:⌧x`\⌧ `\(x:⌧x!⌧) WF-Poly `\ `\8↵. WF-Intersect `\⌧1`\⌧2 `\⌧1\⌧2 Consistent substitutions |=⇢ CS-Empty ;|=; CS-Ext |=⇢;` \V:⇢() ;x:|=⇢;[V/x] Figure 4.5: Rules for well formed Refinement Intersection Types and consistent substitutions. Definition 4.4.2 (Embedding) The embedding J·Kis defined as a map from terms and environments to formulas in the decidable logic such that for all ,E,E0if `\ E:bool,`\E0:bool,Valid(JK^JEK)E0),then`\E)E0. Definition 4.4.3 (Substitution) We define substitution on types, ⇢(), as follows: ⇢(↵)=↵ ⇢({⌫:B|E})={⌫:B|⇢(E)} ⇢(x:⌧x!⌧)=x:⇢(⌧x)!⇢(⌧) ⇢(8↵.)=8↵.⇢() ⇢(⌧1\⌧2)=⇢(⌧1)\⇢(⌧2) The previous definition explains how substitutions, arising from the use of the App rule, work over the refinement expressions of types. A substitution ⇢(mapping variables to terms) is either empty (denoted by ;), or ⇢is of the form ⇢0;[V/x]meaning that ⇢0is a substitution extended with the case where xis substituted by V.A substitution is required to be consistent with respect to some typing context, as shown in Figure 4.5. For the empty substitution, this will only be consistent with respect to the empty tying context. If ⇢is of the form (⇢0;x:= V),then⇢will be consistent with a context ;x:if Vis a value of type ⇢()(the part ⇢0of the substitution is
4.4. PROPERTIES 87 propagated to the type assigned to V)and⇢0is consistent with . The rule CS-Ext from Figure 4.5 captures this behavior. Asubstitutioncanbeliftedtotypingcontextsasexpected: ⇢(;)=; ⇢(;x:)=⇢(); x:⇢() Definition 4.4.4 (Domain of a substitution) The domain of a substitution, Dom(⇢), is defined as follows: Dom(;)={} Dom(⇢;[V/x]) = Dom(⇢)[{x} Lemma 4.4.1 (Substitution permutation) If |=⇢1;⇢2then 1. Dom(⇢1)\Dom(⇢2)=;; 2. for all Liquid Intersection Type ,⇢1;⇢2()=⇢2;⇢1(). Proof. 1. By induction on the derivation |=⇢1;⇢2, splitting cases on which rule was used at the bottom. •case [CS-Empty]: For this case we have ⇢1;⇢2=; and so Dom(⇢1)\Dom(⇢2)=;. •case [CS-Ext]: For this case we have = 0;x:0 ⇢2=⇢0 2;[V/x] By inversion on the rule [CS-Ext] 0|=⇢1;⇢0 2 ;`V:⇢1;⇢0 2(0) By IH Dom(⇢1)\Dom(⇢0 2)=; A variable is bounded at most once within a typing context, so x62 Dom(0). This implies that x62 Dom(⇢1;⇢0 2)since this substitution is consistent with 0. Given Dom([V/x]) = {x}we can conclude that Dom(⇢1)\Dom(⇢2)\ Dom([V/x]) = ;, which is the desired conclusion.
88 CHAPTER 4. LIQUID INTERSECTION TYPES 2. By induction on the structure of . •case ={⌫:B|E}:Wehave ⇢1;⇢2({⌫:B|E})={⌫:B|⇢1;⇢2(E)} Using (1) we can conclude that every variable is substituted at most once and since Eis a boolean expression we have ⇢1;⇢2(E)=⇢2;⇢1(E) By the definition of substitution ⇢1;⇢2({⌫:B|E})={⌫:B|⇢1;⇢2(E)} ={⌫:B|⇢2;⇢1(E)} =⇢2;⇢1({⌫:B|E}) •case =x:⌧x!⌧:Wehave ⇢1;⇢2(x:⌧x!⌧)=x:⇢1;⇢2(⌧x)!⇢1;⇢2(⌧) By IH ⇢1;⇢2(⌧x)=⇢2;⇢1(⌧x) ⇢1;⇢2(⌧)=⇢2;⇢1(⌧) By the definition of substitution ⇢1;⇢2(x:⌧x!⌧)=x:⇢1;⇢2(⌧x)!⇢1;⇢2(⌧) =x:⇢2;⇢1(⌧x)!⇢2;⇢1(⌧) =⇢2;⇢1(x:⌧x!⌧) •case =⌧1\⌧2:Wehave ⇢1;⇢2(⌧1\⌧2)=⇢1;⇢2(⌧1)\⇢1;⇢2(⌧2) By IH ⇢1;⇢2(⌧1)=⇢2;⇢1(⌧1) ⇢1;⇢2(⌧2)=⇢2;⇢1(⌧2) By the definition of substitution ⇢1;⇢2(⌧1\⌧2)=⇢1;⇢2(⌧1)\⇢1;⇢2(⌧2) =⇢2;⇢1(⌧1)\⇢2;⇢1(⌧2) =⇢2;⇢1(⌧1\⌧2)
4.4. PROPERTIES 89 •case =↵:Trivial. •case =8↵.0:Wehave ⇢1;⇢2(8↵.0)=8↵.⇢1;⇢2(0) By IH ⇢1;⇢2(0)=⇢2;⇢1(0) By the definition of substitution ⇢1;⇢2(8↵.0)=8↵.⇢1;⇢2(0) =8↵.⇢2;⇢1(0) =⇢2;⇢1(8↵.0) Lemma 4.4.2 (Well-formed substitutions) 1. If |=⇢1;⇢2then there are 1,2such that = 1; 2,Dom(⇢1)=Dom(1), Dom(⇢2)=Dom(2); 2. 1; 2|=⇢1;⇢2,Dom(⇢1)=Dom(1),Dom(⇢2)=Dom(2)iff1|=⇢1, ⇢12|=⇢2. Proof. 1. By induction on . •case =;:Forthiscasewehave 1= 2=; The only substitution that is consistent with the empty context is the empty one, so ⇢1=⇢2=; We can then conclude Dom(1)=Dom(⇢1) Dom(2)=Dom(⇢2)
96 CHAPTER 4. LIQUID INTERSECTION TYPES •case [WF-Poly]: By inversion `\ By IH 0`\ So, the following derivation is valid WF-Poly 0`\ 0`\8↵. •case [WF-Intersect]: By inversion `\⌧1 `\⌧2 By IH 0`\⌧1 0`\⌧2 So, the following derivation is valid WF-Intersect 0`\⌧10`\⌧2 0`\⌧1\⌧2 5. By induction on the derivation of `\M:, splitting cases on which rule was used at the bottom. •case [Sub]: By inversion `\M:1 `\12 `2 By IH, (3.) and (4.) 0`\M:1 0`\12 0`\2 So, the following derivation is valid Sub 0`\M:10`\120`\2 0`\M:2
4.4. PROPERTIES 97 •case [Intersect]: By inversion `\M:⌧1 `\M:⌧2 ⌧1\⌧2:: T By IH 0`\M:⌧1 0`\M:⌧2 So, the following derivation is valid Intersect 0`\M:⌧10`\M:⌧2⌧1\⌧2:: T 0`\M:⌧1\⌧2 •case [Var-B]: By inversion (y)=⌧1\···\⌧n ⌧i:: B(8i.1in) As y6=xwe have (y)= 0(y). So, the following derivation is valid Var-B 0(y)=⌧1\···\⌧n⌧i:: B(8i.11n) 0`\y:{⌫:B|⌫=y} •case [Var]: Very similar to the previous case. •case [App]: By inversion `\M:(y:⌧y!⌧) `\N:⌧y By IH 0`\M:(y:⌧y!⌧) 0`\N:⌧y So, the following derivation is valid App 0`\M:(y:⌧y!⌧) 0`\N:⌧y `\MN :[N/y]⌧ •case [Fun]: By inversion ;y:⌧y`\M:⌧ `\⌧ ⌧:: T
98 CHAPTER 4. LIQUID INTERSECTION TYPES By IH and (4.) 0;y:⌧y`\M:⌧ 0`\⌧ So, the following derivation is valid Fun 0;y:⌧y`\M:⌧0`\⌧⌧:: T 0`\y.M :(y:⌧y!⌧) •case [Const]: Easy, by the following derivation Const 0`\c:ty(c) •case [Let]: By inversion `\M: ;y:`\N:⌧ `\⌧ By IH and (4.) 0`\M: 0;y:`\N:⌧ 0`\⌧ So, the following derivation is valid Let 0`\M:0;y:`\N:⌧0`\⌧ 0`\let y=Min N:⌧ •case [Gen]: By inversion `\M: ↵62 By IH 0`\M: We still have ↵62 0,since0only differs from by the binding x:x. So, the following derivation is valid Gen 0`\M:↵62 0 0`\[⇤↵]M:8↵.
4.4. PROPERTIES 99 •case [Inst]: By inversion `\M:8↵. `\⌧ Shape(⌧)=T By IH and (4.) 0`\M:8↵. 0`\⌧ So, the following derivation is valid Inst 0`\M:8↵.0`\⌧Shape(⌧)=T 0`\[T]M:[⌧/↵] Lemma 4.4.4 (Substitution) If 1`\V:0 = 1;x:0; 2 0= 1;[V/x]2 then: 1. if |=⇢1;[V/x]⇢2then 0|=⇢1;⇢2; 2. if `\E)E0then 0`\[V/x]E)[V/x]E0; 3. if `\12then 0`\[V/x]1[V/x]2; 4. if `\then 0`\[V/x]; 5. if :: Tthen [V/x]:: T; 6. if `\M:then 0`\M:. Proof. By simultaneous induction on the derivations. 1. We split by cases on the structure of . •case =;: This case is void, since we assume contains at least x:0.
100 CHAPTER 4. LIQUID INTERSECTION TYPES •case = 1;x:0; 0 2;y:00:Forthiscase 2= 0 2;y:00 ⇢2=⇢0 2;[V0/y] By inversion on rule [CS-Ext]: 1;x:0; 0|=⇢1;[V/x]; ⇢2 ;` \V0:⇢1;[V/x]; ⇢0 2(00) We have that FV(V0)=;, since it is typed with an empty environment. By IH and (5.) 1;[V/x]0 2|=⇢1;⇢0 2 ;` \[V/x]V0:[V/x](⇢1;[V/x]; ⇢0 2)(00) Since ⇢1;[V/x]; ⇢0 2=⇢1;⇢0 2;[V/x], the following derivation is valid CS-Ext 1;[V/x]0 2|=⇢1;⇢0 2;` \[V/x]V0:[V/x](⇢1;⇢0 2)(00) 1;[V/x]0 2;y:[V/x]00 |=⇢1;⇢0 2;[[V/x]V0/y] Given that [V/x]V0=V0, the previous derivation could be written CS-Ext 1;[V/x]0 2|=⇢1;⇢0 2;` \[V/x]V0:[V/x](⇢1;⇢0 2)(00) 1;[V/x]0 2;y:[V/x]00 |=⇢1;⇢0 2;[V0/y] where 1;[V/x]0 2;y:[V/x]00 = 1;[V/x]2and ⇢1;⇢0 2;[V0/y]=⇢1;⇢2 2. By inversion on rule [Imp] `\E:bool `\E0:bool 8⇢.(|=⇢and ⇢(E)⇤ >implies ⇢(E0)⇤ > By (5.) 0`\[V/x]E:bool `\[V/x]E0:bool By the form of ,⇢must be of the form ⇢1;[V/x]; ⇢2,so 8⇢1,⇢ 2.(|=⇢1;[V/x]; ⇢2and ⇢1;[V/x]; ⇢2(E)⇤ >implies ⇢1;[V/x]; ⇢2(E0)⇤ >
4.4. PROPERTIES 101 We have ⇢1;[V/x]; ⇢2=⇢1;⇢2;[V/x],so 8⇢1,⇢ 2.(|=⇢1;[V/x]; ⇢2and ⇢1;⇢2;[V/x](E)⇤ >implies ⇢1;⇢2;[V/x](E0)⇤ > By (1.) 8⇢1,⇢ 2.(0|=⇢1;⇢2and ⇢1;⇢2;[V/x](E)⇤ >implies ⇢1;⇢2;[V/x](E0)⇤ > The following derivation is then valid Imp 0`\[V/x]E:bool `\[V/x]E0:bool 8⇢1,⇢ 2.(0|=⇢1;⇢2and ⇢1;⇢2;[V/x](E)⇤ >implies ⇢1;⇢2;[V/x](E0)⇤ > 0`\[V/x]E)[V/x]E0 3. By induction on the derivation of `\12, splitting cases on which rule was used at the bottom. •case [-Base]: By inversion ;⌫:B`\E1^···^En)E0 1^···^E0 m By IH (2.) and as [V/x]B=B 0;⌫:B`\[V/x](E1^···^En))[V/x](E0 1^···^E0 m) So, the following derivation is valid -Base 0;⌫:B`\[V/x](E1^···^En))[V/x](E0 1^···^E0 m) 0`\[V/x]({⌫:B|E1}\···\{⌫:B|En})[V/x]({⌫:B|E0 1}\···\{⌫:B|E0 m}) •case [-Intersect-Fun]: since [V/x](y:⌧y!⌧1)\[V/x](y:⌧y!⌧2)=(y:[V/x]⌧y![V/x]⌧1)\(y:[V/x]⌧y![V/x]⌧2) the desired conclusion holds by the following derivation -Intersect-Fun 0`\[V/x](y:⌧y!⌧1)\[V/x](y:⌧y!⌧2)[V/x](y:⌧y!⌧1\⌧2) •case [-Fun]: By inversion `\⌧0 y⌧y ;y:⌧0 y`\⌧⌧0
102 CHAPTER 4. LIQUID INTERSECTION TYPES By IH 0`\[V/x]⌧0 y[V/x]⌧y 0;[V/x]y:⌧0 y`\[V/x]⌧[V/x]⌧0 By the definition of substitution, the following derivation is valid -Fun 0`\[V/x]⌧0 y[V/x]⌧y0;[V/x]y:⌧0 y`\[V/x]⌧[V/x]⌧0 0`\y:[V/x]⌧y![V/x]⌧y:[V/x]⌧0 y![V/x]⌧0 •case [-Var]: Easy, by the following derivation -Var 0`↵↵ •case [-Elim]: By the definition of substitution, the desired conclusion holds by the following derivation -Left 0`[V/x]⌧1\[V/x]⌧2[V/x]⌧i i2{1,2} •case [-Intersect]: By inversion `\⌧⌧1 `\⌧⌧2 By IH 0`\[V/x]⌧[V/x]⌧1 0`\[V/x]⌧[V/x]⌧2 By the definition of substitution, the desired conclusion holds by the following derivation -Intersect 0`\[V/x]⌧[V/x]⌧10`\[V/x]⌧[V/x]⌧2 0`\[V/x]⌧[V/x]⌧1\[V/x]⌧2 •case [-Poly]: By inversion `\12 By IH 0`\[V/x]1[V/x]2 By the definition of substitution, the desired conclusion holds by the following derivation -Poly 0`\[V/x]1[V/x]2 0`\8↵.[V/x]18↵.[V/x]2
4.4. PROPERTIES 103 4. By induction on the derivation of `\, splitting cases on which rule was used at the bottom. •case [WF-B]: By inversion ;⌫:B`\E:bool By IH (6.): 0;⌫:[V/x]B`\E:bool Since [V/x]B=B, the desired conclusion holds by the following derivation WF-B 0;⌫:B`\E:bool 0`\{⌫:B|E} •case [WF-Var]: Easy, by the following derivation 0`\↵ •case [WF-Fun]: By inversion ;y:⌧y`\⌧ By IH 0;y:[V/x]⌧y`\[V/x]⌧ By the definition of substitution, the desired conclusion holds by the following derivation WF-Fun 0;y:[V/x]⌧y`\[V/x]⌧ 0`\y:[V/x]⌧y![V/x]⌧ •case [WF-Poly]: By inversion `\ By IH 0`\[V/x] By the definition of substitution, the desired conclusion holds by the following derivation WF-Poly 0`\[V/x] 0`\8↵.[V/x]
104 CHAPTER 4. LIQUID INTERSECTION TYPES •case [WF-Intersect]: By inversion `\⌧1 `\⌧2 By IH 0`\[V/x]⌧1 0`\[V/x]⌧2 By the definition of substitution, the desired conclusion holds by the following derivation WF-Intersect 0`\[V/x]⌧10`\[V/x]⌧2 0`\[V/x]⌧1\[V/x]⌧2 5. By induction on the derivation of :: T. This item clearly holds, since a substitution [V/x]only affects refinement expressions, maintaining the correspondent ML type. So, the derivation for :: Tis the same for [V/x]:: T. 6. By induction on the derivation of `\M:, splitting by cases on which rule is used at the bottom. •case [Sub]: By inversion `\M:1 `\12 `\2 By IH, (3.) and (4.) 0`\[V/x]M:[V/x]1 0`\[V/x]1[V/x]2 0`\[V/x]2 So, the following derivation is valid Sub 0`\[V/x]M:[V/x]10`\[V/x]1[V/x]20`\[V/x]2 0`\[V/x]M:[V/x]2 •case [Intersect]: By inversion `\M:⌧1 `\M:⌧2 ⌧1\⌧2:: T
4.4. PROPERTIES 105 By IH, and (5.) 0`\[V/x]M:[V/x]⌧ 0`\[V/x]M:[V/x]⌧2 ([V/x]⌧1\[V/x]⌧2)::T By the definition of substitution, the desired conclusion holds by the following derivation Intersect 0`\[V/x]M:[V/x]⌧1 0`\[V/x]M:[V/x]⌧2([V/x]⌧1\[V/x]⌧2)::T 0`\[V/x]M:[V/x]\[V/x]0 •case [Var-B]: By inversion (y)=⌧1\···\⌧n,⌧ i={⌫:B|Ei} ⌧i:: B(8i.1in) Two sub-cases follow: either y=xor y6=x; –sub-case y=x:Forthiscasewehave⌧={⌫:B|Ex}. By the definition of substitution [V/x]y=V So, Vis a variable of basic type and we have 1(V)=⌧00. By Lemma (4.4.3) 1;[V/x]2(y)=⌧00 The following derivation is valid Var-B 1;[V/x]2(y)=⌧00 ⌧00 :: B 1;[V/x]2`\V:{⌫:B|⌫=V} Given that V=[V/x]ythen we have 1;[V/x]2`\V:{⌫:B|⌫=V}⌘ 1;[V/x]2`\[V/x]y:[V/x]{⌫:B|⌫=y} which is precisely the desired conclusion. –sub-case y6=x:Forthis[V/x]y=y,so [V/x]{⌫:B|⌫=y}={⌫:B|⌫=y}
112 CHAPTER 4. LIQUID INTERSECTION TYPES By IH `\M0: So, the following derivation is valid Let `\M0:;x:`\N:⌧`\⌧ let x=M0in N: •case [Gen]: By inversion `\M: ↵62 By IH `\N: So, the following derivation is valid Gen `\N:↵62 `\[⇤↵]N:8↵. •case [Inst]: By inversion `\M:8↵. `\⌧ Shape(⌧=T By IH `\N:8↵. So, the following derivation is valid Inst `\N:8↵.`\⌧Shape(⌧)=T `\[T]N:[⌧/↵] Theorem 4.4.2 (Over approximation) If `\ QM:then `\M:. Proof. The proof follows by straightforward induction on the typing derivation. At each case the key observation is that each Liquid Intersection Type is also a Dependent Intersection Type and for each rule in the decidable system there is a matching rule in the undecidable side. For the case of [-Base]weuseDefinition1. Combining Theorems 4.4.1 and 4.4.2 guarantees that at run-time, for every well-typed term, taking an evaluation step preserves types.
Chapter 5 Type Inference We present in this chapter an algorithm for inferring Liquid Intersection Types, shown in Figure 5.1. Before executing this algorithm we bind every sub expression using the let-in constructor. This transformation is closely related with A-Normal Forms [FSDF93] and is performed to force types of intermediate expressions to be pushed into the typing context, so they can be used at the moment of application. The algorithm we propose is built upon three main phases: (i) we use the ML inference engine to get appropriate types, serving as type shapes for Liquid Intersection Types; (ii) for some particular sub-terms a set of constraints is generated, ensuring the well-formedness of types and that subtyping relations hold, in order to infer sound types; (iii) taking qualifiers from Qwe solve the generated constraints on-the-fly,muchlikeinclassical inference algorithms. 5.1 Using Damas-Milner type inference One key aspect of our inference algorithm is the use of the inference algorithm W [DM82] to infer ML types. Given the fact that a Liquid Intersection Type for a term is a refinement and intersections of the corresponding ML type, the types inferred by Wact as shapes for our Liquid Intersection Types. Indeed, the function Shape(·) (figuring in the typing rules and in the inference algorithm) maps a Liquid Intersection Type to its corresponding ML type. For example, Shape((x:{⌫=0}!{⌫=0})\(x: {⌫0}!{⌫0})) = int !int. In the inference algorithm, whenever Wis called, we need to feed it with an environment containing exclusively ML types. This is done by lifting Shape(·)to environ113
114 CHAPTER 5. TYPE INFERENCE Infer(,x,Q)=ifW(Shape(),x)=Bthen {v:B|v=x} else (x) Infer(,c,Q)=ty(c) Infer(,x.M,Q)=let (x:ˆ⌧1!ˆ⌧0 1)\...\(x:ˆ⌧n!ˆ⌧0 n)= Fresh(W(Shape(),x.M),Q)in let ⌧00 i=Infer(;x:ˆ⌧i,M,Q)in let A=T(x:ˆ⌧j!ˆ⌧0 j)|`\(x:ˆ⌧1!ˆ⌧0 1)\...\(x:ˆ⌧n!ˆ⌧0 n) in T(x:ˆ⌧k!ˆ⌧0 k)|x:ˆ⌧k!ˆ⌧0 k2A,;x:ˆ⌧k`\ Q⌧00 kˆ⌧0 k Infer(,MN,Q)=let (x:⌧1!⌧0 1)\...\(x:⌧n!⌧0 n)=Infer(,M,Q)in let ⌧=Infer(,N,Q)in T[N/x]⌧0 i|`\ Q⌧⌧i Infer(,let x=Min N,Q)=let ˆ⌧=Fresh(W(Shape(),let x=Min N),Q)in let ⌧1=Infer(,M,Q)in let ⌧2=Infer(;x:⌧1,N,Q)in let A=T{ˆ⌧0 i|`\ˆ⌧}in Tˆ⌧00 |ˆ⌧00 2A,;x:⌧1`\ Q⌧2ˆ⌧00 Infer(,[⇤↵]M,Q)=let =Infer(,M,Q)in 8↵. Infer(,[T]M,Q)=let ⌧0=Fresh(T,Q)in let 8↵.=Infer(,M,Q)in let A=T{⌧0 i|`\⌧0}in [A/↵] Figure 5.1: Type inference algorithm ments, Shape(),byapplyingittoeverybindingin. The function Fresh(·,·)takes an ML type and the set Qas input and generates anewLiquidIntersectionTypethatcontainsallofthecombinationsofrefinement expressions from Q. Taking for instance the ML type T=x:int !int (we assume we can annotate types with the corresponding abstraction variable, so it is easier to use with refinements) and Q={⌫0,⌫0},Fresh(T,Q)would generate the Liquid Intersection Type (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})
5.2. CONSTRAINT GENERATION 115 5.2 Constraint generation The constraints generated during inference serve as a means to ensure that the subtyping and well-formedness requirements are respected. In the presentation of the algorithm we borrow the notations from the typing rules, with `\standing for a well-formedness restriction over and `\0constraining type to be a subtype of 0. The well-formedness constraints are generated for terms where a fresh Liquid Intersection Type is generated (-abstractions, let-bindings and type application). For a fresh generated Liquid Intersection Type, solving this kind of constraints will result in a type where the free variables of every refinement are in scope of the corresponding expression. The second class of constraints are the subtyping constraints, capturing relations between two Liquid Intersection Types. A constraint `\0is valid if the type 0is a super-type of ,meaningthatthereisatypederivationusingthesubsumption rule to relate the two types. The well-formedness and subtyping rules (Figure 4.3) can be used to simplify constraints prior to their solving. For instance, the constraint `\⌧1\...\⌧ncan be simplified to the set {`\⌧1,...,`\⌧n}.Ontheotherhand,theconstraint `\(x:⌧1!⌧2)(x:⌧0 1!⌧0 2)can be further reduced to `\⌧0 1⌧1and ;x:⌧0 1`\⌧2⌧0 2. 5.3 Constraint solving We now describe the process of solving the collected constraints throughout the inference algorithm. This process will reduce to two different validity tests: a wellformedness constraint will, ultimately, reduce to the constraint of the form `\ {⌫:B|E}and so it will amount to check if the type bool can be derived for Eunder ; for the subtyping case, the simplification of constraints will result in a series of restrictions of the form `\{⌫:B|E1}\...\{⌫:B|En}{⌫:B|E0 1}\...\ {⌫:B|E0 m},leadingtocheckifJK^JE1K^...^JEnK)JE0 1K^...^JE0 mKholds. Finally, if a constraint of the form ⌧1\...\⌧n⌧0 1\...\⌧1\...\⌧n\...\⌧0 mis generated, we use the rule [-Elim]totrytosolveit. Whenever well-formedness constraints are generated, these are solved before the sub-
116 CHAPTER 5. TYPE INFERENCE typing ones. This step ensures only well-formed types are involved in subtyping relations. Well-formedness constraints arise when a fresh Liquid Intersection Type is generated, since that is when refinement expressions are plugged into a type. Such fresh types will be of the form 1\...\n,sothesolutionforaconstraintoftheform `\⌧1\...\⌧nis the type T{⌧i},theintersectionofall⌧i(with 1in)such that `\⌧i.Weassignthissolutiontoatemporary type, denoted by A, which will be used during the solving of subtyping constraints. The subtyping constraints will ensure that inferred types only present refinement expressions capturing the functional behavior of terms. These will be used with - abstractions, applications and let-bindings. Except for applications, subtyping constraints are preceded by the resolution of well-formedness restrictions, and so it is the case that subtyping relations will be checked using the temporary type A. For the case of -abstractions, after generating the fresh Liquid Intersection Type (x: ˆ⌧1!ˆ⌧0 1)\...\(x:ˆ⌧n!ˆ⌧0 n),aseriesofcallstoInfer are triggered, which we present via the syntax let ⌧00 i=Infer(;x:ˆ⌧i,M,Q), with 1in. These calls differ only on the type ˆ⌧iof xpushed into the environment, implying that different types for Mcan be inferred. After solving the well-formedness constraints, we must remove from type Athe refinement expressions that would cause the type to be unsound. We use the notation x:⌧k!⌧0 k2Ato indicate that T{x:⌧k!⌧0 k}should be a supertype of A,inthesensethatitcanbeobtainedfromAusing exclusively the rule [-Elim] (taking an analogy with set theory, T{x:⌧k!⌧0 k}would be a sub set of the intersections of A). Then, the inferred type will be T{x:ˆ⌧k!ˆ⌧0 k},suchthat (x:ˆ⌧k!ˆ⌧0 k)2Aand the constraint ;x:ˆ⌧k`\⌧00 kˆ⌧0 kis valid, that is, the type inferred for Munder the environment ;x:ˆ⌧kis a subtype of ˆ⌧0 k.Asanexample, consider Q={⌫0,⌫0,y=5},thetermx. xand =;. The inference procedure will start by generating the type: (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{y=5})\ (x:{⌫0}!{y=5})\ (x:{y=5}!{⌫0})\ (x:{y=5}!{⌫0})\ (x:{y=5}!{y=5})
5.3. CONSTRAINT SOLVING 117 Then, with well-formedness constraints, and since no variable yis in scope, we are left with: (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0}) Finally, because of subtyping relations, the inferred type will be: (x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0}) For application and let-bindings, solving subtyping constraints works in a similar manner as for -abstractions. The type of an application is inferred similarly as in [FP91]: for the function Mwith type x:⌧1!⌧0 1\...\⌧n!⌧0 nand the argument Nwith type ⌧,thetypeofMN is T{⌧0 i},suchthat1inand `\⌧⌧iis checked valid. We give now a complete example of how our algorithm behaves, considering type inference for (x.x ⇤x).WithQ={⌫0,⌫0},ouralgorithmstartsbygenerating the correspondent Liquid Intersection Type for x:int !int: Fresh(x:int !int,Q)=(x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0})\ (x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0}) Then, a series of recursive calls (differing in the type assigned to xwithin the typing context) are performed. We use 1=x:{⌫0}and 2=x:{⌫0},andusethe predicate Valid(·)to represent the process of solving subtyping constraints: Infer(1,x⇤x, Q)={⌫=x⇤x} Infer(1,⇤x, Q)=z:int !{⌫=x⇤z} Infer(1,⇤,Q)=w:int !z:int !{⌫=w⇤z} Infer(1,x,Q)={⌫=x} Valid(x0^⌫=x)>)? Yes Infer(1,x,Q)={⌫=x} Valid(x0^⌫=x)>)? Yes Infer(1,x⇤x, Q)={⌫=x⇤x}
118 CHAPTER 5. TYPE INFERENCE Infer(2,x⇤x, Q)={⌫=x⇤x} Infer(2,⇤x, Q)=z:int !{⌫=x⇤z} Infer(2,⇤,Q)=w:int !z:int !{⌫=w⇤z} Infer(2,x,Q)={⌫=x} Valid(x0^⌫=x)>)? Yes Infer(2,x,Q)={⌫=x} Valid(x0^⌫=x)>)? Yes Infer(2,x⇤x, Q)={⌫=x⇤x} Valid(x0^⌫=x⇤x)⌫0)? Yes Valid(x0^⌫=x⇤x)⌫0)? No Valid(x0^⌫=x⇤x)⌫0)? Yes Valid(x0^⌫=x⇤x)⌫0)? No Given the validity results of the last four constraints, the Liquid Intersection Type inferred for (x.x ⇤x)is (x:{⌫0}!{⌫0})\(x:{⌫0}!{⌫0}) 5.4 Properties of inference We were able to prove that our inference algorithm is sound with respected to the typing rules. This property is formalized as follows: Theorem 5.4.1 (Soundness) If Infer(,M,Q)=then `\ QM:. Proof. By structural induction over M. •case M⌘x: –subcase in which Mhas a basic type in this case W(Shape(),x)=B and so xhas type {⌫:B|1}\...\{⌫:B|n}, which we abbreviate to ⌧1\···\⌧n. The following derivation is then valid (x)=⌧1\···\⌧n⌧i:: B(8i.1in) `\ Qx:{⌫:B|⌫=x}B-Var
5.4. PROPERTIES OF INFERENCE 119 –subcase in which xhas not a basic type: in this case =(x). So, the following derivation is valid (x)=(x)::T `\ Qx:Var •Case M⌘c: Easy, by application of the rule [Const]. •Case M⌘x.N:Inthiscasethealgorithmcomputes –(x:ˆ⌧1!ˆ⌧0 1)\...\(x:ˆ⌧n!ˆ⌧0 n)=Fresh(W(Shape(),x.M),Q) By IH ;x:ˆ⌧i`\ QN:⌧00 i,8i:1in(a) The type Arestricts the inferred type only to the well formed intersections: `\(x:ˆ⌧1!ˆ⌧0 1)\...\(x:ˆ⌧n!ˆ⌧0 n)reduces to: {`\(x:ˆ⌧1!ˆ⌧0 1),...,`\(x:ˆ⌧n!ˆ⌧0 n)} Consider the sub-set of derivations in (a) such that ;x:ˆ⌧j`\ Q⌧00 jˆ⌧0 jand that respect the type A. We have then a set of derivations of the form Abs Sub ;x:ˆ⌧j`\ QN:⌧00 j;x:ˆ⌧j`\ Q⌧00 jˆ⌧0 j;x:ˆ⌧j`\ˆ⌧0 j ;x:ˆ⌧0 j`\ QN:ˆ⌧0 j`\x:ˆ⌧j!ˆ⌧0 j `\ Qx.N :(x:ˆ⌧j!ˆ⌧0 j) By repeated application of the rule [Intersect] Intersect `\ Qx.N :(x:ˆ⌧j!ˆ⌧0 j)... `\ Qx.N :(x:ˆ⌧j+k!ˆ⌧0 j+k) `\ Qx.N :(x:ˆ⌧j!ˆ⌧0 j)\...\(x:ˆ⌧j+k!ˆ⌧0 j+k) •case M⌘M0N:ByIH –`\ QM0:(x:⌧1!⌧0 1)\...\(x:⌧n!⌧0 n) –`\ QN:⌧
120 CHAPTER 5. TYPE INFERENCE For all the ⌧isuch that ⌧⌧iwe have a derivation of the form Sub `\ QM0:(x:⌧1!⌧0 1)\...\(x:⌧n!⌧0 n) `\ Q(x:⌧1!⌧0 1)\...\(x:⌧n!⌧0 n)(x:⌧i!⌧0 i)`(x:⌧i!⌧0 i) `\ QM0:(x:⌧i!⌧0 i)D `\ QM0N:⌧0 i[N/x] App in which Dis `\ QN:⌧`\ Q⌧⌧i`\⌧i `\ QN:⌧i Sub Let D1be the entire previous derivation. For each ⌧ithat satisfy ⌧⌧iwe have a derivation of the previous form. So, by repeated application of the rule [Intersect] the following derivation is valid Di... Di+j `\ QM0N:⌧0 i[N/x]\...\⌧0 i+j[N/x]Intersect By the definition of substitution we have ⌧0 i[N/x]\...\⌧0 i+j[N/x]=(⌧0 i\...\ ⌧0 i+j)[N/x], which is precisely the inferred type. •case M⌘let x=M0in N: is of the form ˆ⌧00 1\...\ˆ⌧00 n. By IH –`\ QM0:⌧1 –;x:⌧1`\ QN:⌧2 The type Astands for the set of ˆ⌧0 isuch that `\ˆ⌧0 i, which by the definition of well formed type we have WF-Intersect `\ˆ⌧0 i... `\ˆ⌧0 i+j `\ˆ⌧0 i\...\ˆ⌧0 i+j(b) Consider all ˆ⌧00 iin Asuch that ;x:⌧1`\ Q⌧2ˆ⌧00 i. The following derivation is valid Let D Intersect Sub ;x:⌧1`\ QN:⌧2;x:⌧1`\ Q⌧2ˆ⌧00 i ;x:⌧1`\ QN:ˆ⌧00 i... ;x:⌧1`\ QN:ˆ⌧00 i+j ;x:⌧1`\ QN:ˆ⌧00 i\...\ˆ⌧00 i+j ... `\ Qˆ⌧00 i\...\ˆ⌧00 i+j (c) `\ Qlet x=M0in N:ˆ⌧00 i\...\ˆ⌧00 i+j
5.5. THE LISETTE TOOL 121 in which Dis `\ QM0:⌧1 The derivation (c) is valid by (b), since 00 i\...\00 i+jis a sub-type of 0 i\...\0 i+j. •case M⌘[⇤↵]M0: By IH `\ QM0: The following derivation is valid `\ QM0:↵62 `\ QM0:8↵.Gen •case M⌘[⌧]M0: By IH `\ QM0:8↵. Since ⌧0=Fresh(T,Q),thenT=Shape(⌧0). ⌧0is of the form ⌧0 1\...\⌧0 n. The type Astands for the set of all ⌧0 isuch that `\⌧0 i,soitisasub-typeof ⌧0 1\...\⌧0 n. Then, the following derivation is valid Inst `\ QM0:8↵. Intersect `\⌧0 i... `\⌧0 i+j `\⌧0 i\...\⌧0 i+jShape(⌧0 i\...\⌧0 i+j)=T `\ Q[⌧]M0:[⌧0 i\...\⌧0 i+j/↵] 5.5 The lisette tool In order to automate all the proof-and-typing process required for Liquid Intersection Types inference, we implemented a prototype tool which we baptized lisette (LIquid interSEction TypEs)1.Agraphicalrepresentationfortheworkflowofthistoolisgiven in Figure 5.2. 1http://www.dcc.fc.up.pt/~mariopereira/lisette.tar.gz
Chapter 6 Conclusions and future work Refinement type systems are a family of type systems presenting features suitable for the functional specification of programs, directly on type language. In refinement type systems logical annotations are plugged into types, which can easily lead to undecidable problems. The Liquid Types system overcomes the undecidable issues of general refinement types by restricting the expressions appearing on refinement predicates and by using a conservative subtyping mechanism. We presented a new type system supporting functional descriptions, via refinement types, and offering the expressiveness of intersection types. We keep our system decidable but enhance the expressive power of our type language, having more accurate types being checked by our system. So, this type system can be used to assign programs more precise types than in previous refinement type systems, with types themselves serving as detailed descriptions of programs’ behavior. To design a decidable system we adopted a style closely related to Liquid Types: the refinement expressions presented in types of some terms are exclusively collected from Q,aglobalsetoflogicalqualifiers,andthesubtypingisdecidable. Wealsoimpose that the type of some particular terms must be the intersection of refinements to its ML type, intersecting only types of the same form. We also proposed an inference algorithm for Liquid Intersection Types. This algorithm takes as input an environment ,atermMand the set of qualifiers Q,producinga correspondent Liquid Intersection Type. Our inference algorithm uses the Walgorithm to infer the shape of a Liquid Intersection Type, which is the ML type for that term. To determine which refinement expressions can be plugged into a type, the algorithm produces a series of well-formedness and subtyping constraints, solving them 129
130 CHAPTER 6. CONCLUSIONS AND FUTURE WORK immediately after their generation. We have been able to prove that our algorithm is sound with the respected to the conceived typing rules. The tool lisette represents a practical prototype for the work conceived during the thesis. This tool can be used to experimentally verify the relevance of using intersection types discipline together with functional specification provided by refinement types. 6.1 Future work From this work, we propose some main directions for future work: •We are convinced that our system has the principal type property and that our algorithm infers the most general type for the given program. We intend to formalize and proof this result, considering the work presented in [Fre94] a good starting point to achieve this goal. •In this thesis we followed the road of borrowing the expressiveness and accuracy of intersection types into refinement type systems. Also interesting is to follow the opposite path: we plan on studying on how to extend decidable intersection type systems (of finite ranks) [Jim95, KW99] with type refinement predicates. •It is of much interest to use lisette to infer Liquid Intersection Types for more realistic examples. We plan on preparing a set of representative benchmarks, not only to test the tool, but also to stress out our type system and inference. 6.2 Final remarks Ultimately, we believe the objectives we set for ourselves were fulfilled. We believe our type system represents an interesting means for assigning very expressive and accurate types for programs, and we think it can be of much use when designing a realistic compiler for a programming language with a rich type system. The planned future work will not only allow to study theoretically and practically the completeness of Liquid Intersection Types approach, but also to extend our results and concepts to other interesting type systems. On the personal level, the development of this work contributed for gaining a deeper understanding of type systems and type theory research processes. This thesis also served to get better in touch on how to perform formal research work.
Bibliography [Bar84] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics, Revised second edition.North-Holland,1984. [BCC+08] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed. Iguernelada, Stéphane Lescuyer, and Alain Mebsout. The alt-ergo automated theorem prover, 2008. http://alt-ergo.lri.fr. [BCDC83] Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The journal of symbolic logic, 48(4):931–940, 1983. [BT07] Clark Barrett and Cesare Tinelli. CVC3. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification,volume4590ofLecture Notes in Computer Science,pages298–302.SpringerBerlinHeidelberg, 2007. [Car88] L. Cardelli. Typechecking dependent types and subtypes. In Lecture Notes in Computer Science on Foundations of Logic and Functional Programming, pages 45–57, New York, NY, USA, 1988. Springer-Verlag New York, Inc. [CDC80] M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the -calculus. Notre Dame Journal of Formal Logic, 21(4):685–693, 10 1980. [Chu33] A. Church. A set of postulates for the foundation of logic. Annals of Mathematics, 34(2):839–864, 1933. [Cur34] H. B. Curry. Functionality in Combinatory Logic. In Proceedings of the National Academy of Sciences of the United States of America,volume20, pages 584–590, November 1934. 131
132 BIBLIOGRAPHY [Dam84] Luís Damas. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1984. [DM82] Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’82, pages 207–212, Albuquerque, New Mexico, 1982. ACM. [Fil13] Jean-Christophe Filliâtre. One logic to use them all. In 24th International Conference on Automated Deduction (CADE-24),volume7898ofLecture Notes in Artificial Intelligence, pages 1–20, Lake Placid, USA, June 2013. Springer. [Fla06] Cormac Flanagan. Hybrid type checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’06, pages 245–256, Charleston, South Carolina, USA, 2006. ACM. [FP91] Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, PLDI ’91, pages 268–277, Toronto, Ontario, Canada, 1991. ACM. [FP13] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 — where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Proceedings of the 22nd European Symposium on Programming,volume 7792 of Lecture Notes in Computer Science, pages 125–128. Springer, March 2013. [Fre94] Tim Freeman. Refinement Types for ML. PhD thesis, School of Computer Science, Carnegie Mellon University, 1994. [FSDF93] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, pages 237–247, Albuquerque, New Mexico, USA, 1993. ACM. [Gir72] Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, PhD thesis, Universit e Paris VII, 1972.
BIBLIOGRAPHY 133 [Hin69] R. Hindley. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society, 146:29–60, 1969. [Jim95] Trevor Jim. Rank 2 type systems and recursive definitions. Massachusetts Institute of Technology, Cambridge, MA, 1995. [KF10] Kenneth Knowles and Cormac Flanagan. Hybrid type checking. ACM Trans. Program. Lang. Syst.,32(2):6:1–6:34,February2010. [KW99] A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Proceedings of the 26th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’99, pages 161–174, San Antonio, Texas, USA, 1999. ACM. [Mil78] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978. [Nel80] Charles Gregory Nelson. Techniques for Program Verification. PhD thesis, Stanford, CA, USA, 1980. AAI8011683. [NN99] Flemming Nielson and HanneRiis Nielson. Type and effect systems. In Ernst-Rüdiger Olderog and Bernhard Steffen, editors, Correct System Design,volume1710ofLecture Notes in Computer Science,pages114– 136. Springer Berlin Heidelberg, 1999. [OT12] C.-H. Luke Ong and Takeshi Tsukada. Two-level game semantics, intersection types, and recursion schemes. In Proceedings of the 39th International Colloquium Conference on Automata, Languages, and Programming - Volume Part II, ICALP’12, pages 325–336, Warwick, UK, 2012. SpringerVerlag. [PAF14a] Mário Pereira, Sandra Alves, and Mário Florido. Liquid Intersection Types. In 7th Workshop on Intersection Types and Related Systems,Vienna, Austria, 2014. [PAF14b] Mário Pereira, Sandra Alves, and Mário Florido. Liquid Types Revisited. In The 20th TYPES Meeting,Paris,France,2014. [Rey74] John C. Reynolds. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque Sur La Programmation, pages 408–423, London, UK, UK, 1974. Springer-Verlag.
134 BIBLIOGRAPHY [RKJ08] Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. Liquid types. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’08, pages 159–169, Tucson, AZ, USA, 2008. ACM. [Rob65] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23–41, January 1965. [Sho84] Robert E. Shostak. Deciding combinations of theories. J. ACM,31(1):1–12, January 1984. [vB93] S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Department of Computer Science, University of Nijmegen, 1993. [VRJ13] Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. Abstract refinement types. In Proceedings of the 22Nd European Conference on Programming Languages and Systems, ESOP’13, pages 209–228, Rome, Italy, 2013. Springer-Verlag. [Wad90] Philip Wadler. Linear types can change the world! In PROGRAMMING CONCEPTS AND METHODS.North,1990. [WF92] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115:38–94, 1992.
Appendix A lisette code A.1 A-normalization Code for performing A-normalization over terms. (*************************************************************** *a_normalizing(tm) *tm-tiny-MLterm ***************************************************************) let rec a_normalizing = function |TmCons_asc->c |TmAbs(c,t) ->TmAbs(c,a_normalizingt) |TmVar_asx ->x |TmApp(t1,t2)ast-> begin match t2 with |TmCons_ |TmVar_->t |_->ref_a:=succ!ref_a; let x = char_of_int ((!ref_a - 1) + 97) in TmLet (x, a_normalizing t2, TmApp (t1, TmVar x)) end |TmLet(c,t1,t2)->TmLet(c,t1,a_normalizingt2) 135
136 APPENDIX A. LISETTE CODE A.2 Type inference A.2.1 Inference algorithm Implementation of inference algorithm, Figure 5.1. module OrdTys = struct type t = ty let compare t1 t2 = if (=) t1 t2 then 0 else -1 end;; (*OCaml sets are used in order to efficiently represent intersection types*) module SetTys = Set.Make(OrdTys);; (*************************************************************** *fresh(dm_ty) *dm_ty-typeinferredwithDamas-Milneralgorithm ***************************************************************) let fresh dm_ty = let n = ref 0 in let rec put_refs refs = function |DMBool ->incrn;TyBasicRefined(TyBool,RefBasic(List.nth refs (!n - 1))) |DMInt ->incrn;TyBasicRefined(TyInt,RefBasic(List.nth refs (!n - 1))) |DMVar(i) ->TyBasic(TyVar(i)) |DMArrow(c,t1,t2)->TyArrow(c,(put_refsrefst1),(put_refsrefs t2)) in List.fold_left (fun acc e -> SetTys.union acc (SetTys.singleton (n := 0; put_refs e dm_ty))) (SetTys.empty)
A.2. TYPE INFERENCE 137 (*************************************************************** *infer(gamma,term,refs_q) *gamma-typingcontext,term-tiny-MLterm *refs_q-listoflogicalqualifiers ***************************************************************) let rec infer gamma term refs_q = match term with |TmVar(c)asx-> let _, dm_type = damas_milner_w (shape_gamma gamma) x in begin match dm_type with |DMInt->SetTys.singleton(TyBasicRefined(TyInt,(RefBasic(QEq (QNuVar, QVar (c)))))) |DMBool->SetTys.singleton(TyBasicRefined(TyBool,(RefBasic( QEq (QNuVar, QVar (c)))))) |DMVar(_)|DMArrow(_,_,_)->SetTys.singleton(List.assocc gamma) end |TmCons(c)-> begin try SetTys.singleton (List.assoc c cons_ty_list ) with Not_found -> SetTys.singleton (TyBasic (TyInt)) end |TmAbs(c_l,m’)asm-> let _, dm_type = damas_milner_w (shape_gamma gamma) m in let fresh_type = fresh dm_type (list_of_refinements (ty_length dm_type) refs_q) in let a_type = SetTys.fold (fun e acc -> let a = decide_wf_constraint gamma e in if a then SetTys.add e acc else acc )fresh_typeSetTys.emptyin let infer_rec_l = SetTys.fold (funeacc-> begin match e with |TyArrow(c,t,t’)-> begin try let ty_rec = List.assoc (Call ((gamma@[(c, t)]), m’, refs_q )) !list_calls_mem in acc@[ty_rec] with Not_found ->
144 APPENDIX A. LISETTE CODE begin match r with |RefBasic(q) ->lete=replace_nu_varxqin logic_of_quals e |RefCon(q,q’)->lete=replace_nu_varxqin let e’ = replace_nu_var x q’ in LAnd (logic_of_quals e, logic_of_quals e’) |RefTrue ->LAtom(LTrue) end |TyIntersection(t,t’)->lete=embbed_typextin let e’ = embbed_type x t’ in LAnd (e, e’) |_->LAtom(LTrue) in let f acc (x, t) = let e_ty = embbed_type x t in LAnd (acc, e_ty) in List.fold_left f (LAtom (LTrue)) gamma let config = Whyconf.read_config None (*get configuration file*) let main = Whyconf.get_main config (*read config file main section*) let provers = Whyconf.get_provers config (*get installed provers*) (*creating environment, so that each SMT driver can be used*) let env = Env.create_env (Whyconf.loadpath main) let int_theory = Env.find_theory env ["int"] "Int" (*integers theory*) (*************************************************************** *logic_of_constraints(cons) *cons-constrainttobetranslatedintoWhy3language ***************************************************************) let logic_of_constraints = function |SubType(l,t,t’)->letl’=transform_gammalin let gamma_l = gamma_embedding l’ in let l_t = logic_of_type t in let l_t’ = logic_of_type t’ in LImpl (LAnd (gamma_l, l_t), l_t’) |_ ->assertfalse (*************************************************************** *why_term_from_logic(l_term,list) *w_term-Why3term,list-listofalreadyfoundvariables
A.3. INTERACTION WITH WHY3 145 ***************************************************************) let rec why_term_from_logic l_term list= match l_term with |LAnd(d,d’)->letw_d,l=(why_term_from_logicdlist)in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_and w_d w_d’), l’ |LOr(d,d’)->letw_d,l=(why_term_from_logicdlist)in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_or w_d w_d’), l’ |LImpl(d,d’)->letw_d,l=(why_term_from_logicdlist)in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_implies w_d w_d’), l’ |LNeg(d)->letw_d,l=(why_term_from_logicdlist)in (Term.t_not w_d), l |LGt(d,d’)->letgt_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix >"] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.ps_app gt_symbol [(w_d); (w_d’)]), l’ |LLt(d,d’)->letlt_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix <"] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.ps_app lt_symbol [(w_d); (w_d’)]), l’ |LGe(d,d’)->letge_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix >="] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.ps_app ge_symbol [(w_d); (w_d’)]), l’ |LLe(d,d’)->letle_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix <="] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.ps_app le_symbol [(w_d); (w_d’)]), l’ |LEq(d,d’)->leteq_symbol:Term.lsymbol=
146 APPENDIX A. LISETTE CODE Theory.ns_find_ls int_theory.Theory.th_export ["infix ="] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in Term.ps_app eq_symbol [(w_d); (w_d’)], l’ |LArith(ar)->why_term_from_aritharlist |LAtom(a) ->why_term_from_atomalist and why_term_from_arith ar_term list= match ar_term with |LPlus(d,d’)->letplus_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix + "] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_app_infer plus_symbol [(w_d); (w_d’)]), l’ |LMinus(d,d’)->letminus_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix - "] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_app_infer minus_symbol [(w_d); (w_d’)]), l’ |LTimes(d,d’)->letmult_symbol:Term.lsymbol= Theory.ns_find_ls int_theory.Theory.th_export ["infix * "] in let w_d, l = (why_term_from_logic d list) in let w_d’, l’ = (why_term_from_logic d’ l) in (Term.t_app_infer mult_symbol [(w_d); (w_d’)]), l’ |_ ->assertfalse; and why_term_from_atom a_term list = match a_term with |LTrue ->Term.t_true,list |LNuVar ->begintry let var_nu = List.assoc "nuVar" !list_vars in let nu = (Term.t_var var_nu) in nu, if (List.mem_assoc "nuVar" list) then list else ("nuVar", var_nu)::list with Not_found ->
A.3. INTERACTION WITH WHY3 147 let var_nu = Term.create_vsymbol (Ident.id_fresh " nuVar") Ty.ty_int in let nu = (Term.t_var var_nu) in list_vars := ("nuVar", var_nu)::!list_vars; nu, ("nuVar", var_nu)::list end |LVar(c) ->begintry let var_x = List.assoc (Char.escaped c) !list_vars in let x = (Term.t_var var_x) in x, if (List.mem_assoc (Char.escaped c) list) then list else (Char.escaped c, var_x)::list with Not_found -> let var_x = Term.create_vsymbol (Ident.id_fresh (Char .escaped c)) Ty.ty_int in let x = (Term.t_var var_x) in list_vars := (Char.escaped c, var_x)::!list_vars; x, (Char.escaped c, var_x)::list end |LVal(i) ->Term.t_const(Number.ConstInt(Number.int_const_dec( string_of_int i))), list (*************************************************************** *close_forall_why_term(w_term) *w_term-Why3term ***************************************************************) let rec close_forall_why_term w_term = List.fold_left (fun acc (_, var_x) -> Term.t_forall_close [var_x] [] acc) w_term (*************************************************************** *get_answer_of_constraint(cons) *cons-subtypingconstraint ***************************************************************) let get_answer_of_constraint cons = let l_term = logic_of_constraints cons in let w_t, l = why_term_from_logic l_term [] in let gen = close_forall_why_term w_t l in let my_theory = Theory.create_theory (Ident.id_fresh "My_theory") in let use th1 th2 = let name = th2.Theory.th_name in Theory.close_namespace
148 APPENDIX A. LISETTE CODE (Theory.use_export (Theory.open_namespace th1 name.Ident.id_string) th2) true in let my_theory = use my_theory int_theory in let my_goal_id = Decl.create_prsymbol (Ident.id_fresh "my_goal") in let decl_goal = Decl.create_prop_decl Decl.Pgoal my_goal_id gen in let my_theory = Theory.add_decl my_theory decl_goal in let my_theory = Theory.close_theory my_theory in let my_tasks = List.rev (Task.split_theory my_theory None None) in let provers = Whyconf.get_provers config in let provers = Whyconf.Mprover.bindings provers in let get_provers_name (p: Whyconf.config_prover) = p.prover.prover_name in let bool_of_answer = function |Call_provers.Valid->true |_->falsein let print_prover_answer prover (result: Call_provers.prover_result) = let answer = match result.pr_answer with |Call_provers.Valid->"checked" |_->"notchecked"in let p_name = get_provers_name prover in let time = result.pr_time in printf "@[%s checks valid?@ %s in %5.2f seconds@]@." p_name answer time in let rec pre_stop_iter f l p = match l with |[] ->() |e::l’->fe;ifpethen()elsepre_stop_iterfl’pin let rec pre_stop_fold_left f l p = match l with |[] ->false |e::l’->fe;ifpethentrueelsepre_stop_fold_leftfl’pin List.map (*this fold_left goes through all the tasks*) (*this iter goes through all the provers, possibly stopping before if some prover is able to discharge the implication*) (fun t -> pre_stop_fold_left (fun _ -> printf "@[Task is: %a@]@." Pretty.print_task t) provers (fun (k, p) -> try let driver : Driver.driver = Driver.load_driver env p.Whyconf.driver [] in
A.3. INTERACTION WITH WHY3 149 let result = Call_provers.wait_on_call ( Driver.prove_task ~command:p.Whyconf.command driver t ()) () in print_prover_answer p result; bool_of_answer result. pr_answer with e -> eprintf "Failed to load driver: %a@." Exn_printer. exn_printer e; false); ) my_tasks