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 data-type that made it explicit. The idiom … Continue reading

Posted in Computers | Tagged , , | Leave a comment

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

Posted in Computers | Tagged | Leave a comment

An Interesting CPP Bug

The C preprocessor, being a dumb text-manipulating tool that does not understand the syntactic structure of the underlying program, is often a hiding place for subtle headache-inducing bugs. I’ve been bitten such bugs myself and one bug I had a … Continue reading

Posted in Computers | Tagged , , , | 3 Comments

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

Posted in Computers | Tagged , | 6 Comments

Type-Safe Tic-tac-toe

I recently had occasion to screw around Haskell’s type system. The end goal was to produce a Tic-tac-toe game in which all type-correct moves are legal and where all illegal moves produce type errors. I decided call the following moves … Continue reading

Posted in Computers | Tagged , , | Leave a comment

[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 well-typed expression eventually reduces to a value. The proof is quite clever and that the … Continue reading

Posted in Computers, Rest | Tagged , , , | 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

Posted in Computers | Tagged , , , | 2 Comments

Macros In Haskell

Haskell too has macros. The subsystem is called Template Haskell. It is a Lisp-like 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

Posted in Computers | Tagged , , , | 6 Comments

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

Posted in Computers | Tagged , | Leave a comment

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

Posted in Computers | Tagged , , , , , | 1 Comment