I've been recently trying to get back to doing more Functional Programming and Type Theory. One of the things I've done is taking part in a free 5-week online course organized by Chris Martens. Originally, it was playfully titled Special Topics in Chris Martens: Logical Frameworks. For those not familiar, this is a reference to Special Topics courses, like Special Topics in Programming Languages. These are advanced one-off courses that are typically not included in the standard curriculum.
This particular course was focused on the Twelf programming language and its underlying formal system. The formal system of Twelf is the Edinburgh Logical Framework (LF), which is described in the paper A Framework for Defining Logics by Harper, Honsell, and Plotkin.
When the course was announced in January, I immediately signed up. I was curious how Twelf compares to Agda and Rocq, which I was familiar with. Outside of coming across Twelf on Oleg Kiselyov's website a while back, I had no idea what to expect.
To prepare for the course, Chris recommended TAPL chapters 8 to 12, which introduce Simply Typed Lambda-Calculus. But I ended up reading the earlier chapters as well. For a Type Theory book, I found TAPL very readable. This is likely because I was already familiar with the material. But I think it might also be due to how the book is structured. TAPL makes good use of typography to highlight different types (no pun intended) of information, splits text into manageable paragraphs, and has these big margins for taking notes, which I absolutely love.
You can find the syllabus, schedule, and code on the course website. But these are not replacements for the course itself because it's meant to be interactive. There were two sessions per week: one lecture, where we also got homework assigned, and one meeting for group discussion.
Over the course of eight virtual sessions, we did quite a few things. Naturally, we went through the basics of Twelf. Then proved some properties of Binary Search Trees and AVL Trees as a warmup. After that, we studied LF and Higher-Order Abstract Syntax (HOAS). Chris derived the typing rules of STLC and then translated them to Twelf. We also covered Canonical Forms. There were plenty of opportunities to ask questions and the whole atmosphere was very inclusive, with textual and voice chat on Zoom as well as long-form discussions on Zulip.
Despite being a free course, everything was exceptionally well organized. Lectures and discussions started and ended on time. Digital whiteboard and live coding were used to present material step by step. Exercises had various difficulty levels, some were open ended. Chris were also very active on Zulip outside of class hours.
Our group had a good mix of beginners, people curious about Functional and Logic Programming, PhD students and Programming Language Theory researchers, and Twelf experts. Although people had various levels of experience, the course was well balanced and addressed the needs of all.
Speaking of Twelf experts, I'd like to thank Rob Simmons for quickly sharing background information on some of the obscure features of the language. He also did some infrastructure work, such as creating a Docker container to make it easier to install Twelf. Additionally, Rob configured Twelf Live, a Twelf interpreter that can be accessed from a browser.
I also want to highlight the efforts of Jason Reed. Jason has been working on the Twelf LSP server and Twelf on WASM, which powers Twelf Sandbox.
It took some time to create the mentioned infrastructure. So before it was available, I managed to install Twelf using the following commands (on macOS):
% git clone https://github.com/standardml/twelf
% cd twelf
% brew install smlnj
% export PATH=/usr/local/smlnj/bin:"$PATH"
% make smlnj
% bin/twelf-server
# try loadFile
Vim syntax highlighting is available in the course repo. I modified it a bit to my own taste:
Here's my syntax highlighting code:
" modify ~/.vim/syntax/twelf.vim and add these:
hi twelfPercentKeyFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=MediumPurple guibg=NONE
hi twelfTypeFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=orange guibg=NONE
hi twelfCommentFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=LightGreen guibg=NONE
hi twelfSymbolFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=DarkGrey guibg=NONE
hi twelfPunctuationFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=LightBlue guibg=NONE
hi twelfDeclarationFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=hotpink guibg=NONE
hi twelfFreeVariableFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=lightgreen guibg=NONE
hi twelfCurlyFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=gold guibg=NONE
hi twelfSquareFace term=NONE cterm=NONE ctermfg=green ctermbg=NONE gui=NONE guifg=purple guibg=NONE
" put these in ~/.vimrc
set termguicolors
colorscheme ron
" Wrap long lines.
set wrap
set textwidth=80
highlight ColorColumn ctermbg=red guibg=hotpink
I'm going to briefly mention some of the features of Twelf that make it different compared to other dependently typed languages, like Agda.
Being an old system, Twelf doesn't have any interactive features.
You interact with it by loading files into the interpreter.
There is no support for tactics either.
Twelf does offer some automation via %solve, which allows it to instantiate a type.
The experience might also be slightly better in Emacs, I think it reloads code automatically, but I haven't personally used it.
Totality is opt in rather than being opt out.
Also, you need to declare how your definition is supposed to be used.
This is done using some combination of
%total,
%mode,
%block,
%worlds, and
%freeze.
I mention the last one in particular because a Type Family is automatically frozen to avoid soundness issues after a %worlds declaration.
My FP background is mainly in Haskell and Agda, which is also the syntax I generally prefer, so I had to adjust a bit to Twelf in the beginning. But after the first lecture and doing the exercises it was fine. I'd say the main visual difference is this: when doing proofs, you need to define Meta Variables for the result of an expression. This especially comes up in proofs by induction. In Agda, you'd just make a recursive call, but in Twelf you refer to the result variable declared earlier.
Spoiler alert: the following listing is an answer to one of the exercises.
For example, see how I go from A to B to C here and then also declare C as the result of the definition:
every-nat-eo/s
: every-nat-eo (s A) C
<- every-nat-eo A B
<- eo-succ B C.
In Agda, it looks like this, which is just a recursive call:
every-nat-eo (s n) = eo-succ (every-nat-eo n)
I want to highlight that all of these things are not bad and not good, just different. Some students did have problems with totality checking being opt in, because it resulted in missing cases. But I could also imagine contexts where built-in totality checking, like in Agda, would be getting in the way. So it's nice to have different systems at your disposal.
At the end of the course, we also got a chance to present our own work:
My demo ended up being a two-part introduction to Agda and computer-assisted theorem proving. It's an hour-long interactive talk done in Spacemacs and it doesn't have any prerequisites outside of general programming knowledge. Since I already have the materials, I'd be happy to give this talk again (free of charge). The target audience for this could be students, an FP meetup, or a company curious about FP. Please let me know if you're interested.
As someone who grew up in the era of floppy disks, when computers were not always connected to the internet, I'm very excited about opportunities available today. I wish more people did things like this course. Besides learning new material, I've met new people and reconnected with folks I used to talk online ten years ago. Also, because I had such a great time, it made me seek other opportunities like that. For privacy reasons, I didn't mention all course participants in this post, only those actively participating and who I asked beforehand. But I'd like to thank everyone once again, and especially Chris Martens, for making this group a success.