One of the best arguments against type theory, as it is incarnated today, is that too much proof search is built into the core calculus. This of course all stems from that pesky conversion rule.

Γ ⊢ e : A    Γ ⊢ A = B
---------------------- (Conv)
      Γ ⊢ e : B

The problem here being that the equality judgement doesn’t embrace one of the virtues of type theory, being that propositions come with proof terms. Since the typing derivation has a proof term, and the proof term reflects the typing judgements of the language (basically having one piece of syntax per typing judgement), it is easy to check that a term is well typed. And more importantly the amount of work it takes to type check a term (ignoring Conv) is reflected in the size of the term itself. These virtues are broken by the conversion rule, since there is no judgemental equality proof term to guide the checking, and the amount of work to come up with a proof of judgemental equality is certainly not reflected in the proof term for the typing judgement (having basically O(Big) time complexity).

These are certainly problems, and they were articulated well in both A Logical Framework with Explicit Conversions, and Quadratic Type Checking for Objective Type Theory. But I have another problem to pick with the conversion rule, mainly that it builds just enough proof search into the system that it placates the user and so no good tooling for external proof search is built. Contrast this with Isabelle, which certainly has problems of its own, but doesn’t have proof search for the equational theory over the entire lambda calculus+++ built in. Instead, Isabelle has excellent tooling for external proof search, and lets you unleash the power and glory of about five different SAT solvers in parallel to try and solve whatever problem you may have. Personally, I’d like to use a type theory with this level of enthusiasm for having the computer aid in writing your program. But instead, for now, we’re stuck with mediocre, complicated proof search built into our core language.

In my philosophy of logic class, a point was made that propositions can’t possibly be truth valued expressions since it would mean that all true propositions are “the same”. Later on in the lecture, this point was then dismissed, but my immediate reaction was that this obviously can’t be true, since mathematics treats them this way (the point being brought up in the context of “meaning” in linguistics). And while it may be true, knowing ∀x, y : ℕ. x + y = y + x is certainly more useful than knowing ⊤. However, while I’m sure that this reaction is correct, I haven’t been able to articulate why, so I will use todays poast to try and work this out.

I think the answer, as it did in class, comes down to the meta/object language destinction. In the object language it is the case that (∀x, y : ℕ. x + y = y + x) = ⊤, and so to the object language they are “the same”. However, in the meta language they are now humble pieces of syntax which are distinguishable.

I suppose then, what I meant earlier by the former being more “useful” than the latter is this. During a proof we must of course distinguish a universal quantifier from top, since some proof rules apply to the former and not to the latter. Therefore proof must take place in the meta language.

This reveals a contradiction I have in my mental model of type theory, where I had always conceived of type theory as a language containing proof and proposition. Indeed, many proof assistants based on it try to present it this way, but the trick is in letting the user ask the question, e : A? Here, the : is a relation in the meta language, it just so happens to be the case that it is decidable, and so the computer can do the “real” proof for you. I guess the genius of type theory here is that the structure of the expressions in the typing judgment mimic the proof rules for : so closely that it is actually almost as if proof and proposition were in the same language. This may also explain why you can do the opposite in a logical framework, making the syntax for the : proof rules feel like writing the expressions themselves.

Extensionally

• Pleasant to look at, it is not currently
• Esoteric, obvious things should be easy to find, but I like websites that you can explore and find hidden gems in
• A record of my thoughts, not academic writing that I assert to be true. This would set too high a bar for poasts.
• A record of things I like, I enjoy websites which link to other material the author enjoys

Intensionally

• Easy to publish to. Pushing to main in my git repo should automatically trigger a pull and build on my server. There should also be an easy way to publish from my phone (that this isn’t easy has hindered some of my poasts being published in the past few days).
• Described in one place. I like the idea of taking a leaf from choreographic programming and writing a Haskell library which lets you describe a website in Haskell and then serves it.
• Resource efficient, shouldn’t be bloated with js frameworks just to show something easily described as a static site. This doesn’t mean that I couldn’t have pages which are resource intensive, there just needs to be a good reason for it.
• Easy to develop. Though I want to ditch Hugo, live reloading is incredibly nice to have, somehow this needs to be possible with my Haskell framework (even if it is just monitoring files for changes, then killing the server, re-compiling it, and running it again).

This semester I set myself a few goals, one of which being that I will write a single blog post. However, I think now that this was a mistake. If writing a blog post was truly difficult and time consuming, then maybe it would have been appropriate. But as it stands, it takes me at most an hour to write one and publish it. This means that in my head I know that it’s a small thing, a simple thing, and so I procrastinate.

I think the problem here is the mismatch between the simplicity of writing a blog post and the importance it is given by making it a semester goal. My other two goals are quite large, both being writing semi-complicated pieces of software. Therefore I am officially upgrading my blog writing goal to one post a day, leaving myself no room for procrastination.

The word “should” will be used a lot in the following post.

I should be able to tell Agda (or <insert language with theorem proving capabilities here>) how to compile my data types. The compiler already uses some heuristics to choose an isomorphism between my inductive types and their runtime representation, so I should just be able to make its life easier and give it one.

Here’s the vibes for what I should be able to write

-- Agda should provide this universe of runtime types
RuntimeCode : Set
RuntimeEl : RuntimeCode -> Set

data MyBool : Set where
  MyTrue : MyBool
  MyFalse : MyBool

myBoolCode : RuntimeCode
myBoolCode = Refinement QWord (\x -> Either (x = 0) (x = 1))

there : MyBool -> RuntimeEl myBoolCode
there MyTrue = MkRefinement 1 (Right Refl)
there MyFalse = MkRefinement 0 (Left Refl)

andBackAgain : RuntimeEl myBoolCode -> MyBool
andBackAgain (MkRefinement 1 (Right Refl)) = MyTrue
andBackAgain (MkRefinement 0 (Left Refl)) = MyFalse

{-# RUNTIME_REPRESENTATION MyBool myBoolRuntimeRep #-}
myBoolRuntimeRep : Iso MyBool (RuntimeEl myBoolCode)
myBoolRuntimeRep = MkIso there andBackAgain
-- plus proofs that going there and back again is id

I don’t have this totally worked (or even kind of worked out), but this should be something that I can do in a language with the kind of power that Agda does. Of course this could be extended further, I should be able to give Agda some assembly code with a proof that it correctly implements a function.

NbE With Effects

Usually when playing with dependent types we are tempted into creating pure languages. This may stem from a few different places, the sort of person who wants dependent types is more mathematically inclined and pure languages are closer to math (or are math), or maybe they feel (possibly correctly) that pure languages have nicer engineering properties. However there is one fundamental reason that I think trumps them all, dependent types require comparing arbitrary programs (even ones with free variables) and deciding if they are equivalent.

This is quite easy when the programs are pure, simply run them to their final state and then compare the results, maybe using a few tricks during the comparison, such as alpha and eta rules. Once we want to add in effects however, things get more complicated. With a pure program we have the sense that the final state of an expression, its normal form, encompasses everything there was to know about the expression. The expression (\x. x + 2) 2 doesn’t really convey more information than simply 4. However if we run print "Hello, World!" and get just (), it really does feel like some information is lost, information that we would probably want to use to decide program equivalence.

NbE Without Effects

Let’s take a quick detour and talk about how we usually normalize pure programs. The normal method is to use NbE (normalization by evaluation). There’s a two main reasons for this, it’s usually easier than other methods, and it’s usually faster than other methods. Depending on the day, the fact that this is the case either feels like we’re breaking some law of nature, or completely natural and the perfect embodiment of Rob Pike’s third rule of programming. In any case, the gist of it is this, we transform our expression into some other form where normalization is easier, then we transform back into an expression in such a way that we only produce normal forms. The domain where the forms we transform into live is called the value domain, the transformation from expression to the value domain is called eval, and the transformation back to expression is called quote. This leads us to a system that looks a bit like this.

             eval
            ------>
Expressions         Values
            <------
             quote

The key point to emphasize once again is that the composition of eval and quote always takes expressions to their normal form, even if they have free variables.

NbE With Algebraic Effects

Luckily for me there’s already some work on extending NbE to handle effectful programs, namely the paper by Ahman and Staton, Normalization by Evaluation and Algebraic Effects. Unfortunately for me there’s much to much math in the paper for my brain to parse currently, but I’m pretty sure the NbE algorithm in the paper looks something like this.

                   eval
Expression with   ------> Realm of
Algebraic Effects <------ Mathematics
                   quote

The problems here are that A. I don’t have the realm of mathematics installed on my machine, and B. the language I want to normalize isn’t explicitly one of algebraic effects. However, I think that inspiration can still be drawn from the paper to solve our problem using one key insight they bring up. That is that algebraic effects can be normalized by way of the equation defined for each effect.

Algebraic Effects Without NbE

Let’s take another small detour to quickly discuss what the heck is an algebraic effect. Imagine that we have some program with a single bit of global state. This bit could be thought of as some global boolean switch that we can turn on and off. We might use some function read to read the state, and write to write to it. This would let us have a program like the following:

do
x <- read
if x
then
  do
  write 1
  return "Hello!"
else
  do
  write 0
  return "Goodbye!"

If we were to transform this program into one which uses algebraic effects it would look like this:

read [\x.
  if x
  then write 1 [\(). return "Hello!"]
  else write 0 [\(). return "Goodbye!"]
]

I think the best way to think about this transformation is that each effectful function from before has been turned into the node of a tree where each node has as its child the continuation from the original program.

Now that we have an expression using algebraic effects, we can ask the question, what would it’s normal form look like? Notice in the program above that there’s some redundant writes going on. If the global state is 1 then we “change” it to a 1, and if it’s 0 we write a 0. We can write down an equation that maybe captures this intuition that some algebraic effect tree nodes can be reduced in some way.

read [\x. if x then write 1 [cont] else alt] = read [\x. if x then cont () else alt]
read [\x. if x then alt else write 0 [cont]] = read [\x. if x then alt else cont ()]

There are other equations we could write down, maybe if we write then immediately read we could just remove the read since we know what the state is, but these two will do for now. If we apply these equations to our program to try and get the smallest program possible, then we would get the following:

read [\x.
  if x
  then return "Hello!"
  else return "Goodbye!"
]

Transforming back into our original language we would get:

do
x <- read
if x
then return "Hello!"
else return "Goodbye!"

For a more detailed discussion, and to learn what’s so algebraic about algebraic effects, please see What is Algebraic about Algebraic Effects and Handlers? by Andrej Bauer.

NbE With Algebraic Effects, For Reals

Ok we’ve finally gotten to the good bit, how to do NbE on a program containing effects. In fact we’ve already seen it in the previous section. There we transformed a program into one with explicit algebraic effects, applied some effect equations, then transformed back into the original language. This is simply NbE where the value domain handles effects using algebraic effects. For fun, and for profit, let’s look at this process using an actual real life example that occurs in a project I’m working on. This project contains a language which sits somewhere after closure conversion, and is one where closure allocation has been made explicit. We have some form for allocating closures malloc-clo, and one for applying them app-clo. Let’s look at a simple example for the source program (\x. x) 10.

id env x = x

do
f <- malloc-clo id ()
app-clo f 10

Here the lambda in the source program has been hoisted up to the global level and been named id. If we turn this program into one using algebraic effects, we would get.

id env x = return x

malloc-clo id () [\f.
  app-clo f 10 [\res. return res]
]

Just like we did for the global state example, we can write down some equations to capture our intuition that some effects are redundant.

malloc-clo l env [\f. B(app-clo f a [cont])]   
=
malloc-clo l env [\f B(cont (l env a))]

where B(c) denotes some expression B containing c

malloc-clo l env [\f. B]
=
B
where f does not appear free in B

Now applying this first equation to our example gives us:

id env x = return x

malloc-clo id () [\f.
  return (id () 10)
]

and applying our second equation, and the definition of id gives:

id env x = return x

return 10

This is great considering our intuition that (\x. x) 10 normalizes to 10. It’s also great since we never even really had to simulate heap allocation or the like, even though that’s sort of the effect that we would want from malloc-clo.

It remains to be seen whether or not this approach will pan out, but at least it’s interesting.

Unix is a live programming language.

Files can be thought of as objects which only respond to two messages, read and write.

Plan 9 and FUSE both add the ability for read and write to do more than just do disk i/o.

This makes Linux sort of like a Smalltalk where objects are programmed through FUSE.

The file system provides the “live” part.

Because files can be updated during execution (while the operating system is running), and because there is a level of indirection to refer to them (file paths are pointers, not the contents of the file), changing how a files responds to read and write messages will change how other parts of the system function.

For example, imagine changing /bin/echo to point to a program which is like normal echo but prints a space between each character. How would this change the behaviour of other programs which use it?

The genius of Plan 9 is that it is a distributed object-oriented language which restricts messages to simple byte streams.

In this view, however, executing files is a bit weird.

We can think of exec as a message which causes the object to treat the output of a read message sent to itself as machine code and run it on the cpu.

Hashbangs let us override this behaviour.

The analogy between object orientation (in the original sense) and Unix is more than a novelty, it can bear fruit.

If exec is weird, is it truly needed? Smalltalk itself has no exec.

Imagine a Unix where exec is removed and FUSE is made easy to program.

Imagine a Unix where use defined messages are allowed, files being able to respond to more than just read and write.

Maybe even a Unix where more data types are allowed than the humble byte stream? (Gasp)

I have no idea if any of these ideas would be good, but at least they would be interesting and novel.

They seem, at least to me, to be a genuine mutation of the Unix formula (would a Unix without exec even be a Unix?).

I hope I’m smart and dedicated enough to at least try them out.

And if not me, someone else.

Good software is not only a pleasure to use, but is well written. Unfortunately most software is rarely a pleasure to use, let alone well written.

Window Managers

• dwm

Terminal Emulators

This class of software shouldn’t still be so important by now, finding a better solution for creating interfaces to things is a top priority.

• st

Web Browsers

There are no known web browsers which even approach being good. Use something open source, a free browser might be a contradiction in terms.

Text Editors

Text is the most extensible data format at the moment. Being able to edit it will be of vital importance while this is true.

• vis
• kakoune

Programming Languages

To what degree we should ignore the underlying execution of the code and in what way is unclear. Therefore languages such as Haskell cannot be considered good software at the present time.

• C
• Go

User Interface Tools

• dmenu
• wjt
• xmenu

Today we will be looking at 2 lines of shell script. While they may look quite unassuming, when bound to a shortcut (super-v in my case) they will give you a nice and elegant interface for changing the volume on your system. A demonstration can be found here.

The pre-requisite programs for today are the following

• pamixer
• wjt
• xargs

Without further ado here is the script.

wjt -x $(pamixer --get-volume) \
| xargs -I? pamixer --set-volume ?

The best place to start explaining this is probably wjt.

wjt is a very simple program, when you run it it gives the user a slider bar at the top of their screen. Whenever the user changes the value of the slider (by clicking or using one of the shortcuts, see man wjt) the new value is printed to stdout. An initial value can be provided though the -x flag as we do in our script.

Next we use pamixer to interface with pulseaudio. On the first line pamixer --get-volume does exactly what you would expect, it prints the current volume. Say the current volume is 20. When we run wjt -x $(pamixer --get-volume) the code inside the $() is run first. This code is then replaced by its output, which we established is 20, giving us wjt -x 20. When this is then executed a slider pops up with an initial value of 20.

Finally we will cover xargs. When the first line is executed its output (the new values of the slider) is put into the input of the second using the pipe (|) operator. xargs then takes each line of this output and runs the given command with the ? replaced with the input on that line. Say we run the whole script and then change the slider to 21, xargs will receive a line of input containing 21. It will then take its given command pamixer --set-volume ? and replace the wildcard given by the -I flag (in this case ?) with that line of input and then run the new command. This results in xargs running the command pamixer --set-volume 21 which has exactly the effect you would expect, the system volume is set to 21. xargs then repeats this process for every new line of input, giving us a simple, elegant volume widget.

This is my new website! I’m not quite sure about the colour scheme yet, it’s a bit special…