
Recent Posts
Recent Comments
sanjoyd on Faking Dependent Types in… drocta on Faking Dependent Types in… Matt on Faking Dependent Types in… Francis Kim on Faking Dependent Types in… Anurag Bishnoi on On why religion is a double… Archives
Categories
Meta
Category Archives: Computers
First steps with Agda: provable factoring
In my last post we looked at the problem of factoring an integer. We ran into an issue with the termination checker and resolved it by wrapping the recursion into a separate inductive datatype that made it explicit. The idiom … Continue reading
First steps with Agda: well founded recursion
Last week I finally got time to explore Agda in some detail; something I had on my list for a while. Agda is a dependently typed programming language. That means in Agda you can have a function of the type … Continue reading
An Interesting CPP Bug
The C preprocessor, being a dumb textmanipulating tool that does not understand the syntactic structure of the underlying program, is often a hiding place for subtle headacheinducing bugs. I’ve been bitten such bugs myself and one bug I had a … Continue reading
Faking Dependent Types in C++
It is possible to have some kind of dependent typing in C++ using templates. The “solution” isn’t elegant or usable, but I found it mildly interesting so I’ll try to explain it here. The C++ type system with templates is … Continue reading
TypeSafe Tictactoe
I recently had occasion to screw around Haskell’s type system. The end goal was to produce a Tictactoe game in which all typecorrect moves are legal and where all illegal moves produce type errors. I decided call the following moves … Continue reading
[Proof] λ→ is normalizing
I studied a proof today that I had been putting off for some time now; that a simply typed lambda calculus is normalizing — every welltyped expression eventually reduces to a value. The proof is quite clever and that the … Continue reading
Posted in Computers, Rest
Tagged math, programming language theory, programming languages, types
Leave a comment
New JIT Interface for GDB
I worked on GDB as a part of my internship at Igalia. The work I did is finally merged, and this blog post describes the problem that I tried to solve and the solution I implemented. The Problem Let’s say … Continue reading
Macros In Haskell
Haskell too has macros. The subsystem is called Template Haskell. It is a Lisplike AST generation framework that comes as a GHC extension (that is, it isn’t a part of the language as of now). This blog post is a … Continue reading
Threading A Graph
One operation that moving garbage collectors (among other things) have to concern themselves with is updating of references. Once you move object X from position P0 to P1, you’ll also need to update all references to X accordingly. To be … Continue reading
Tree Traversal in O(1) Space
I’ve been reading some texts recently, and came across a very interesting way to traverse a graph, called pointer reversal. The idea is this — instead of maintaining an explicit stack (of the places you’ve visited), you try to store … Continue reading