Repository files navigation

This repository is meant to be a personal collection of implementations of the concepts from the TaPL(Types and Programming Languages) book.

(There are code samples available on TAPL's website(OCaml), but I chose to implement them from scratch on Haskell)

• Example of a type system with bounded quantification

Each folder contains a parser+interpreter of a given type system. You just need to enter in the repository andcabal run tapl.

1. Untyped lambda calculus(Chapter 5, 6, 7)
2. Simply Typed Lambda Calculus(with extensions: records/tuples, variant/sum, etc.)(Chapter 9, 10, 11)
3. Simply Typed Lambda Calculus with subtyping(Chapter 15, 16)
4. Simply Typed Lambda Calculus with recursive types(Chapter 20, 21)
5. Simply Typed Lambda Calculus with type reconstruction(type inference)(Chapter 22)
6. System F(Chapter 23, 24, 25)
7. System F with subtyping(Bounded Quantification)(Chapter 26, 28)
8. System F omega(with type operators)(Chapter 29, 30)

The main type systems features covered on TaPL are:

• Types: allows you to classify the possible runtime values of terms, e.g. a variable of typeNat, can only hold a natural number at runtime(e.g. 0, 1, 5, etc.).
• Subtyping: allows you to have a more specific type than a more general one, i.e. given a typeS, which is a subtype of the typeT, all possible runtime values ofS will be within all the possible runtime values ofT, e.g.Nat(0, 1, 2, ...) is a subtype ofInteger(-2, -1, 0, 1, 2, ...). We can use this feature on functions and variables, e.g. a function that needs aInteger as an argument, can also take a variable of typeNat as an argument, becauseNat is a subtype ofInteger.
• Recursive types: allows you to represent infinite data structures, e.g. a list of something(data NatList = Nil | Cons Nat NatList), a tree of something, etc.
• Type inference: allows you to omit the type annotations on your code, the compiler will infer the type of each term, e.g.λn: succ (succ n)(instead ofλn:Nat. succ n)n will be inferred to typeNat, because the compiler knows thatn must be a natural number, since we're applying thesucc function on it, likewise withλb: if b then 0 else 2,b will be inferred toBool, with no added type annotations.
• Polymorphism(or more formally "Parametric polymorphism"): allows you to write generic functions(that operate onany type), e.g.let id=(λT. λt:T. t), where the first argument is a type argument, and the second one is a term argument, with that we can use the same function on multiple types:id Nat 0 will be evaluated to0,id Bool true will be evaluated totrue, etc.
• Higher-order polymorphism(or type operators): allows you to write generic functionson types, e.g. we can define thePair type constructor(or kind), and we can feed this type constructor with two type arguments to yield a new type, e.g.Pair Nat Bool symbolizes thetype of a pair of a natural number and a boolean value.