Mikrokosmos

Hello there!

I'm Soham Chowdhury, a student of mathematics learning to coherently speak algebraic number theory and (eventually) arithmetic geometry.

I'm also a functional programmer interested in programming-language theory and expressive type systems; a self-taught guitarist and musician interested in counterpoint and fugal writing; a fan of a lot of music and writing; and an enthusiast for unexplained analogies in and around mathematics.

I'm interested in and like discussing a variety of things, including literature, music (theory), physics, philosophy, and cognitive science.

This is my personal site and blog, named after the Béla Bartók work.

Projects

preposterous

A work-in-progress implementation of the OutsideIn(X) type inference engine of Vytinotis, Peyton Jones, Schrijvers, Sulzmann (2010), used in the Glasgow Haskell Compiler.

sound-and-complete

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.

rien

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

noether

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

Drafts

Learning the Bound library
January 6, 2018

Notes and short proofs of concept

Greatest hits from around the web