This is my first post about Lean on this blog :) It is meant as a response to Joachim’s post about extrinsic termination proofs. I want to show how a slight modification of his idea can be used to define partial function definitions using well-founded recursion.

Denotational semantics assign meaning to a program (e.g., in untyped lambda calculus) by mapping the program into a self-contained domain model in some meta language (e.g., Scott domains). Traditionally, what is complicated about denotational semantics is not so much the function that defines them; rather it is to find a sound mathematical definition of the semantic domain, and a general methodology of doing so that scales to recursive types and hence general recursion, global mutable state, exceptions and concurrency12. In this post, I discuss a related issue: I argue that traditional Scott/Strachey denotational semantics are partial (in a precise sense), which means that It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and Internal details of the semantic domain inhibit high-level, equational reasonining about programs After exemplifying the problem, I will discuss total denotational semantics as a viable alternative, and how to define one using guarded recursion.

Welcome back! At the end of part 1 from December 41, I made a promise to implement a strictness analysis à la GHC with you. Why would this be useful? In the last post, I argued that a rough understanding of how strictness analysis works helps to debug and identify the actual causes of missed unboxing opportunities and fix them with minimal effort. So here it is, enjoy!

Non-strict languages like Haskell often require the programmer to reason about strictness to achieve good performance. A while ago, Michael Snoyman wrote a blog post about this, giving an introduction on the matter as well as an overview over the tools at our disposal. In this post, I want to offer another, more surgical approach to plugging space leaks that works hand in hand with optimizations carried out by the compiler.

As Hakylls FAQ points out, in order to have source code highlighting for your blog, you need appropriate CSS markup. It would be convenient if one could choose from the wealth of themes out there, but the existing pygments styles don’t seem to work any longer.