I recently managed to get my MSFP2020 extended abstract uploaded to the arXiv (don’t worry, link to follow!). It took me this long because I finally need to cite it – which is to say, because everything’s taking me this long. But it’s about time I blogged at least a little about it and upped some related things into my own space.
History and Ideas
It’s been a long trip (…a decade and counting so far) and it’s far from over, but once upon a time I read the first paper on information effects1, had an idea that matched some of my existing ones and have found myself feeling increasingly obligated to drag it across the line as I keep seeing more things come of it.
Perhaps the key idea of my own is: the information, in the Shannon sense, created by an [abstract] interpreter is the meaning of the program it interprets. Typecheckers very much included. But it’s also fair to say that as an effectful (effect-oriented?) hacker I’m further opinionated about how to exploit that!
The major things I’ve actually talked about so far are information aware type systems – a constraint-based way to present type systems that allows for careful accounting of information flow – and telescopic constraint trees, a representation of typechecking problems that is to some extent necessary for handling sufficiently dependent types. I can derive the trees (and the rules for them) from Information Aware rules, or even the typing rules from rules for building trees! While I definitely can’t do it mechanically, I can even have a go at reverse-engineering a type system from an example program and a worked example of typechecking it. And hopefully, if the work makes sense to you then you’ll be able to as well.
Telescopic constraint trees themselves aren’t new (as mentioned in the acknowledgements, Conor McBride got there first and they’ve spent a long time as folklore). The relationship between my presentation of them and my presentation of typing rules is new, and because it’s not fixed to one type system I’ve found myself in the awkward position of having to name a piece of folklore. There’s a good tutorial paper about applying the folklore to Hindley-Milner mentioned in the acknowledgements section, and I’ve cheerfully stolen the approach to generalisation (and the sequencing it requires) from it.
I’ve had a lot of fun with this, and I have some other old ideas to resurrect and throw through some of this machinery as well. Recently though I’ve been working on a collection of related logic languages (one of which I’m calling Nooblog2), with the goal of building the metalanguage for information aware type systems (and other related problems: elaboration needs some extra tricks for example).
Material
Here’s my MSFP2020 material, variously from arXiv, my own site and YouTube:
- MSFP2020 Extended Abstract – Information Aware Type Systems and Telescopic Constraint Trees
- Slides
- Talk Video
While I’m here, I’ll add some alternative bits and pieces, some older and some newer:
- Idris Developer’s Meeting 2021 mostly focuses on telescopic constraint trees including discussion of substructural languages and an observation about Quantitative Type Theory that Conor McBride and I had separately and got round to discussing in 2016
- SPLS October 2019 – Telescopic Constraint Trees is an earlier talk that contains some discussion of structural rules for telescopic constraint trees themselves, and of what happens when we discover a local metavariable actually needs a more global scope
- Information Aware Type Systems and Telescopic Constraint Trees [Extended Mix] has a worked solution (complete with some deliberately arbitrary choices) of a telescopic constraint tree problem
Several of these slides mention a Twitter account that I have since deleted. Email addresses should still be good, and contact details are on this site’s About page.
Acknowledgements
Finally, I should make some acknowledgements that I haven’t had room for elsewhere:
- First of all, Conor McBride, not just for the discussion and filling me in on the history, or even for having developed a telescopic constraint tree for Epigram 1, but also for the amount of personal support and encouragement they’ve given me over the years.
- On which note, Adam Gundry also deserves a mention for the conversation in 2012 when he was still Conor’s PhD student! Adam, Conor and James McKinna’s Type Inference in Context is an excellent paper for anyone who wants to read a slightly more conventional take on this using Hindley-Milner as a minimal motivating system.
- Everybody who has reinvented telescopic constraint trees, and especially everybody who tried to get there when dependent types had provided the motivation but no answer was available. I have a story to tell about this (and the inevitability of it), and some year I’ll get it into a suitable state for a wide audience: those who don’t want to wait should consider that I build the trees by isomorphism and ask themselves what happens if a language is capable of reifying metavariable binders.
- Edwin Brady for plenty of useful chat and encouragement to give my first SPLS talk of 2019 (the part where I dual-wielded a microphone and the stick for pulling the screen shades down to point at the screen is not, technically, his fault).
- Chris Martens for helping me get started on the citation trail for something akin to the notion of moding I’m using. Also their online class on Twelf at the start of last year, which I should still post about!
- The MSP101 group and everybody who’s been part of it over the years for variously hosting and putting up with me.
- Sam Lindley for encouraging me to submit to MSFP2020 after the announcement at SPLS October 2019.
- Both Sam and Max [New], Freelance Programme Chairs, as well as my reviewers and my shepherd Stephanie Balzer.
- Paolo Giarrusso for helping me refine my material for people who think less like me.
- Dominic Orchard for his enthusiasm and cheerleading.
- Clarissa Littler for discussion and support.
- My ex AJ for supporting and otherwise putting up with me during my 2019/early 2020 burst of activity.
- Everybody who’s ever put up with me producing an iPad with some slides loaded and asking “would you like to hear about my work?”, however much context they did or didn’t have!
