Haskell

functional

We can express lambda calculi

\begin{equation} f = \lambda x . x \qty(\lambda y . y) \end{equation}

def f = \x -> x (\y -> y)

This is currently polymorphic

Haskell primer

pairs!

dup' :: a -> (a,a)
dup' x = (x,x)

arrows here are right associative

pattern match

fst :: (a,b) -> a
fst (x, _) = x
fst (x, _) = x

underscore has special meaning

lists!

a list (cons)

1 : 2

nil

[]

we can also write

[1,2]

ADTs

data IntList = IntCons Int IntList | IntNil

btw; you can also use `backticks` to infix something, so to construct something you can write

type theory and well-founded sets

Program Verification

Proving certain properties about programs—perhaps types, but not just types.

Program verification proofs are usually written manually, but uses a proof assistant which…

proof assistant

Helps with proof, by:

1. checking the proof for correctness (uses type theory)
2. helps automate the easy parts

Agda

A whirlwind tour through Agda

Agda whitespace rules

Agda allows UNICODE! IN! VARIABLES! so:

i:Int is! not! i : Int

• the first thing is an indentifier of type i:Int
• the second thing is an i of type Int

Dependent Type Theories with Agda

booleans

Consider two empty declarations:

data False : Set where

this is a type with nothing in it!

record True : Set where

this is a type with exactly one thing in it!

False has no elements in it, and True has exactly one element in it.

Today’s lambda calculus

why static typing?

• find type errors when the program is written
• …which makes guarantees for all possible executions
• …which can leads to a faster execution because you don’t have to do runtime type checks (this is actually non-trivial!)

why (not) static typing

• you can detect type errors during execution—so it can be sound as well
• this is not untyped: you can still have types (untyped is raw bits)

implementation

every value has a “tag” — for instance, integers vs. functions

more Combinator Calculus and confluence