Intro to functional programming
Welcome to the Lambda Shell! This interactive tutorial will teach you the basics of programming in a purely functional environment. Specifically, we will be using a variation of typed lambda calculus called System F. As we go along, we will use a web shell that runs our programs for us.
First order Functions
The most important concept of functional programming is that of the function. Unlike other languages, in System F (and all lambda calculi), functions are a foundational construct. All functions in System F follow the same format. They take as an argument a single expression e, and output a single expression v. Consider the following program. In it, the argument is stored in a variable called x, and the output of the function is x itself. The notation may be a bit strange at first, but it is as simple as lambda <variable name> . <expression using that variable>. Try running the program below.
lambda x.x
Oh no, it didn't work! Why is that? Well in order for System F to compile and run this code, it needs to know what the type of its arguments and return values are. A type is a bit like metadata of the expression. In the same way that you might say this file is a PDF, you want to say that this variable is an integer.
But this is a bit confusing right now, because the only expressions we've seen are variables which can have any types, and functions whose type depends on those variables. How do we get a type in the first place! What we would like is to say that the previous function takes any argument x, and then returns it. Phrased differently, the for every type α, the function takes in an α and returns an α.
Fortunately, System F lets us do this! We can define a type function LAMBDA whose argument is a type. That type can then be used by the normal function inside of it. Let's see what that looks like
LAMBDA a.
lambda x:a.x
What do you expect the type of this expression to be? Try to figure it out before running the code.
Was the result what you were expecting? Effectively this statement is the function that can take any input, and return that same output, regardless of the type. We call this the identity function. Next we will figure out how to call that function.