Completing every advent of code problem in Idris 2 for fun and profit
Find a file
Nathan McCarty 4d8ad3a12d
Some checks failed
/ build-docker (push) Has been cancelled
/ build-push-book (push) Failing after 28s
CI first pass
2025-07-27 02:16:02 -04:00
.forgejo/workflows CI first pass 2025-07-27 02:16:02 -04:00
ci Setup docker container for CI use 2025-07-27 01:22:50 -04:00
scripts new-day script 2025-03-17 02:25:00 -04:00
src Stub out day 17 2025-07-27 01:58:32 -04:00
templates new-day script 2025-03-17 02:25:00 -04:00
.gitignore mdbook setup 2025-01-27 01:38:09 -05:00
advent.ipkg Year 2015 Day 15 Part 1 No Prose 2025-03-18 01:54:02 -04:00
book.toml Some notes 2025-01-27 17:06:08 -05:00
pack.toml Cleanup 2025-07-27 01:16:00 -04:00
README.md Stub out day 17 2025-07-27 01:58:32 -04:00

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

    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 matching1.

    • 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 blocks2

    • 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