The Unclear Impact

When giving examples, we will sometimes assume multiple concrete base types like N or B for instance,
as it is entirely moral to do so.

Categorizing types as "moral" or not is really funny

When I grow up I want to be an immoral type

idk why but gradual typing papers are nice to read
Compared to when I was trying to read about guarded types or parametricity it's like ahh... a nice calm paper about very nice things

I guess I've only read 2.25 gradual typing papers. It might just as well be that all of the authors of these three papers happened to be good writers

oh I love this colour notation for compilation

[[_]] : ℒs → ℒt, but the ℒs and inner brackets are in blue, and the ℒt and outer brackets are in red

ddg​ Galois connection

Image of a rubber duck with a purple wizard's hat and an association football. Left pointing arrow with a small Greek letter gamma above and a right pointing arrow with a small Greek letter alpha underneath. Image of a rubber duck with long brown hair and a hockey stick.