Today, we’re gonna talk about conlangs! Conlang is short for constructed language. There’s a bunch of famous conlangs. Esperanto is probably the most famous of the idealistic “let’s unite the world” conlangs—it’s pretty old, going back to the late 1870s. In the 1930s, some dude named Jerry Tolkien published a whole series of fantasy novels just to popularise z$5h# and his other conlangs, an effort we can say was at least passably successful. In recent decades, we got tlhIngan Hol, lekh dothraki and Valyrio udrir, each of which now have communities of speakers formed around them. Heck, two of those even got their’s own DuoLingo course! Unfortunately, one thing all these languages share is that they were created by dudes…
Session types. Ostensibly, I’ve studied them for the past few years, so I should know something about them, right? I am gonna try and explain the foundations of session types, and along the way, there will be programs which crash, Victorian ladies having milk puddings, and tin can telephones.
Neural Networks. They’re, uh, pretty pervasive by now, so you’ve probably heard of them, telling you which of your friends is in that picture, and that they know what you wanna text better than you do. But what do they know? Do they know things? Let’s find out!
This post is a continuation of Constraint Grammar can count!, in which I talked a bunch about how expressive constraint grammar is. Now, for most of that post, what I actually meant was the fragment of constraint grammar where you only use the REMOVE rule. However, I always had the suspicion that I’d be pretty easy to simulate a Turing machine using only the ADDCOHORT and REMCOHORT commands, treating the list of cohorts as the Turing machine’s tape—and I don’t think I was the only one to feel that way.
One of my favourite card games is The Great Dalmuti. It’s a variant of a widely-played card game with many, many names: President, Scumbag, Kings and Arseholes. Each of these may have slightly different rules, and slightly different decks, but they are all more or less the same game.
I’ve had a bunch of discussions about this game over the years, most of which were about the possible strategies. Personally, I don’t believe that this game is all that hard to play well—and consequently, that it isn’t all that hard to write an AI for it. Pehaps even a very simple, rule-based AI can play passably. However, friends of mine think that it is a much harder problem, and that much more advanced techniques will be needed. Therefore, I thought I’d write a little playground for AIs to play in.
Quite a while ago, UnicornPower introduced me to a game called Breadbox. It’s an experimental cousin of 20 Questions, also known as Plenty Questions, which is played by two players—or more, really—who we’ll name Allie and Blake:
- Allie thinks of something.
- As their first question, Blake asks “Is it a breadbox?”
- Allie—who, seeing the mandatory first question, obviously wouldn’t choose a breadbox—answers “No, it’s not!”
From there on out, all Blake’s questions have to be of the form…
- “Is it more like a breadbox, or more like…?”
…where breadbox is replaced by whatever the current guess is, and the dots are filled in with whatever Blake wants. Let’s see if we can write an AI for playing this game!
Previously, I mentioned that one of the most common posts on Agda blogs is implementing the simply-typed λ-calculus. Gergő Érdi even goes as far as to call it the FizzBuzz of dependently-typed programming, and rightfully so: If you do a quick search, you’ll find dozens of examples.
In Dependently-Typed Programming with Agda, Ulf Norell implements a type checker the simply-typed λ-calculus; Francesco Mazzoli more or less follows Ulf, but extends his λ-calculus with a primitive operator for addition; and, Gergő Érdi extends Ulf’s approach with a checker for scope and binding.
I figured it would be more fun if, instead of rewriting the type checker example, I would do something a little bit different. So for my λ-calculus post, I’ll have a look at kinds of different ways of implementing the simply-typed λ-calculus. Today, natural deduction and the sequent calculus.
Constraint grammar—it is a natural language processing formalism with great two distinctions: it routinely scores amongst the highest in tasks such as part-of-speech tagging and word-sense disambiguation, with F-scores at around 99%; and it has made some of the most dubious choices in programming language syntax in history. Though its specification has changed tremendously since CG1, it is nontheless a grammar formalism which sees a lot of usage. One natural question to ask of any grammar formalism is “how expressive is it?”
Over the weekend, inariksit visited me, and we decided to find out!
Back when I wrote this, I had just discovered “Extensible Effects: an alternative to Monad Transformers” by Oleg Kiselyov, Amr Sabry, Cameron Swords, and Hiromi Ishii, and I’ve always had a penchant for mucking about with linguistics and Haskell… so… let’s have a little fun with this library and some basic AB grammars in Haskell, see how far we can get within the universally well-defined maximum length of a blog post!
I wrote this code a long time ago, and verifiying the correctness of some sorting algorithm is pretty much the standard “Hello World! I can Agda!” blog post—well, that and implementing the λ-calculus—but I really wanted an excuse to test my Jekyll/Agda integration…
