Next Meetup

Let's read Edwin Brady's paper describing how Idris is put together
We've finally finished the Idris book. Go us! Now let's look at what we learned from a different point of view. Edwin Brady's 2013 paper "Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation" ( describes how the Idris we know and love (well, sort of) is compiled into a simpler language, TT. If you're interested in the theoretical properties of Idris, what you really want to look at is the properties of TT. The paper is a bit out of date -- the section on tactics, for example, is no longer of interest -- but the bulk of it is probably still helpful to anyone who wants a better understanding of Idris, or who is interested in learning to build a dependently typed language on top of a well-understood core language. Let's read the paper, then get together to discuss it, along with anything else that comes to mind.


360 3rd Street Suite 675 · San Francisco, CA


What we're about

Have you been writing software for a while and now want to go deeper into the philosophy and mechanics of programming languages? Have you been hearing about things like automated theorem proving, hybrid type checking, gradual types, and wondering whether you'll be finding them soon in mainstream programming languages? Are you interested out-of-the-mainstream programming language paradigms like logic programming? Have you heard mathematical-sounding terms like lambda calculus and pi calculus, and wondering whether understanding them will make you a better programmer? If so, welcome.

We're focused less on spreading the gospel of functional programming (although we assume you know something about it) than on figuring out what makes programming languages of any paradigm expressive and reliable. And we try to take a more concrete approach than category theory's high-level overview of programming language structures, coming up with code we can execute and tools we can use.

Members (1,052)

Photos (7)