Advent of Code 2022: Day 1

• The puzzle
• My solution

I tried using Idris to write this one. Some quick thoughts:

• I didn’t use dependent types at all — my solution would have been nearly identical in Haskell.
• The error messages from Idris were mostly unhelpful.
  • I often hit an error saying it couldn’t find an typeclass implementation for a variable I didn’t declare anywhere.
  • I needed more manual type annotations than I thought necessary — for example, {m = _ Error IO}.
  • The syntax for named implementations is not well-documented and it took a few tries to write it in a way that was accepted by the compiler and did the right thing.
• There is no equivalent to Hoogle, and in particular I needed to search the Idris github repo to find the Maximum instance for Semigroup, which doesn’t even appear in the rendered documentation.
• The rendered documentation would be more helpful if it linked to the source code, like Haddock does.
• I’m not sure my code is idiomatic Idris, if there is such a thing.

I don’t think I’ll use Idris for further tasks because its UX relies too heavily on the users knowing how the parser and compiler works.