Refining types

In dependently typed programming, I find it's common to start with some "imprecise" type and refine it to something that contains more information. For example, I »

Fixed points of GADTs

Consider a basic language containing integer and boolean literals along with addition. The first approach to modeling this language could be a type like the following: »

Why HoTT matters

Equality is one of the most fundamental concepts in mathematics. But what is it? This one rule: for all x, x = x. If you are familiar »

Theories and parsing

I've had a lot of opportunity to get some reading in while spending time in the beautiful Chania. One of the books I'm reading is Logic »

Encoding unfolds

Folds are a pretty big deal. I've written a lot about them in the past. One thing I haven't covered, however, is their sister: the unfold, »