This page gives access to main projects I participated in during the last years.
Idris Pipes (Idris open source library)
IdrisPipes is a library for library for composable and effectful production, transformation and consumption of streams of data in Idris. It is inspired from Pipes and Conduit Haskell libraries, and is available at QuentinDuval/IdrisPipes.
In short, IdrisPipes is an Idris package that aims at providing the means to write:
- Effectful programs, with side effects such as IO
- Over a stream of data, potentially infinite
- Efficiently, by streaming data and controlling memory consumption
- In a composable way, allowing problem decomposition and reuse
The package description and motivation are introduced in this blog post. This should help you understand what pipes are about and how to use them.
Idris Reducers (Idris open source library)
Idris reducers is a library for lazy transformation pipe in Idris, inspired from Clojure transducers, available at QuentinDuval/IdrisReducers. Its goal is to provide transformation of accumulating functions that:
- Can be composed together as pipe-lines of transformations
- Do not suffer from the overhead of creating intermediary lists
- Can support arbitrary inner state (for non trivial transformations)
The main concepts and their associated types are introduced in this blog post. This should help you understand what transducers are and how to build you own.
Tiny Rand (C++ open source library)
Tiny rand is a small header-only library which helps generating random instances of composite objects in C++, available at QuentinDuval/tiny_rand. It builds on the STL random header to generate any kind of STL data structures:
- Primitives: int, double, strings, …
- Containers: vector, list, maps, sets, …
- Product types: tuples, and custom struct or classes
- Sum types: variants, optionals, …
The rationale and design choices are available in this blog post.
Fully type-safe Bowling Kata (Idris)
A type safety challenge in Idris, based on the Bowling Kata (http://codingdojo.org/kata/Bowling/) but adding enough type level invariants to make sure we cannot instantiate invalid games.
Can you make sure a bowling game can only be instantiated if it represent a valid game? The solution is available at QuentinDuval/IdrisBowlingKata and explained in this blog post.
Tribolo (Game in Clojurescript)
Three players (Blue, Red and Green) play one after the other on board made of 16 times 11 cells. Each player tries to convert the maximum number of cells to their own color. A player can convert cells of another player by “jumping” over them.
- To play the game
- Check the code on GitHub
The game is implemented in Clojurescript. If you desire to know how to build such a game, you can check the series of post dedicated to it.
Tic Tac Toe (Game in Clojurescript)
Two players (Cross and Circle) play one after the other on board made of 3 times 3 cells. Each player tries to convert cells to form a line, column or diagonal.
- To play the game
- Check the code on GitHub
- The Devoxx 2017 slides (in french)
- The Live coding at DevoxxFR 2017 (in french)
The game is implemented in Clojurescript. If you desire to know how to build such a game, you can check the post dedicated to it.
Deque 