9. System F: Introduction to Polymorphic Lambda Calculus

System F: Introduction to Polymorphic Lambda Calculus

System F, also known as the second-order lambda calculus or polymorphic lambda calculus, is an extension of the simply typed lambda calculus with support for polymorphism.

In System F, functions can be polymorphic, meaning they can operate on values of any type.

This is achieved through the introduction of type variables and type abstraction.

A key feature of System F is the universal quantification of types, allowing functions to be parameterized by types.

For example, the polymorphic identity function in System F is written as:

λA. λx:A. x

This function can take an argument of any type A and return it unchanged.

Lab Activity: Implementing System F

Let's implement a basic interpreter for System F in Python.

class Type:
    def __init__(self, name):
        self.name = name

class Term:
    def __init__(self, term):
        self.term = term

def identity(A):
    return lambda x: x

def main():
    int_identity = identity(Type("Int"))
    str_identity = identity(Type("String"))
    
    print("Identity of Int:", int_identity(42))
    print("Identity of String:", str_identity("Hello"))

if __name__ == "__main__":
    main()
  

In the lab activity, we define a `Type` class to represent types and a `Term` class to represent terms in System F.

We then implement a polymorphic identity function `identity`, which returns a function that accepts an argument of any type and returns it unchanged.

We demonstrate the implementation by creating instances of the identity function for different types and applying them to values.