## Classical Axioms in Coq

For the past few days I’ve been working through an amazing text, Software Foundations, which aims to develop “basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant”. This post is an … Continue reading

## Typechecking TAL0 in Agda.

This post is an annotated solution to problem 4.2.11 in the book Advanced Topics in Types and Programming Languages from the chapter Typed Assembly Language by Gerg Morrisett. Introducing TAL0 I’ll do my best to give an informal introduction to … Continue reading

## Initial Algebras: Part II

In the last post we looked at functor algebras and properties of morphisms (arrows) between them. In this post we’ll explore initial functor algebras (or initial F-Algebras). The Cliffhanger The last episode ended with a question on whether it is … Continue reading

## Initial Algebras: Part I

Meta-post This post is light on math and uses Haskell to express formalisms. If you’re clear on what a Functor is, you’re good to go. Functors and Algebras There is this regular old functor, with the type constructor Func. We’ve … Continue reading

Posted in Computers | | 6 Comments

## Logic Puzzles in Agda

This post assumes basic knowledge of Agda. A few days ago, Paul Snively published a post which set me thinking on how Agda (which is the closest thing to Coq I have some knowledge of) fares in similar scenarios. Pretty … Continue reading

## 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

## 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

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 | | 6 Comments

About this post This is one of those posts I write to ensure I actually understand a concept. Read at your own peril. Some knowledge of Haskell is required. The Problem One Hello World problem that is sometimes used to … Continue reading

Posted in Computers | | 9 Comments

I’ve been studying Haskell for a while now, and in the past few months I’ve gone from “Monads are impure” to “all Haskell functors are endofunctors” and “join f = f >>= id“. Some small things I noticed during this … Continue reading

Posted in Computers | Tagged | 5 Comments