I’ve known for a while that dependent types can be defined as initial and final dialgebras. This is a somewhat obscure fact; but an important generalization of the more commonly referenced fact that non-dependent types are initial and final (co)algebras of specific endofunctors. The only thorough source of this fact... [Read More]

In this post, I will show a nice, clean, organized, schematic, and theoretically well-justified approach to sorting. I’ll implement it in Python because of my target audience, but there’s no significance to the choice beyond that. I’m going to describe and implement Merge Sort and Quicksort via hylomorphisms. That may... [Read More]

This post consists of some notes on lambda encodings I made a while ago. I figured I’d put them here, since it’s more visible and easier for me to find. [Read More]

I read a rather fascinating paper recently called “Implicative algebras: a new foundation for realizability and forcing”. I thought this was a good paper, and I need content for this blog, so I figure giving a summary of it would be a good idea. [Read More]