Profile cover photo
Profile photo
Dan Doel
219 followers
219 followers
About
Dan's posts

Post has attachment
Public
Someone recently reminded me of the paper on incremental lambda calculus, so I went back and read some of it, along with the blog post by Bob Atkey where he explains how change structures from the incremental calculus are equivalent to reflexive graphs, which can be used to talk about relational parametricity. At the end of the post, he mentions that he hopes that understanding the connection between the two could lead to advances for both.

So, I was thinking about what the connection would mean. The 'obvious' thing to want to do (to me) is to view a polymorphic term as a function that accepts a type, and then take its derivative with respect to the type argument. The derivative would be some related term that accepts 'changes' in types, which are relations through the equivalence that Atkey gives (if I understand correctly).

But then, this starts to sound very much like the work Jean-Philippe Bernardy and others have done on calculi that have internal parametricity. So my conjecture would be that properly incorporating polymorphic types into the incremental lambda calculus would leave you with a generalization of such calculi. So for instance, the incremental folks could look at Bernardy's work for how they would add polymorphic types to their system.

"We can do both things in a single system, because they're actually the same thing," is probably not the sort of "interesting advance" that Atkey was hoping for in his article, but I'd be interested if there's a paper that works through the details and my hypothesis turns out to be the case.

So, I heard that everyone gets to change all their passwords, because Cloudflare may have leaked them. The bug appears (though I'm not an expert) to have been caused because the parser tool they were used is really a thin macro around a C state machine, and expects you to put in-line C in certain parts. And some of that C jumped directly to a part of the state machine in an unsafe way, violating some invariants.

Cloudflare says this is their fault, and not the fault of the parsing tool (Ragel) they were using. But I disagree. It is absolutely the fault of the tool if making a simple error like that causes the tool to generate a buffer overflow, instead of some less catastrophic error behavior, or better yet, failing to compile. (It's of course still their fault for using such a tool.)

I'm not really surprised, though. When people are confronted with catastrophic mistakes that programmers (continually) make, the response is almost always, "programmers should get good and stop making mistakes," rather than, "we should develop and use tools that make these mistakes more difficult or less catastrophic to make."

If you ask me, though, people shouldn't use a parser generator which if used imperfectly causes it to generate massive, invisible security holes.

Hey FedEx. Maybe, if a delivery requires a signature---a signature that I am not allowed to put on the packing slips you leave; it has to be in person---you should attempt to contact me to receive said signature, by knocking on my door for instance.

Maybe I shouldn't have to leave a note for the delivery person telling them to knock, because I am in fact home for the second day in a row, attempting to sign for the package.

Or am I required to sit on the porch and do nothing all morning?

I've been working on our SQL generator lately, and have become increasingly amazed at how complicated, inconsistent and arbitrary SQL's syntax is. A lot of it lately has had to do with 'order by' clauses, and they provide a lot of good examples. (Some of this may be Microsoft specific, but not all of it.)

Previously, I had though 'order by' was part of 'select.' But it turns out you can apply it to things like union. I was surprised, because this actually seems convenient and nicely orthogonal. But there are also many queries you can't apply it to. The one that makes sense is another 'order by', which would be redundant, and 'order by' also can't be used as a subquery in a 'select' for instance. You can have a subquery that uses 'order by' with 'offset/fetch' to get a subset of the relation, but 'offset/fetch' is also not eligible to be used with 'order by', even though there are reasons to want to nest that. (You also can't union a limited result set directly, for some reason.) You must have a 'select' to promote the limited relation to the right syntactic class.

The real fun, though, has to do with the things you are allowed to order by. Since 'order by' can be attached to some subqueries, you can order by whatever columns that query has, without qualification (because the query has no name to qualify by). You are not allowed to order by constant expressions like '1 + 1'. However, you are allowed to order by constant numerals, like '1', which actually refers to the first column of the subquery, positionally.

If the subquery is a 'select', you are also able to order by (non-constant) expressions. These expressions are allowed to mention the (possibly qualified) column names of the tables in the 'from' clause. But they are not allowed to mention the columns selected by the whole subquery.

If the subquery is a 'union' or similar, the things you are allowed to refer to of course come from the first subquery of the 'union', because 'union' is positional. So you can refer to the named columns selected in the first subquery, and are not allowed to refer to the named columns in the other subqueries.

If the first subquery of the 'union' is a 'select', you are also allowed to order by certain expressions in terms of the columns in scope in the 'from' clause. However, the only allowed expressions are the ones that can be detected to be equivalent (possibly up to qualification; not sure) to an expression that was selected. And in that case, ordering by the expression means to order by the positional column that the expression appeared in. So:

select t.a a, t.b b, (t.a + 1) c
from (values (1,2), (2,3)) as t(a,b)
union
select p, q, r
from (values (1, 4, 37)) as s(p,q,r)
order by a+1 desc

Has (1,4,37) as the first row, because 37 is the highest value for the third column, even though you might think that a should refer to the first column, and so we should order by the successor of the first column.

And if you really want to order by a constant expression, you can, because SQL allows you to order by subqueries, so you can 'order by (select 1 + 1)'. I assume you just get an arbitrary order in that case.

Isn't that great?

I and other people have written about related stuff before, but some time ago I realized an amusing crystalization that I haven't seen explicitly written up anywhere. So here it is.

I usually tell people that 'finally tagless' stuff is Church/Boehm-Berarducci encoding.* To define μF, you use ∀r. (F r -> r) -> r. However, the details of the approach (in the papers I've read) are somewhat tailored to be nice in Haskell. For one, without extensions, that quantified type isn't first-class, so you only implicitly program with it by writing polymorphic functions.

More importantly, the (F r -> r) algebra portion is represented by type classes. This nicely affords extensible data types. Adding constructors corresponds to taking coproducts F + G, but the algebras of these coproducts can be represented by products of algebras. Classes are really nice here, because they can represent the product of a set of (named) algebras, so you don't have to keep track of the order your constructors come in, and can't include the same constructors twice.

When encoding higher-order things, r gets parameterized, so you end up with types like `(C1 r, C2 r, ...) => r T`. You can even encode GADTs this way, by having the algebra methods in Cn have more specific types for the arguments to r.

Now, another big trend among Haskell/functional programmers is extensible, algebraic effect systems. For these, we have a set of algebraic effect specifications, and work with the free monad over those specifications. So, what happens if we apply the 'finally tagless' approach to this?

What you get is essentially the mtl. Every class like MonadState has methods that are what you'd get if you pushed the algebraic effect specifications through to the finally tagless approach. And the above mentioned row-like (commutative and idempotent) behavior of class constraints in the finally tagless approach gives you all the nice 'extensible' aspects.

The mismatch in the mtl is that many of the classes contain non-algebraic components. For instance, throw is algebraic, but catch is not. These don't really hurt much for most purposes (and might be convenient sometimes); but strictly speaking its something of a mismatch.

If you want to do algebraic effect style handlers, what this corresponds to is choosing a transformer to fill one of the constraints. If I have a (MonadState s m, MonadError e m) context, I can use `ExceptT e n` to handle the exceptions, and push the context down to (MonadState s n). Not all constraints have to be discharged at once (although that is the common way people use the library).

So, if you combine a couple of the trendiest things these days, what you get is something that has been in use for decades. :)

[*] For people who know more category theory than type theory folklore for some reason, Boehm-Berarducci encoding basically goes like this: imagine if one of your type-forming principles were, "any end formula I can write down exists by fiat." Then you get all kinds of right Kan extensions, and any time you want to define a 'free' thing, you just used the fact that `Ran U 1 ⊣ U`, and your ability to write down a formula for the left adjoint.

I've been trying out the dedicated YouTube music app on Android recently, and it's incredible how worthless it is. It's almost universally inferior to the normal YouTube app at its intended domain.

It can play music in the background, but so can the normal app. It can't create or edit playlists, you need to switch the normal app for that. And when you do have a playlist, the music app will often judge that some of the entries aren't music, and omit them, so you can't use it for playback, either. The only thing it does that is unique is play random sequences of songs related to a video you pick.

I'm not sure I've ever seen something like this, where a dedicated application is almost strictly inferior to the more general version by the same company in (essentially) every way.

I was talking recently with someone about his idea for tweaking things about file handles. I could only think of one minor annoyance with the idea, and I noted that it would probably be a pretty moot point if you were using a copy-on-write filesystem (which are increasingly popular), and if they actually presented an interface that exposed the underlying immutability, which they don't.

But some time after, I realized the story is even more ridiculous than I had first thought, because SSDs are taking over long term storage these days. And mutation is not a great operation on them either. So the hardware is already doing something more like allocating modified values and garbage collecting, and only presenting mutation as an interface to that.

Then on top of the immutable disks presenting a mutable interface, people write immutable filesystems that present a mutable interface, and only use the underlying immutability for some extra features, like snapshotting.

Then, within the immutable filesystem presenting a mutable interface, people use version control systems, which are higher level immutable filesystems. But the feature everyone is obsessed with in these is the ability to appear to mutate the immutable structures, even though it's really a mutable-appearing view to an immutable structure with garbage collection.

Something to think about next time you hear a Real Programmer tell you that mutation is, "how things really work."

Post has attachment
Someone mentioned to me after I wrote the adjoint triples blog post that the colim ⊣ const ⊣ lim triple can actually be seen as part of the cohesion adjoint quadruple, where the quadruple would have a right adjoint to lim (I think).

So, I fooled around, and figured out that the analogue of that triple in Haskell (or really, a total version thereof) actually extends into an adjoint quintuple, with a right adjoint to lim (forall) and a left adjoint to colim (exists). At least, it works for the co- and contravariant endofunctor cases---I didn't bother thinking about quantifying over higher-kinded types and whatnot.

Post has attachment
Fun with adjoint triples and the (co-)Yoneda lemma.

Post has attachment
I haven't bothered reading up on 5th edition D&D, so I don't know how good or bad it's supposed to be. But I imagine it's a bad sign that they're reprinting 2nd edition.
Photo
Wait while more posts are being loaded