Latest Posts

  • 5th May 2014

Category Theory proofs in Idris

Dependent types provide an unprecedented level of type safety. A quick example is a type-safe printf implementation. They are also useful for theorem proving. According to the Curry-Howard correspondence, mathematical propositions can be represented in a program as types. An implementation that satisfies a given type serves as a proof of the corresponding proposition. In other words, inhabited types represent true propositions.

Read more 
  • 4th November 2013

Functional data structures in JavaScript with Mori

I have a long-standing desire for a JavaScript library that provides good implementations of functional data structures. Recently I found Mori, and I think that it may be just the library that I have been looking for. Mori packages data structures from the Clojure standard library for use in JavaScript code. …

Read more 
  • 22nd May 2013

Functional Reactive Programming in JavaScript

I had a great time at NodePDX last week. There were many talks packed into a short span of time and I saw many exciting ideas presented. One topic that seemed particularly useful to me was Chris Meiklejohn’s talk on Functional Reactive Programming (FRP). …

Read more