Programming for a culture approaching singularity
In 2001, Ray Kurzweil published his inspiring, controversial essay The Law of Accelerating Returns. I acknowledge that the essay sometimes seems far-fetched, and perhaps some details are overly (or underly) idealistic, but in essence I find it very convincing. I will take it as an assumption for this article, and I also assume my readers [...]
Life and Projects
I just lost my job. This happening was unexpected except to the deep knowledge of my subconscious, who, for the last week, has been practicing what to say when it happened. The reason is that my “level of productivity is not sufficiently high to justify [my] contract rate”. I agree with this, and although the [...]
Reflections on a Holy Grail (FRP)
It has been two years, twenty-six days, six hours, twenty-four minutes and thirty seconds since my eyes caught the first glimpse of my mistress, functional reactive programming. Her simplicity, beauty, and power has captivated me since, but she has teased me — all of us lonely fools, really — by slipping through my fingers every [...]
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 to put [...]
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 we made [...]
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 little doubt that [...]
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 one. Seems like [...]
Dana (actual) progress
I have some very exciting news! I wrote some actual code in the Dana repository. It is the IΞ Certificate module. That is, it’s an abstract data type Proof, such that only valid proofs in IΞ can be constructed. The certificate module (IXi.Term and IXi.Proof together) is about 280 lines, which isn’t fantastically small, but [...]
Some Constructions in IΞ
Over the past couple months, I have been attempting to find a language to use as a core calculus for Dana, as anyone who follows this blog knows. I have been slowly converging on IΞ for its elegance and simplicity. It turns out to be very powerful, capable of modeling many structures while avoiding many [...]
Might as well face it, I’m addicted to logic
I’m trying really hard not to become a logician. Like my obsession with FRP, it would be very interesting and educational. But my FRP fancy came from a desire to make games more easily, and I have since lost interest in that endeavor, studying FRP for its own sake. Now I am trying to change [...]
Recent Comments