This is my log for December Adventure. I don’t have a clear plan for the contents, we’ll see where it goes :)

The December Adventure is low key. The goal is to write a little bit of code every day in December.
–– Eli Mellen

Dec 01

I did a handful of things today. Not a lot of coding, mostly uni work.

Set the blog up and replaced my old simple placeholder site. I’m using zola with Duckquill which I found very pretty. I stumbled into a fair bit of issues with nothing working in the beginning with a blank zola project, setting some post metas and blog extras did the trick.

Today was mostly writing the technical report for ComRaTT which is a part of a preliminary research project I’m working on with my mate kaep. The project is a compiled functional language that borrows the type system of Async RaTT which our supervisor(s) created. I wrote a couple of typst helper methods to help make the paper a little prettier and consistent. Mostly helper methods like

#let modality_circle(symbol) = {
  let circle-size = 1em
  let text-size = 0.9em
  circle(height:circle-size, stroke: 0.5pt)

  place(center+horizon, dx: -circle-size/2)[
    #set align(center+horizon)
    #set text(size: text-size)
    #box(width: text-size, height: text-size)[$symbol$]
  ]
}

#let mod_exists = modality_circle($exists$)
#let mod_forall = modality_circle($forall$)

#let turns = symbol(
  "⊢",
  ("double", "⊨"),
  ("triple", "⫢")
)

#let darrow = math.arrow.b.double

Typst is such a nice break from LaTeX.

I’ve been holding off working on the correctness proof of a primitive, verified compiler in Idris for a couple of days (not related to above). Hopefully holding back will bring out some ideas to crack the problem once I find time to look at it. Idris is pretty cool! We are basing this work on “functional pearls”

Functional pearls are elegant, instructive examples of functional programming. They are supposed to be fun, and they teach important programming techniques and fundamental design principles [..]

Specifically we’re translating “A type-correct, stack-safe, provably correct, expression compiler in Epigram” into Idris and adding exceptions and let bindings. May show some of that in the coming days.

Rest of the evening will be spent with my lovely wife.

Dec 02

Got that correctness proof done! Very exciting. It got a little long, so I’ll rather just link to the commit.

It’s very messy and Idris1 isn’t the best at error messages so I ported to Idris2 and backported once it worked – though both versions are more or less the same.

I also wanted to do something less mind straining, so I did AoC day 1 in Idris2 too

import Data.String

part1 : List (Integer, Integer) -> Integer
part1 loc =
  let (left, right) = unzip loc
      sortedPairs = zip (sort left) (sort right) in
   sum . map (abs . uncurry (-)) $ sortedPairs

part2 : List (Integer, Integer) -> Integer
part2 locs =
    let (left, right) = unzip locs in
    sum $ map (\l => l * cast (count_x l right)) left
    where
      count_x : (Eq t, Foldable m) => t -> m t -> Nat
      count_x v = count (== v)

parse : String -> List (Integer, Integer)
parse = map parseLine . lines
  where
    parseLine str = case words str of
      [l, r] => (cast l, cast r)
      _ => (0, 0)


readInput : IO (List String)
readInput = case !getLine of
  "" => pure []
  line => pure (line :: !readInput)

main : IO ()
main =
  let input = !readInput
      pairs = parse (unlines input)
  in do
    putStrLn $ "Part 1: " ++ show (part1 pairs)
    putStrLn $ "Part 2: " ++ show (part2 pairs)

I especially enjoy the !-notation which acts similar to an inline do-block. It’s syntax sugar that roughly provides (!) : m a -> a. It reminds me of the new ! and ? suffix in Roc. I think it’s a great way to make code more readable and is advantageous over the old backpassing syntax we had before.

That’s all for today. I didn’t want to do much more coding after all that Idris stuff :’)

Dec 03

Didn’t do a lot today. I updated my nix config a little after updating my flake lock.

I also followed along the API Authentication guide for Phoenix Framework’s mix phx.gen.auth. Was really easy to get working. Not really sure what to do with it though. I have a little playground project going that I want to do some exploration/learning with. Mostly learning about effective domain design and rapid prototyping with LiveView. No code to show though.