Building a programing language, step by step:

Lambda Calculus

\begin{equation} e \to x | \lambda x.e | e\ e \end{equation}

and you can add types

\begin{equation} e \to x | \lambda x: t.e | e\ e | i \end{equation}

\begin{equation} t \to \alpha | t \to t | \text{int} \end{equation}

Adding ADT

Algebraic Data Type—

\begin{equation} \lambda a_1 . \lambda a_2 \dots \lambda a_{k}. \lambda f_1 . \lambda f_2 \dots \lambda f_{n} f_i a_1 a_2 \dots a_{k} \end{equation}

Logic Programming

Logic is the study of correct arguments. For instance, for some predicate \(P\); for instance:

\begin{equation} \forall x .\exists y. P(x,y) \end{equation}

• we can “prove” this by doing the thing
• we can also do that by contradiction (but that won’t create a witness \(y\) of the statement)

PROLOG

PROgramming LOgic - PROLOG; not general, but good in specific cases (databases, scheduling outputs, etc.)

pros and cons

pros

• very declarative
• easy to write some backtracking search approaches

worst

• “algorithm” / “complexity” obscured because you only have one algorithm
• because you get performance only by wrangling goal ordering

PROLOG time

So, every predicate returns true/false.

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.