Type Independent Features on Lambda Calculus

Syntactic sugar represents a process of including new features to a language without actually implementing a new structure. It extends the previ- ously built structure and includes functionality based on the easiness of the users. Python possesses a sheer number of such examples. In this study, we chose five different such features, Enumerator, Packing, Unpacking, Zip and Unzip. These features are all iterable features and can be implemented on top of lambda cal- culus, list, pair and basic language operations. With the addition, these features were implemented such that it can consume numerous types of input and operate on that. Also, the notion of subtyping and typed systems has been added to these features. Enumerator is a feature that provides the functionality to iterate over a different type of objects. Enumerator can be implemented on a list, tuple, string objects, etc. Packing is used where all arguments are packed into one variable and can be passed as an argument in a method without appreciating the exact number of arguments. *args and **kwargs are the most common example of packing and unpacking. Unpacking performs the opposite operation, where it turns a partic- ular variable into the original data structure. Whereas, Zip operates on multiple iterable variables with same index structure and returns a distinct iterable object. Unzip achieves the opposite where it divides a list of pair into two lists. These specific features of Python will be implemented using Lambda calculus in Coq IDE. Our result will show the functionality and behavior of these features in diverse types of operations.

Avatar
Rangeet Pan
Research Assistant

My research interests include distributed robotics, mobile computing and programmable matter.