Author Archives: sanjoyd

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

Movies to make you think, part II

Some less famous movies which I found nice (in no particular order): Waltz With Bashir Annie Hall (maybe not so exotic) Pan’s Labyrinth Teen Kanya (get a version with subtitles if you don’t speak bangla) (edit: to clarify, I’m talking … Continue reading

Posted in Rest | 4 Comments

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

TSA in the sky with diamonds

An anti-drug article [1] was written and published by some IIT Kharagpur students in one of our campus newspapers. I think the article is rubbish and here’s why. I think the article should, in principle, offend any self-respecting individual due … Continue reading

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

Books, movies and music

I graduated out of high school an idiot. I hadn’t read anything, seen anything or heard anything (Everybody anyone?). Now that I’m becoming moderately literate in such things, I think I can make a generalization — the information content (sorry … Continue reading

Posted in Rest | 1 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