Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity
Completing every advent of code problem in Idris 2 for fun and profit
78 commits 3 branches 0 tags 1.2 MiB
Raku 100%
Find a file
Nathan McCarty f675677a76 Fix build-book output directory
2025-01-29 03:35:21 -05:00
scripts Fix build-book output directory 2025-01-29 03:35:21 -05:00
src Year 2015 Day 13 Part 2 2025-01-29 03:32:22 -05:00
.gitignore mdbook setup 2025-01-27 01:38:09 -05:00
advent.ipkg Add JSON Parser 2025-01-27 05:10:11 -05:00
book.toml Some notes 2025-01-27 17:06:08 -05:00
pack.toml Initial commit 2025-01-04 09:48:10 -05:00
README.md Year 2015 Day 13 Part 1 2025-01-29 02:55:12 -05:00

README.md

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

References