slides.pdfpc

[file]
slides.pdf
[duration]
35
[end_user_slide]
1
[notes]
### 1
this is not going to be a talk about Scala
not practical
still relevant 10 years from now
diverse community, some engineers, some mathematicians
type lambda, soundness, Church encoding
no time to explain, just give some background, pique interest, give pointers for your own exploration

### 2
This is going to be a basic introduction
I do not assume any prior computer science knowledge
If anything is not clear please ask -- it is my fault, not yours

Core topics
  basics of untyped lambda calculus
  programming in lambda calculus

Very briefly others

### 3
### 4
tried introducing syntax only, was confusing
mental model helps
### 5
lambda -- definition of anonymous function of specified variable
prefix notation
only one of possible interpretations, but convenient
### 6

Explain grammar
Lambda terms consist of three things: variables/abstractions/applications

### 7
This is a term that consists of a single variable, v1

>> What does its AST look like?
### 8
A single variable node
### 9
application of x to y
not a valid term, missing parentheses
convention: application binds to the left
### 10
The root is an application; its children are two variables, x and y
### 11
abstraction
again, we omit redundant parentheses
full-stop is opening parenthesis that extends until the end of subterm
### 12
abstraction has just one subterm, so the tree has two nodes
### 13
More complex example
### 14
variable under abstraction is bound by it
unbound occurrence: free
terms with no free occurrences: combinators

### 15
same variable can be both free and bound in a term
### 17
For convenience terms are written as linear expressions (like arithmetics)
This was static description
What operations can we perform on those trees?
### 18
remove abstraction under application
replace *free* occurrences of x in M

### 19
1. x y is M, \z.z is N
2. z is M, y is N

computation! (function evaluation)
### 20
bound occurrence example
### 21
in which order do we reduce? Reduction strategies.

call-by-value: start with innermost, do not reduce under abstraction
call-by-name: start with outermost, do not reduce under abstraction
like in scala

does order matter?
### 22
confluence (for unrestricted beta-reduction)
does every reduction chain terminate?
### 23
### 24
>> who is completely lost? who understands everything?
### 25
FP = programming with mathematical functions
semantics -> we will investigate functional programming

### 26
this is how it is commonly written
we only have lambda terms. How do we represent boolean values?
### 27
given this representation, how can we encode conditional?
### 28
apply the boolean to the values for two branches

Peano numbers: zero and successor
### 29
each number is a fn of two args
zero: like false (incidentally)
succ: takes an n and produces a number where s is applied to n, passing through two args

What do actual numerals look like?
### 30
Church encoding
How do we do arithmetics?
### 31
minus is tricky
we can define equality etc.
how do we do factorial?
### 32
names we assigned so far -- just macros, not part of the language
how do we do recursion without names?

### 33
Best explained on an example
### 34
like factorial, but takes the function to call as arg
Intuition: Y feeds a function to itself
let's convince ourselves it works
### 35
### 36
we have seen we can represent basic programming constructs and objects such as numbers as lambda expressions
why is it useful? easier to (formally) reason about the semantics of programs we write
### 37
We work with statically typed language
### 38
idea: function type specifies type of arg and result with arrow in between

arrow binds to the right

another way to introduce types: explicit type annotations on abstractions

how are the types assigned?
### 39
this is how rules of inference are written
### 40
types are assigned by building derivation trees using those two rules
structure follows the struture of lambda term
### 41
we defined a new calculus, with different set of valid terms
simple types do not permit omega or Y
balancing act: allow expressing more programs, disallow bad programs
can extend simple types

more complex types systems permit more programs
what are those more complex type systems?
### 42
### 43
Three basic extensions of simple types:

\2: System F, polymorphism (terms depending on types)
\w: type operators (types depending on types)
\P: dependent types (types depending on terms)

extensions can be combined
### 44
lambda cube
\w: Fw, popular research type system
where is object orientation (Scala)?
### 45
should be a fourth dimension

subtyping can be combined with some other extensions
### 46
Scala still not there

### 47