Advent

The goal of this project is to get all 500 currently available stars in the form of one single Idris application, and thoroughly document the results as literate Idris files.

Authors Note

This entire book is a single literate code base, the source code is available at https://git.stranger.systems/Idris/advent.

The solutions contained in this project are intended to be read in sequential order, though can reasonably be read in any order if you have a good level of familiarity with more advanced functional programming topics.

The solutions will involve progressively more advanced topics as day and year number increase, though I try not to introduce too much within the scope of any one day.

Suggestions and other feedback are highly welcome, please reach out to me via any platform you know me on, or send an email to the ~thatonelutenist/public-inbox mailing list on source hut.

While this project is intended to read more like a book, while it is still a work in progress, you can follow its development as a psuedo-blog by subscribing to the rss feed for the repository in your feed reader: https://git.stranger.systems/Idris/advent.rss.

Index of non-day modules

• Runner

  Provides data structures for structuring the division of the project into years, days, and parts.

• Main

Provides the Runner based command line interface for running a selected day's solution.

• Util

  Provides extensions of the functionality of the standard library and external libraries. Extensions to the standard library are in the base of this module.

  • Util.Eff

    Extend the functionality of the effects included in the eff library

  • Util.Digits

    Provide views that enable recursively pattern matching numbers as lists of digits, in both ascending and descending order of significance.

• Array

  Provider wrappers over the standard library IOArray type to make them more ergonomic to use.

• Parser

  Effectful parser mini-library

  • Interface

    Effectful parser API

  • ParserState

    Internal state of a parser

  • Numbers

    Parsers for numerical values in multiple bases

  • JSON

  JSON Parser

Index of years and days

• 2015

  • Day 1

    Warm up problem, breaks in our new runner and not much else interesting.

  • Day 2

    An early hint of effectful parsing.

  • Day 3

    Peculiarities of writing mutually recursive functions in dependently typed languages.

  • Day 4

    Basic FFI to openssl to steal its MD5 function for Idris's use.

  • Day 5

    First introduction to views and dependent pattern matching¹.

  • Day 6

    Naive approach to handling the first 2d grid problem.

  • Day 7

    Introduces dependent maps and indexed type families.

  • Day 8

    Proper effectful parsers and non-determinism in effect stacks.

  • Day 9

    Naive approach to handling the first graph traversal problem.

  • Day 10

    Introduce our Digits, dependent pattern matching on integers as lists of digits.

  • Day 11

    Introduces refinement types

  • Day 12

    New Parser Effect stack and DLists

  • Day 13

    Naive ring buffer and parameters blocks²

  • Day 14

    Introduction to streams, infinite collections of data

  • Day 15

    Introduction to barbies, types that can change their close, through their use to implement the builder pattern

  • Day 16

    Manual refining of types and default implicit arguments

  • Day 17

    $BLURB

References

---

1. Idris 2 Manual: Views and the "with" rule ↩︎

2. https://idris2.readthedocs.io/en/latest/tutorial/modules.html#parameterised-blocks-parameters-blocks ↩︎