# Lets's talk FP one more time
18:30 - Coming together
19:00 - Simply Typed Lambda Calculus by Sven
19:45 - Category Theory in Action by Paul
## From Untyped to Simply Typed Lambda Calculus
speaker: Sven Tennie
categories: programming language theory
The Simply Typed Lambda Calculus adds function types (e.g. not:: Bool -> Bool) to the Untyped Lambda Calculus. It is the simplest example of a typed lambda calculus and can be used as a foundation for functional programming languages with simple type systems (i.e. without polymorphism, higher kinded types, dependent types...) You can also consider it as the next easy learning step into understanding more complex type systems.
Following the motto: "... there is nothing so practical as a good theory!" we'll combine theory and practice by writing an interpreter and a type checker, guided by their theoretical counterparts. These are Evaluation Rules for the interpreter and Typing Rules for the type checker.
To understand evaluation and typing rules we'll learn how to read Inference Rules in general. You can find this notation in many papers about type systems and operational semantics - so it's definitely worth learning.
Of course, we'll start with a quick recap/introduction to the Untyped Lambda Calculus.
Code examples will be in Haskell, but I promise to keep them as simple as possible - No fancy stuff... ;)
## Category Theory in Action
Let's have a small live-coding session where we try to take the basic concepts of Category Theory and bake them into code. We will:
- define what a Category is
- how to translate that into code
- what we can derive from that structure, like Monoids, Functors etc..
And let us all hope the compiler is with us and we don't get stuck on compilation errors for hours on end :).
You don't have to bring a notebook, but you can if you want.