My Premonition

Last summer I got the opportunity to work briefly with Conal Elliott in Belgium. The two weeks I spent there are still making an impact on me; immediately I resonated with his semantic design idea. But the more important ideas were the ones I picked up subconsciously, and I’m just now becoming able [...]

The role of a core calculus

A lot of software engineering can be described as the art of skillful procrastination. When we’re designing some software, we would like to put off as many decisions as possible as long as possible, while still making progress toward the goal. This procrastination leads to good abstraction, because any code we wrote before [...]

Recursive Types in IΞ

In the last IΞ post, I introduced the calculus and sketched the construction of some standard mathematical objects. In this post, I will dive a little deeper and construct of all the positive recursive types. The proof will be in an informal style (in particular, omitting the H constraints), but I have [...]

It is never safe to cheat

Anyone who has spent time trying to implement an FRP library knows the unsafePerformIO story. You may use unsafePerformIO as long as you ensure that the result maintains purely functional semantics. It’s possible to create impure values with unsafePerformIO. It is up to you to “prove” that you have created a pure [...]