#BabelOfCode 2024
Week 11, Puzzle 17
Language: Idris
PREV WEEK: https://mastodon.social/@mcc/114582208242623432
RULES: https://mastodon.social/@mcc/113676228091546556
PUZZLE TEXT: https://adventofcode.com/2024/day/17
Now getting extreme with "puzzles out of order". Here's the problem. The AOC author *really* likes puzzles involving 2D arrays. It makes sense. They're easy to visualize as either ASCII art or PNGs. They're a rich space for "simulations". But some languages are better at them than others.
So for Idris week, I pick the "build a CPU" puzzle.
#BabelOfCode 2024
Week 10, Puzzle 11
Language: Textual Wasm
Confidence level: Medium high
PREV WEEK: https://mastodon.social/@mcc/114524697727786286
NEXT: https://mastodon.social/@mcc/117436256447438940
I'm now doing the puzzles slightly out of order.
"Wasm" is a bytecode VM that runs in web browsers as an alternative to JavaScript. Oddly for a modern VM, it's designed to be targeted by C.
A thing I've heard repeatedly claimed, both excitedly & with eyerolls, is that Wasm's human readable form is "a LISP". I want to know what that means.
I was too busy to do AOC this month (that's https://adventofcode.com/).
So I'm thinking I'm going to do AOC 2024, *in 2025*, under the following rules:
- One challenge per week.
- I don't have to perform a challenge every week. The goal is to finish by the start of December.
- I have to do a different programming language every time.
- C, C++ and Objective-C are not eligible languages.
- If I make an honest attempt at a language and fail, I may retry in Go (but only Go) (I need to learn Go)
![import System
main : IO ()
main = do
case getArgs of
[x] => arg <- x
_ => impossible
putStrLn arg
=> is highlighted
"expected => or impossible"](https://files.mastodon.social/media_attachments/files/117/442/839/477/338/475/original/e2497ab429548f6f.png)
![import System
main : IO ()
main = do
args <- getArgs
arg <- (case args of
[_,x] => pure x
_ => die "Wrong number of arguments")
putStrLn arg
-- This compiles and works as expected
-- (If run with 1 command line arg echoes it, otherwise errors)](https://files.mastodon.social/media_attachments/files/117/446/951/183/546/858/original/fbf02393d8ff9b8f.png)
![import System
main : IO ()
main = do
arg <- (case getArgs of
[_,x] => pure x
_ => die "Wrong number of arguments")
putStrLn arg
-- Error: While processing right hand side of main. Can't infer type for case scrutinee
--
-- src.puzzle:5:10--7:39
-- 5 | arg <- (case getArgs of
-- 6 | [_,x] => pure x
-- 7 | _ => die "Wrong number of arguments")
--
-- Warning: compiling hole Main.main
--
-- Okay so admittedly sometimes Rust also has this problem but](https://files.mastodon.social/media_attachments/files/117/446/955/146/850/882/original/eae2ded182d465c8.png)
![import System
import System.File.ReadWrite
main : IO ()
main = do
args <- getArgs
arg <- case args of
[_,x] => pure x
_ => die "Wrong number of arguments"
spec <- readFile arg
spec <- case spec of
Left x => die "Can't open file" -- FileError
Right x => pure x -- String
putStrLn spec](https://files.mastodon.social/media_attachments/files/117/447/098/760/039/537/original/030ec3fa0e389656.png)
![import System
import System.File.ReadWrite
import Data.String
main : IO ()
main = do
args <- getArgs
arg <- case args of
[_,x] => pure x
_ => die "Wrong number of arguments"
spec <- readFile arg
spec <- case spec of
Left x => die(show x) -- FileError
Right x => pure x -- String
-- spec <- lines spec -- Commented out
putStrLn spec
-- This compiles and runs, it opens a file and prints the contents](https://files.mastodon.social/media_attachments/files/117/447/568/500/115/265/original/2b2488e4fdd49869.png)
![import System
import System.File.ReadWrite
import Data.String
main : IO ()
main = do
args <- getArgs
arg <- case args of
[_,x] => pure x
_ => die "Wrong number of arguments"
spec <- readFile arg
spec <- case spec of
Left x => die(show x) -- FileError
Right x => pure x -- String
spec <- lines spec -- Commented out
putStrLn spec
-- Uncommenting that one line results in:
--
-- Error: While processing right hand side of main. When unifying:
-- List ()
-- and:
-- IO ()
-- Mismatch between: List () and IO ().
--
-- src.puzzle:7:2--7:17
-- 3 | import Data.String
-- 4 |
-- 5 | main : IO ()
-- 6 | main = do
-- 7 | args <- getArgs
-- ^^^^^^^^^^^^^^^
--
-- Warning: compiling hole Main.main](https://files.mastodon.social/media_attachments/files/117/447/574/034/875/502/original/95c021f91a19d49f.png)
![$ idris2 -o puzzle src/puzzle.idr && ./build/exec/puzzle data.txt
Error: While processing right hand side of main. While processing right hand side
of main,interpret_register. Sorry, I can't find any elaboration which works. All errors:
If Data.String.(::): When unifying:
AsList (strCons ?_ ?str)
and:
String
Mismatch between: AsList (strCons ?_ ?str) and String.
src.puzzle:23:5--23:7
19 | interpret_register : String -> Int
20 | interpret_register line =
21 | let words = split (== ' ') line in
22 | case line of
23 | [_, _, i_string] => case parseInteger i_string of
^^](https://files.mastodon.social/media_attachments/files/117/447/960/674/564/841/original/04e76be3778dc36f.png)
, not :: . I literally assumed this was wrong. No, It was right.
Idris is "Haskell, but more so". Haskell is "ML, but more so". I have always liked ML. I have never liked Haskell (although when I tried it again for this thread series, I enjoyed it more than I expected). I have always suspected I might like Idris more than Haskell. Maybe the awkward concepts in Haskell aren't *awkward* just *incomplete*. Maybe another language could complete them.
Conveniently, Idris installs itself through the Haskell package manager, which I already installed for week 7!