Articles on functional programming, PLT, types, and other geekery
Posted on October 12, 2015 Tags: sml In this post I’d just like to walk through some fun code, nothing particularly theory-y. The code I’d like to go through is a simple little module in ML that lets you easily construct “dynamic” types. This isn’t through the usual “really big sum of products” approach but instead is completely open and can be extended for every new defined type (at runtime). The…
Posted on September 27, 2015 Tags: types So summer seems to be about over. I’m very happy with mine, I learned quite a lot. In particular over the last few months I’ve been reading and fiddling with a different kind of type theory than I was used to: computational type theory. This is the type theory that underlies Nuprl (or JonPRL cough cough). One thing that stood out to me was that you could do…
Posted on August 26, 2015 Tags: jonprl , types , haskell I was reading a recent proposal to merge types and kinds in Haskell to start the transition to dependently typed Haskell. One thing that caught my eye as I was reading it was that this proposal adds * :: * to the type system. This is of some significance because it means that once this is fully realized, Haskell will be inconsistent (as a…
Posted on August 14, 2015 Tags: types I wanted to write about something related to all the stuff I’ve been reading for research lately. I decided to talk about a super cool trick in a field called domain theory. It’s a method of generating a solution to a large class of recursive equations. In order to go through this idea we’ve got some background to cover. I wanted to make this post readable…
Posted on August 14, 2015 Tags: types I’ve been trying to write a blog post to this effect for a while now, hopefully this one will stick. I intend for this to be a bit more open-ended than most of my other posts, if you’re interested in seeing the updated version look here . Pull requests/issues are more than welcome on the repository. I hope you learn something from this. Lots of people seem…
Posted on July 17, 2015 Tags: jonprl So as a follow up to my prior tutorial on JonPRL I wanted to demonstrate a nice example of JonPRL being used to prove something Interesting Unreasonably difficult in Agda or the like I think I’m asking to be shown up when I say stuff like this… I would like to implement the conatural numbers in JonPRL but without a notion of general coinductive or even…
Posted on July 6, 2015 Tags: jonprl , types JonPRL switched to ASCII syntax so I’ve updated this post accordingly I was just over at OPLSS for the last two weeks. While there I finally met Jon Sterling in person. What was particularly fun is that for that last few months he’s been creating a proof assistant called JonPRL in the spirit of Nuprl. As it turns out, it’s quite a fun project to work on…
Posted on June 29, 2015 Tags: twelf , types Veering wildly onto the theory side compared to my last post, I’d like to look at some more Twelf code today. Specifically, I’d like to prove a fun theorem called cut admissibility (or elimination) for a particular logic: a simple intuitionistic propositional sequent calculus. I chucked the code for this over here . Background If those words didn’t make…
Posted on June 1, 2015 Tags: haskell It’s been a while since I did one of these “read a package and write about it” posts. Part of this is that it turns out that most software is awful and writing about code I read just makes me grumpy. However I found something nice to write about! In this post I’d like to close a somewhat embarrassing gap in my knowledge: we’re going to walk through streaming…
Posted on May 19, 2015 Tags: compilers , haskell I’m a fan of articles like this one which set out to explain a really complicated subject in 600 words or less. I wanted to write one with a similar goal for compiling a language like Haskell. To help with this I’ve broken down what most compilers for a lazy language do into 5 different phases and spent 200 words explaining how they work. This isn’t…
Posted on May 5, 2015 Tags: twelf , types An important property in any term rewriting system, a system of rules for saying one term can be rewritten into another, is called confluence. In a term rewriting system more than one rule may apply at a time, confluence states that it doesn’t matter in what order we apply these rules. In other words, there’s some sort of diamond property in our system…
Posted on May 1, 2015 Tags: types , haskell It’s well known that lambda calculus is an extremely small, Turing Complete language. In fact, most programming languages over the last 5 years have grown some (typed and or broken) embedding of lambda calculus with aptly named lambdas. This is wonderful and everything but lambda calculus is actually a little complicated. It’s centred around binding and…
Posted on April 30, 2015 Tags: compilers , haskell Hello folks. It’s been a busy month so I haven’t had much a chance to write but I think now’s a good time to talk about another compiler related subject: continuation passing style conversion. When you’re compiling a functional languages (in a sane way) your compiler mostly consists of phases which run over the AST and simplify it. For example in…
Posted on April 24, 2015 Tags: sml , haskell Inspired by ezyang’s OCaml for Haskellers I decided to write something similar for SML. If you already know OCaml I also recommend Adam Chlipala’s guide I’ll follow mostly the same structure as Edward’s article so we’ll have {- Haskell -} (* SML *) What Do They Have in Common SML and Haskell have quite a lot in common Common types: () | Int | Integer |…
Posted on March 27, 2015 Tags: sml , haskell I’m taking the undergraduate course on programming languages at CMU. For the record, I still get really excited about the novelty of taking a class (at school!) on programming languages. I’m easily made happy. We started talking about System F and before long we touched on the value restriction. Specifically, how most people think of the value…
Posted on March 24, 2015 Tags: compilers , types , haskell Hi folks, the last week or so I was a little tired of schoolwork so I decided to scratch out some fun code. The end result is an extremely small compiler for a typed, higher order functional language called PCF to C. In this post I’ll explain attempt to explain the whole thing, from front to back :) What’s PCF First things first, it’s…
Posted on March 7, 2015 Tags: twelf , types In this post I wanted to focus on one particular thing in Twelf: %worlds declarations. They seems to be the most mysterious. I’ve had a couple people tell me that they just blindly stick %worlds () (x _ _ _) before every total and pray which is a little concerning.. In this post hopefully we’ll remove some of the “compile-n-pray” from using Twelf code.…
Posted on February 28, 2015 Tags: sml , haskell , types A couple of days ago I wrote a small implementation of a type inferencer for a mini ML language. It turns out there are very few explanations of how to do this properly and the ones that exist tend to be the really naive, super exponential algorithm. I wrote the algorithm in SML but nothing should be unfamiliar to the average Haskeller. Type…
Posted on February 28, 2015 Tags: twelf , types For the last 3 or so weeks I’ve been writing a bunch of Twelf code for my research (hence my flat-lined github punch card). Since it’s actually a lot of fun I thought I’d share a bit about Twelf. What Is Twelf Since Twelf isn’t a terribly well known language it’s worth stating what exactly it is we’re talking about. Twelf is a proof assistant. It’s…
Posted on February 11, 2015 Tags: types I write a lot about types. Up until now however, I’ve only made passing references to the thing I’ve actually been studying in most of my free time lately: proof theory. Now I have a good reason for this: the proof theory I’m interested in is undeniably intertwined with type theory and computer science as a whole. In fact, you occasionally see someone draw…
Posted on January 27, 2015 Tags: haskell , types For those who haven’t heard, GHC 7.10 is making a brave foray into the exciting world of distributed computing. To this end, it’s made a new language extension called -XStaticPointers to support Cloud Haskell in a pleasant, first class manner. If you haven’t heard of static pointers before now, it’s worth glancing through the nice tutorial from…
Posted on January 9, 2015 Tags: types Continuing on my quest of writing about my poorly thought out comments, let’s talk about constructive logic. A lot of people in and around the Haskell/FP community will make statements like The Curry-Howard isomorphism means that you’re proving things in constructive logic. Usually absent from these remarks is a nice explanation of why constructive logic…
Posted on January 8, 2015 Tags: sml , haskell I was having lunch with a couple of Haskell programmers the other day and the subject of the ML family came up. I’ve been writing a lot of ML lately and mentioned that I thought *ML was well worth learning for the average Haskeller. When pressed why the best answer I could come up with was “Well.. clean language, Oh! And an awesome module system” which…
Posted on December 27, 2014 Tags: haskell In keeping with the rest of the “Examining Hackage” series I’d like to go through the source folds package today. We’ll try to go through most of the code in an attempt to understand what exactly folds does and how it does it. To be honest, I hadn’t actually heard of this one until someone mentioned it to me on /r/haskell but it looks pretty cool. It also…
Posted on December 25, 2014 Tags: haskell In this installment of “jozefg is confused by other people’s code” we turn to operational . This is a package that’s a little less known than I’d like. It provides a monad for transforming an ADT of instructions, a monad that can be used with do notation and separates out interpretation. Most people familiar with free monads are wondering what the…
Posted on December 23, 2014 Tags: haskell , types So the results from Stephen’s poll are in! Surprisingly, impredicative types topped out the list of type system extensions people want to talk about so I figured I can get the ball rolling. First things first, all the Haskell code will need the magical incantation {-# LANGUAGE ImpredicativeTypes #-} What Is Impredicative Polymorphism We have a lot…
Posted on December 22, 2014 Tags: types , notes I like types. If you haven’t figured this out from my blog I really don’t know where you’ve been looking :) If you’ve ever talked to me in real life about why I like types, chances are I mentioned ease of reasoning and correctness. Instead of showing how to prove parametricity I’d like to show how to rigorously apply parametricity. So we’ll be a step…
Posted on December 19, 2014 Tags: haskell , types Proving things about programs is quite hard. In order to make it simpler, we often lie a bit. We do this quite a lot in Haskell when we say things like “assuming everything terminates” or “for all sane values”. Most of the time, this is alright. We sometimes need to leave the universe of terminating things, though, whenever we want to prove things…
Posted on December 17, 2014 Tags: haskell , compilers After my last post, I didn’t quite feel like ending there. I was a little dissatisfied with how binding was handled in the type checker, the odd blend of HOAS, GUIDs, and DeBruijn variables was… unique. In the post I explore 3 versions of the same code The original method Using bound to handle all binding Full HOAS There’s a lot of code in this…
Posted on November 26, 2014 Tags: haskell It’s been a while since I posted about some code I’ve been reading, but today I found a little gem: concurrent-supply . This package sets out to provide fast way to generate unique identifiers in a way that’s splittable and supports concurrency. What’s particularly cool about this package is that the code is only about ~100 lines and a goodly chunk of that…
Posted on November 22, 2014 Tags: haskell , types , compilers This week I learned that my clever trick for writing a type checker actually has a proper name: bidirectional type checking. In this post I’ll explain what exactly that is and we’ll use it to write a few fun type checkers. First of all, let’s talk about one of the fundamental conflicts when designing a statically typed language: how…
Posted on November 19, 2014 Tags: haskell One of the common pieces of folklore in the functional programming community is how one can cleanly formulate recursive types with category theory. Indeed, using a few simple notions we can build a coherent enough explanation to derive some concrete benefits. In this post I’ll outline how one thinks of recursive types and then we’ll discuss some of the…
Posted on October 28, 2014 Tags: haskell , c It’s fairly well known that Haskell is a bit um.. different from how stock hardware sees the world. I’m not aware of too many processors that have decided that immutability and higher order functions are the right way to go. Compiling Haskell and its ilk, however, does have one interesting wrinkle on top of the normal problem: laziness. Laziness stands…
Posted on October 27, 2014 Tags: types , notes I’ve been spending a lot of time whacking my head on focusing literature. I’d like to jot down some intuition around what a focused system is and how it relates to the rest of the world. I’m going to steer clear of actually proving things but I will point out where a proof would be needed. What Is Focusing In a nutshell, focusing is a strategy to…
Posted on October 24, 2014 Tags: haskell , personal All though most people I talk to know me for my blog, I do occasionally actually write software instead of just talking about it :) Sadly, as a mercurial user most of my stuff has languished with on bitbucket. I’ve had a few people tell me that this is annoying for various reasons. Yesterday, I finally got around to fixing that! As of yesterday,…
Posted on October 17, 2014 Tags: types , notes Lately I’ve been reading a lot of type theory literature. In effort to help my future self, I’m going to jot down a few thoughts on quotient types, the subject of some recent google-fu. But Why! The problem quotient types are aimed at solving is actually a very common one. I’m sure at some point or another you’ve used a piece of data you’ve wanted to…
Posted on September 29, 2014 Tags: haskell , types , notes I’m part of a paper reading club at CMU. Last week we talked about a classic paper, Abstract Types have Existential Type . The concept described in this paper is interesting and straightforward. Sadly some of the notions and comparisons made in the paper are starting to show their age. I thought it might be fun to give a tldr using…
Posted on September 21, 2014 Tags: agda , types First, an apology. Sorry this has take so long to push out. I’ve just started my first semester at Carnegie Mellon. I fully intend to keep blogging, but it’s taken a little while to get my feet under me. Happy readings :) In this second post of my “intro to dependent types” series we’re going on a whirlwind tour of Agda. Specifically we’re going to…
Posted on August 25, 2014 Tags: haskell , types I’d like to start another series of blog posts. This time on something that I’ve wanted to write about for a while, dependent types. There’s a noticeable lack of accessible materials introducing dependent types at a high level aimed at functional programmers. That’s what this series sets out help fill. Therefore, if you’re a Haskell programmer and…
Posted on August 6, 2014 Tags: types Equality seems like one of the simplest things to talk about in a theorem prover. After all, the notion of equality is something any small child can intuitively grasp. The sad bit is, while it’s quite easy to hand-wave about, how equality is formalized seems to be a rather complex topic. In this post I’m going to attempt to cover a few of the main different…
Posted on July 30, 2014 Tags: types I’m going to a take a quick break from arguing with people on the internet to talk about a common point of confusion with theorem provers. People will often state things like “A program in Coq never diverges” or that “we must prove that X halts”. To an outsider, that sounds impossible! After all, isn’t the halting problem undecidable? Now the thing to realize is…
Posted on July 19, 2014 Tags: haskell , types I’ve written a few times about church representations, but never aimed at someone who’d never heard of what a church representation is. In fact, it doesn’t really seem like too many people have! In this post I’d like to fix that :) What is a Church Representation Simply put, a church representation (CR) is a way of representing a piece of concrete data…
Posted on July 15, 2014 Tags: haskell I had a few people tell me after my last post that they would enjoy a write up on reading extensible-effects so here goes. I’m going to document my process of reading through and understanding how extensible-effects is implemented. Since this is a fairly large library (about 1k) of code, we’re not going over all of it. Rather we’re just reviewing the core…
Posted on July 10, 2014 Tags: haskell One of my oldest habits with programming is reading other people’s code. I’ve been doing it almost since I started programming. For the last two years that habit has been focused on Hackage. Today I was reading the source code to the “logic programming monad” provided by logict and wanted to blog about how I go about reading new Haskell code. This time the…
Posted on July 9, 2014 Tags: coq , types For almost a year and half now I’ve been referencing one particular book on Coq, Certified Programming with Dependent Types . CPDT is a literate program on building practical things with Coq. One of the main ideas of CPDT is that proofs ought to be fully automated. This means that a proof should be primarily a logic program (Ltac) which constructs some…
Posted on June 28, 2014 Tags: agda , types I’ve been using Agda for a few months now. I’ve always meant to figure out how it handles IO but never have. Today I decided to change that! So off I went to the related Agda wiki page . So hello world in Agda apparently looks like this open import IO main = run ( putStrLn "test" ) The first time I tried running this I got an error about an IO.FFI , if…
Posted on June 23, 2014 Tags: teaching This last week I’ve been volunteering at a summer camp. This camp is aimed at kids ages 8 to 12 and teaches the basics of Python! I wanted to write down some of my thoughts and experiences on the whole process. The Curriculum The curriculum for the camp was based around 3 key components Python Raspberry Pis Minecraft The camp was spread over 4 days, each 3…
Posted on June 14, 2014 Tags: haskell In this post I’d like to talk about the second half of recusion-schemes. Previously we’d talked about catamorphisms and friends. These all focused on “destroying” a datastructure by collapsing it layer by layer. We’re now going to talk about the opposite: anamorphisms. Anamorphisms are just like generalized versions of unfoldr . Getting Anamorphisms To…
Posted on June 7, 2014 Tags: haskell , compilers For the last few months I’ve been spending a fair amount of time on a fun little Scheme to C compiler, c_of_scheme . In this post I’ll outline the high level overview of c_of_scheme and in future posts detail the specifics of each component. Modules c_of_scheme is divided into 11 modules: 2 utility modules, 6 modules which each handle one step of…
Posted on May 19, 2014 Tags: haskell This post is a little different than the rest of my blog, I’m not nearly as competent with recursion-schemes as I want to be and I don’t understand them fully (yet). This isn’t entirely complete, but I hope it will provide a useful intuition for how to work with some of the lower ends of recursion-schemes and some idea of how to get into the higher end. I’ll be…