Blog about Haskell, programming lanugage semantics, theory and implementation
Propositions as types never troubled me: a proposition is a type, a proof a term of it, the Curry-Howard correspondence. In Agda, a total language, it is the whole point; in Haskell it is more slogan than tool, scary to newcomers and pointless to practitioners, since the language is partial and undefined proves anything. The nimbus around it never reaches the subtle part: Lean’s separate sort Prop…
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. Background: structural vs. well-founded recursion Many recursive function definitions terminate on all inputs by an inductive argument.…
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…
Welcome back! At the end of part 1 from December 4 1 , 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! Since this is a literate…
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…
As Hakyll s 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. That’s probably because pandoc has since deprecated highlighting-kate in favor of skylighting , which adopts a different CSS naming…