Post · Fedizen

@mcc@mastodon.social 7 days ago

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

@mcc@mastodon.social last yr.

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

@mcc@mastodon.social 2 yr. ago

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)

0 Boosts

0 Likes

@mcc@mastodon.social 7 days ago

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!

@vchakhno@mathstodon.xyz 6 days ago

@mcc Out of curiosity, what didn't you like about Haskell? I have recently learned it for real and started using it in actual projects – I had only used it for a few coding exercises a few years back – and it's been a delightful experience, but I'd like to hear complaints others might have.

@mcc@mastodon.social 6 days ago

@vchakhno I dunno, vibes just felt funny. Chunky, awkward syntax and the code and documentation all uses a b c d as variable names. Also to be clear the reason I did not like it between the years 2001 and 2025 was i couldn't frickin figure it out.

I posted my diary of learning Haskell last year here: https://mastodon.social/@mcc/114433465965880352

@vchakhno@mathstodon.xyz 6 days ago

@mcc I can't really speak for the syntax, seems at its core like lambda calculus + pattern matching + let and where + do notation. I'm familiar with those so that's OK. Not sure how close it maps to ML. Not a fan of the slight differences between case and pattern matching. Multiline sometimes doesn't do what I would like.

I wish there was a dup operator (W combinator), basicly (\f x -> f x x). Somehow every other combinator of BCKW has their own.
I like how operators have slight variations for ease of use. <=<, <$, <*, *> ...

If you're not familiar with using Functors and Applicatives I suggest taking a look at "Learn you a Haskell for great good" which is a free website that's usually recommended to learn Haskell. That's the one I recently learned from, and enjoyed the whole way. It explains them with tons of examples, it makes them really intuitive.
But maybe you've been trough this already

I feel like the single letter variable names have their meaning either in their type, or in the algebraic structure they're part of. If you don't know the structure already you're fucked, good luck going from the laws to the use cases...

Personally I've been looking specifically for books and blog posts about common patterns in haskell in order to learn about those structures.
One such example are optics, I haven't seen them yet but they're on my list, and I have a rough idea what Lens/Prisms are for thanks to previous exposure.

Uh. Sorry for the text dump. I'm low on sleep. I hope it's informative somehow.

@tkalvas@mastodontti.fi 6 days ago

@mcc I definitely think the awkwardness of Haskell is incompleteness, not a bug. I've tried to work on it for years, but I'm getting to be resigned to being not smart enough to make real progress at it. Specifically, I think the monad business is going at it the wrong way. You can express all that as effect types and get it completely out of the algorithmic syntax and into the type syntax, where you can use inference and type definitions to package it arbitrarily nicely.

@mcc@mastodon.social 6 days ago

@tkalvas I'd definitely like to understand applicatives and I'd definitely like to understand Effects.

If I am already doing a survey of functional languages, which language would you recommend looking at if I want to experience effects done right?

@tkalvas@mastodontti.fi 5 days ago

@mcc Koka, definitely. It's a bit experimental, I wouldn't try to support a production system with it, but it is very nice as a design and programming ergonomics. Although the exact same could be said of Unison.

1 more reply

@mcc@mastodon.social 7 days ago

Inconveniently the Haskell package manager doesn't fricking work.

What… I don't understand what this very long error message is telling me. Do I need to upgrade Cabal? Do I need to downgrade Cabal? Is some existing package I have selected in a version incompatible with Idris? I can literally blow away my entire set of installed Haskell packages, I don't mind. Would that help? :(

EDIT: A six year old Google Groups comment reveals the secret is to pass cabal the flag "--allow-newer". Terrifying

An INCREDIBLY long cabal "Could not resolve dependencies" error message

mirek kratochvil

@exa@mastodon.online 6 days ago

@mcc this looks like idris package is declaring incompatibility with newer versions of cabal (which you seem to have installed), might be useful to ping them to bump their versions

(this is annoyingly common with "latest" haskell tooling versions)

@mcc@mastodon.social 6 days ago

@exa if u look down thread I did a force bump and it's not just declared incompatible it's actually incompatible. And they're unlikely to fix it because they've deprecated Idris 1 and moved entirely to Idris 2 which is no longer Haskell based.

@ionchy@types.pl 7 days ago

@mcc noooo don't install Idris thru Cabal, use the Idris package manager https://github.com/stefan-hoeck/idris2-pack/blob/main/INSTALL.md

idris2-pack/INSTALL.md at main · stefan-hoeck/idris2-pack

Contribute to stefan-hoeck/idris2-pack development by creating an account on GitHub.

@mcc@mastodon.social 7 days ago

@ionchy it appears you can install idris 1 through cabal but *not* idris 2, furthermore it appears idris 1 no longer works.

@mcc@mastodon.social 7 days ago

Cont'd
- Passing --allow-newer fails *worse*—well, I turned the safety off
- I read the tutorial closer. It links a github
- The github is archived.
- I back ALL the way out. Instead of searching "idris tutorial" I go to the Idris home page. I then discover
- I have been looking at the Idris 1 tutorial. Idris 1 is discontinued. New thing is Idris 2.
- Idris has a totally different tutorial and is now deployed via Racket instead of Haskell (?!??)
- I have been, apparently, barking up a dead tree.

Failed to build cheapskate-0.1.1.2 (which is required by idris-1.3.4). See the build log above for details.

@mcc@mastodon.social 7 days ago

So.

I install Racket. Wow! Racket takes up a lot of space! I guess I'll need this for week 14 anyway.

I install "pack", Idris's dedicated package manager. I guess I don't get to be happy Idris uses an existing package manager anymore. Installation for the Idris package manager is "curl to bash". The bash script clones a git repo. There is weeping and gnashing of teeth. There is no way I will remember to uninstall this thing or remove it from my bashrc files when this project's done. Whatever.

Text over the Idris package manager installing 177/289 packages:

Wow, this is pretty slow. Is this compiling native binaries? If so, does that mean it only needed Racket as a bootloader, not a host, and maybe I should have installed the presumably slimmer "Chez Scheme"? Also if you're already running a bash script why can't you just write a scheme interpreter in Bash. it can't be that hard — Text over the Idris package manager installing 177/289 packages: Wow, this is pretty slow. Is this compiling native binaries? If so, does that mean it only needed Racket as a bootloader, not a host, and maybe I should have installed the presumably slimmer "Chez Scheme"? Also if you're already running a bash script why can't you just write a scheme interpreter in Bash. it can't be that hard

6+ more replies

@mcc@mastodon.social 7 days ago

Anyway! Idris! I'm in!

Idris is a "dependent types" language. "Dependent types" are the thing your favorite language doesn't have that prevents you from having that feature you wished it had but it doesn't. A running gag in Rust is every desirable but missing feature would be possible with dependent types. DT means a type can contain a value, or do ops on values, for example a function that adds an array of length N to an array of length M and produces an array M+N. Like Ada, but… … … better?

@mcc@mastodon.social 7 days ago

For some reason Idris has two tutorials.

https://idris2.readthedocs.io/en/latest/tutorial/index.html
https://idris-community.github.io/idris2-tutorial/

Reading how they describe their types, I wonder if the CPU emulator puzzle was the wrong choice for this language. Something with arrays might've better exercised Idris' capabilities?

First thing that catches my eye: it has an "infix" sugar like ML. But then they say:

"Functions, data constructors, and type constructors may all be given infix operators as names."

TYPE CONSTRUCTORS MAY BE INFIX

HECK YES

A Crash Course in Idris 2 — Idris 2.0 Documentation

@mcc@mastodon.social 6 days ago

Unsorted thoughts

"Holes are useful." is a funny sentence to see in a manual

"where" and "let" seem redundant

> Nested record fields can be accessed using the dot notation:
>
> x.a.b.c
> map (.a.b.c) xs

…Haha heck nice, that was the feature I was proudest of in Emily

"multiplicity 0" (calculated/erased at compile time) and "multiplicity 1" (linear typing) sound like things I VERY MUCH want in a programming language, though the ergonomics around it are a little alien to me, a C/Rust girl

@mcc@mastodon.social 6 days ago

Okay important question

I have a vague sense Haskell has "monads" and Idris has "applicatives". Idris in fact seems to have both— https://idris2.readthedocs.io/en/latest/tutorial/interfaces.html#idiom-brackets

If I say "do" I've made a monad and if I say "[| … |]" (ugh, ocaml at its worst) that's an applicative. Difference isn't clear. If I just write monads and ignore [||] in my learning-Idris program am I Missing Out?

I still don't know what an Effect is. I thought it was the Effect Monad but the Idris manual talks like applicatives are Effects.

Interfaces — Idris 2.0 Documentation

@mcc@mastodon.social 6 days ago

Okay so the important things seem to be this comment

https://social.treehouse.systems/@dysfun/117441025783295712

the second screenshot (the terminal shot) attached to this post

and this comment

https://mastodon.social/@porglezomp/117441075637749928

I still don't understand it, but I think I'm closer to understanding it than I have been ever in the last 25 years. Just gotta think about those type signatures. And in the meantime I don't *have* to understand it, I can just use do notation and worry later about which Math Things my code corresponds to.

3 media files

@dysfun@treehouse.systems

haskell and idris both have both

your three fundamental typeclasses for effectful stuff are functor, applicative and monad.

functor: map (<$>)
applicative: apply (<*>)
monad: bind (>>=). — @dysfun@treehouse.systems haskell and idris both have both your three fundamental typeclasses for effectful stuff are functor, applicative and monad. functor: map (<$>) applicative: apply (<*>) monad: bind (>>=).

terminal screenshot

Main> :t (<$>)
Prelude.(<$>) : Functor f => (a -> b) -> f a -> f b
Main> :t (>>=)
Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
Main> :t (<*>)
Prelude.(<*>) : Applicative f => f (a -> b) -> f a -> f b — terminal screenshot Main> :t (<$>) Prelude.(<$>) : Functor f => (a -> b) -> f a -> f b Main> :t (>>=) Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b Main> :t (<*>) Prelude.(<*>) : Applicative f => f (a -> b) -> f a -> f b

@porglezomp@mastodon.social

the real difference between Idris and Haskell here is just that Functor <= Applicative <= Monad, whereas in Haskell at least one of those relations is missing. So in Idris you can just go up each level when you need more operations and you don’t have to rewrite anything to adapt it. — @porglezomp@mastodon.social the real difference between Idris and Haskell here is just that Functor <= Applicative <= Monad, whereas in Haskell at least one of those relations is missing. So in Idris you can just go up each level when you need more operations and you don’t have to rewrite anything to adapt it.

@mcc@mastodon.social 6 days ago

Among the things not mentioned in either Idris tutorial

- What file extension is used for Idris files? (it's .idr)

- How do you execute an idris file?

Running idris2 puts you at a REPL. Running "idris2 src/puzzle.idr" churns a long time, creates a series of utterly baffling files in a build/ subdirectory, then drops you at the same repl. "-c" does this then quits; but it still does nothing useful.

One tutorial implies "pack -o hello exec src/puzzle.idr" will do something; this hangs forever

@mcc@mastodon.social 6 days ago

I understand true LISP heads are comfortable just spending all their time in a REPL forever. I am not a true LISP head. I'm an ocaml poser.

I *think* the mysterious "pack" command, while hanging, created in the mysterious "build" subdirectory a "hello.rkt" file that wouldn't have been there otherwise. I remember someone saying idris works by transpiling itself to a "backend" lang, so maybe I'm supposed to figure out the non-hanging args to "pack", transpile, then execute the rkt file in racket.

@mcc@mastodon.social 6 days ago

*Rubbing eyes* okay, so

idris2's command line --help lists a "-o <file>" flag, which "specifies output file". Output file for what? Apparently this actually means "build an executable, put it in ./build/exec [path non-negotiable], and name it <file>".

I run this. I run it in `time`. It does create a runnable Linux executable.

It takes it one minute and fifty-three seconds to compile the program:

main : IO ()
main = putStrLn "Help"

During which time I sincerely could not tell if it had hung

@ShadSterling@mastodon.social 7 days ago

@mcc “I have been, apparently, barking up a dead tree”

moood

@lritter@mastodon.gamedev.place 7 days ago

@mcc have you talked to @dysfun yet who is deep into idris by now

1+ more replies