Day 2 of PL
Fri, 22 Dec 2023 17:54:07 -0500
Day 1 was very theory-heavy; I have a post drafted up for it but I’m not sure if I’ll publish it here. Perhaps in the bird-nest but who knows? If you’re interested just let me know via email or comment on my Neocities site page, but it’s likely that I’ll just post it anyways, because who doesn’t love theory?
If you’re curious, it is mainly just the very basics of lambda calculus. I go over lambda-notation, some basic definitions, and different types of reductions (alpha, beta, eta…), and include some useful (to me, anyways) links for further reading.
For Day 2 I decided to go a bit more hands-on by tinkering around with Lisp and Ocaml. I wanted to balance the theory with some practice, after all. My main exposure to Lisp is Emacs Lisp via my config file, so not much.
I’ve been pulling kinda haphazardly from a handful of sources:
- CS3110 from Cornell University; a functional programming and software engineering course
- CS421 from University of Illinois at Urbana-Champaign; a programming languages course
- Software Foundations from University of Pennsylvania; multiple formal verification courses
- The infamous Structure and Interpretation of Computer Programs from MIT, though sparingly
CS3110 and Software Foundations are bit more organized and easier to tackle as a student who doesn’t go to either of these schools.
I will mention that both CS3110 and CS421 teach Ocaml, and that Software Foundations is rather different from either of them due to being an entire suite of courses rather than just one class, and also due to the fact that it focuses on formal verification and thus teaches Coq extensively.
So all these classes definitely have their own distinct flavor, but they still centre around (or at least, make it a point to cover in-depth) functional programming languages.
Setting up an Ocaml workflow is not too bad. I will note however that
the Opam set-up script that was auto-generated and placed into my
init.el
severely slowed down the start-up
time for emacs, to the point where it took 5 seconds just for emacs to
properly open. Instead of leaning on that user set-up script and Merlin,
I’d recommend downloading and just using the tuareg package. Right now I
have no clue which line in the Ocaml script was causing such latency,
but I’ll benchmark & look into things later.
Some Ocaml notes
A demonstration of scope and alpha-reduction
The notion of alpha-reduction in Ocaml is demonstrated via a concept called scopes. You may have heard of the related concept of shadowing a variable.
You can explicitly define a scope of a given variable x like this:
let x = 12 in x + 1
This binds the value 12 to the variable x
only within
the expression x + 1
.
A (bad practice) demonstration of scope:
let x = 12 in
(let x = 13 in x + 1) + x
This ultimately ends up resolving to 13 + 1 + 12
.
Variable shadowing occurs in the parentheses. I like to think of it as
scopes overlapping. Generally, you do not want this to occur in your
programs as it impairs readability.
This reinforces the notion of variables’ names not really mattering. This is clear in math, where f(x) = x^2 and f(y) = y^2 defines the same function, semantically.
The fact that variables’ names don’t really matter is formalized in alpha-reduction (which may sound fancy, but it is just saying that you can replace any variable with any name, as long as you are consistent about it).
Anonymous functions (lambda notation)
You can define anonymous functions in Ocaml; that is, functions without a name, like this:
fun x -> x + 1
In lambda notation, this would be written as:
\lambda.x.x+1
You can also name anonymous functions, which might sound kind of silly:
let incr = fun x -> x + 1
You might think, hey, isn’t that just a longer way of saying:
let incr x = x + 1
Yes! The latter is just syntactic sugar for the former. All functions in Ocaml seem to be born as anonymous functions under the hood.
Lists
Lists are a first-class part of Ocaml, much like Python, Haskell, and Lisp. There’s no need to use a library like in Java or C++. All elements of a list must be of the same type.
To prepend an element to the head of a list, there is an operator
that Ocaml has taken from Lisp: the cons operator, signified by
a double colon ::
.
4 :: [1;2;3]
yields [4;1;2;3]
This is a constant time (O(1)) operation.
You can also append to the end of the list. Ocaml has its own
operator for this too: the @
operator.
[1;2;3;4] @ [5;6;7;8]
yields
[1;2;3;4;5;6;7;8]
We note that this is a linear time (O(N)) operation, where N is the length of the first list.