QuantitativeTypeSystems-Project

This is the work developed for the Project course at DCC-FCUP in 2020

=======Getting Started=======

----Prerequisites----

-You need to have the GHC compiler installed in your machine. You can download it in https://www.haskell.org/ghc/download.html.

=======Content=======

• LambdaCalculus.hs: contains the 'data's that define lambda-terms.

• SimpleTypes.hs: simple type system; includes the unification algorithm (function unify) and type-inference algorithm (function typeInf).

• Rank2IntersectionTypes.hs: rank 2 intersection type system; includes the algorithm that transforms <=2,1-satisfaction problems into equivalent unification problems (function transformSat) and the type-inference algorithm (function r2typeInf).

• QuantRank2IntersectionTypes.hs: similar to Rank2IntersectionTypes.hs, but it features our new type-inference algorithm that extracts quantitative information (function quantR2typeInf).

• parser.y: description of the parser to be generated with Happy.

• parser.hs: parser generated by Happy.

=======How to Use It=======

In order to use the parser, first you should compile parser.hs with ghc parser.hs -o parser in the terminal and then you can execute the parser file generated by using ./parser. The parser accepts isolated lambda terms and calls to the type inference functions typeInf and quantR2typeInf applied to the lambda terms.

-- The functions allowed are ti0and qti2, which infer the type of terms, for simple types and rank 2 intersection types with quantitative information, respectively. They should be used in the following way: ti0(Term) and qti2(Term), where Term is a lambda term.

-- Regarding the format of the terms, applications correspond to 2 terms separated by a space (Term Term) and abstractions \Var.Term, where Varis a alphanumeric string and Term a lambda term. Terms can also be between parentheses, for precedence.

Some examples of input to the parser are:

• \x.\y.x y: corresponds to the term (\x.(\y.(x y)))
• \f.\x.f (f x): corresponds to the term (\f.(\x.(f (f x))))
• (\x.x) (\x.x): corresponds to the term ((\x.x) (\x.x))
• \x.x \x.x: corresponds to the term (\x.(x (\x.x)))
• ti0(\x.x): performs type-inference with simple types for the term (\x.x)
• qti2(\x.x): performs type-inference with rank 2 intersection types for the term (\x.x)