Free Monads: from the basics to the implementation of composable and effectful stream processing

In the previous post, we introduced IdrisPipes, a library for composable and effectful production, transformation and consumption of streams of data in Idris. We talked about the motivations behind this library, its API and its model, and some of the features it offers. In this post, we will embark in a journey from the basics... Continue Reading →

IdrisPipes: a library for composable and effectful stream processing in Idris

We will continue our series on post on Idris, by implementing a pipe library for Idris, inspired by the great Haskell pipes and Haskell conduit libraries. The goal is to provide Idris with a library for composable and effectful production, transformation and consumption of streams of data. In short, IdrisPipes is an Idris package that... Continue Reading →

Why template parameters of dependent type names cannot be deduced, and what to do about it

Following the presentation a type by any other name at the CppCon, a great talk that shows how to incrementally refactor code using tooling and type aliases, I got interested in one of the observation made by Jon Cohen: template parameters of dependent type names cannot be deduced. This short post aims at describing this... Continue Reading →

My CppCon 2017 Trip Report – 10 great talks to watch and learn from

The last edition of the CppCon 2017 just ended. As for the previous edition, it was a real pleasure to be there, discussing with talented and curious fellow developers, and watching great talks. In particular, I got the feel that the conference offered more diverse talks than the previous edition. Inspired by the trip report... Continue Reading →

Transforming data structures into types: an introduction to dependent typing and its benefits

The 1.0.0 of Idris has been released just a few months back, just enough to start trying out the language and some of the possibilities dependent typing offers. Back in July, we implemented a type safe bowling kata in which we could not create a bowling game that would not satisfy the rules of the... Continue Reading →

Monoids: what they are, why they are useful, and what they teach us about software

Monoids are a pretty interesting concept in software development. Monoids are everywhere. Monoids are simple yet powerful. And Monoids have a lot to teach us about software, in particular about composition and building powerful abstraction. This post will take you through a small tour of what Monoids are and are for. We will first define... Continue Reading →

Create a website or blog at

Up ↑

%d bloggers like this: