• 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" (https://pdfs.semanticscholar.org/1407/220ca09070233dca256433430d29e5321dc2.pdf) 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

  • Let's do Chapter 7 of Bartosz Milewski's Category Theory for Programmers
    So far we've talked about the structure *in* categories. What about structure *between* categories? Functors tell us how to get from one category to another, or, in the case of endofunctors, from a category to itself. In a programming language, an endofunctor manifests as a type-level function (or, depending on the language, something that just looks like a function), which takes a type as an argument and returns a type. You are probably familiar with a number of useful endofunctors, even if you haven't been calling them that. Let's read the chapter and do the exercises, then get together for our usual lively and occasionally on-topic discussion. We'll try to get properly underway around 6:15.


    160 Spear St., Ste. #1700 · San Francisco, CA