Martin Sulzmann
What students usually think programming is:
What programming actually is:
Therefore, there is no need to worry. AI will not replace us. Copilot is just a tool.
Keep in mind:
If ChatGPT can write, e.g., quicksort, in 5 seconds, why are we here?
Programming is not typing code
Programming is turning vague ideas into precise, verifiable artifacts
Idea:
Split array (some totally ordered collection of values) into those that are lesser and greater than a certain element (commonly referred to as the pivot element).
Quicksort the lesser and greater array.
Concatenate the results.
Let’s consider some examples where we write [x1,...,xn]
to denote an array of n elements from x1 to xn.
[3,2,5,1,4]
Pick first element 3 as our pivot element.
lesser = [2,1]
greater = [5,4]
quicksort [2,1] => [1,2]
quicksort [5,4] => [4,5]
Then,
quicksort [3,2,5,1,4]
= (quicksort [2,1]) + [3] + (quicksort [5,4])
= [1,2] + [3] + [4,5]
= [1,2,3,4,5]Challenge: Implement Quicksort in 2min (without using google, …).
quicksort [] = []
quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater)
where
lesser = filter (< p) xs
greater = filter (>= p) xs5 lines of code. That’s it. In Haskell we write ++ for list concatenation.
The Haskell code directly corresponds to the quicksort specification.
The code below can also be found here
void display(int x[], int low, int high) {
printf("\n x[] low = %d high =%d \n", low, high);
for(; low <= high; low++) {
printf("%d ", x[low]);
}
}
void swap(int* x, int* y) {
int temp = *x;
*x = *y;
*y = temp;
}
void quicksort(int x[],int left, int right){
int i, j, pivot, temp;
if(left < right){
pivot=left;
i=left;
j=right;
/*
1. Partition array
(a)
From left and right compare against pivot element.
Adjust i (upper left frontier) and j (lower right frontier).
Swap if frontiers haven't met yet.
(b)
Swap so that pivot element is placed in the middle.
2. Recursively quicksort
(a)
All elements lesser (or equal) than pivot element.
(b)
All elements greater than pivot element.
*/
// (1a)
while(i<j){
while(x[i]<=x[pivot] && i<right) // (I1)
i++;
while(x[j]>x[pivot]) // (I2)
j--;
if(i<j){
swap(&x[i], &x[j]);
}
}
// (1b)
swap(&x[pivot], &x[j]);
// (2a)
quicksort(x,left,j-1);
// (2b)
quicksort(x,j+1,right);
}
}
/*
Further comments.
(I1) The side condition "i<right" ensures that we stay
within valid array bounds.
We might reach the case that i = right.
Access to x[right] is valid, so we can safely evaluate
x[i] <= x[pivot] and then abort the while loop because
condition "i<right" no longer holds.
(I2)
*/Given n > 1000 integers, write a function to return the smallest 5 integers.
In class live coding.
Programming still matters because abstraction level determines how we can reason.
The Haskell code is correct and implements the quicksort idea (this can be done via simply symbolic reasoning steps)
The C code looks okay but verifying its correctness is much harder
We can compare Haskell and C as follows.
C is a low-level language, great for reasoning at the machine level:
Total control over the “machine”
The user needs to take care of all low-level details (memory management, …)
Few safety and correctness guarantees (there’s a significant gap between the C code and the specification)
Haskell is a high-level language, great for reasoning at the math level:
No control over memory and evaluation strategies (all done automatically)
The user does not need to worry about low-level details
Can establish strong safety and correctness guarantees (the Haskell code pretty much corresponds to the specification)
Let’s play with lists in Haskell.
Some live coding.
Here’s the gist of it.
The above program type checks but running the program leads to a crash (“Prelude.head: empty list”).
Do you know similar situations in other languages?
How can we catch such bugs without having to run the program?
Idea: We make use of expressive types to represent program properties.
Types classify values. For example, the type Int
represents all integers (of a fixed size).
The list [true,false,true] has the type
[Bool]
What if we could additionaly describe the length of lists in terms of types?
Wait a sec, the length is a value, this would mean types depend on values? Yes!
In languages with parametric polymorphism we can mimic dependent types by encoding values via types. The general idea is to introduce phantom types. These are types where some of the type parameters are not connected to any program terms. We will see such an example shortly.
Here’s a representation of length-indexed lists. in Haskell.
-- Natural numbers.
data Zero = Zero
data Succ n = Succ n
-- Length-indexed lists.
data List a n where
Nil :: List a Zero
Cons :: a -> List a m -> List a (Succ m)Some live demo based on the following Haskell playground code.
Can this be done in other languages? Yes.
Programming is about precision in a world of ambiguity.
Programming is more than coding
Thanks to AI tools less emphasis on coding more emphasis on formal specification
For example, we could view the Haskell quicksort version as the formal specification and the C version as the code that implements the specification
This course is about:
abstraction
formal reasoning
language design differences
specification discipline
intellectual responsibility
where we focus on Haskell.
Some teaching materials were developed with the assistance of AI-based tools.