colimiting case

Hello there!

I'm Soham Chowdhury, a functional programmer interested in compilers, programming-language theory, and expressive type systems.

I'm also a student of mathematics interested in algebraic and arithmetic geometry and in number theory; a self-taught guitarist (and nearly omnivorous consumer of music); a fan of a lot of good writing; an occasional speedcuber; and an enthusiast for unexplained analogies in and around mathematics, physics, and computer science.

This is my personal site and blog.


Real-world type theory I: untyped normalisation by evaluation for ╬╗-calculus
February 1, 2020



A near-complete implementation of the Sound and Complete type system from Dunfield and Krishnaswami (2016), which describes a minimal ML-like language with GADTs, existential types, and coverage-checked pattern-matching.


A set of Nix scripts for reproducible, predictable Haskell development environments supporting custom package-sets and native dependencies.


A numeric programming framework for Haskell featuring highly polymorphic algebraic structures and custom deriving strategies to build complex algebraic behaviors from simpler ones.

Notes and short proofs of concept

Greatest hits from around the web