Moonside

Moonside OP wrote

I was mostly joking, but I'm halfway done with the 1st of these books. It's definitely laborious, but interesting. It seems like things are faraway from production and changing pretty fast in that space. Some others: Agda, Idris, ATS (this seems scary). The most impressive Coq project I've seen is this C compiler: http://compcert.inria.fr .

Btw, juggling with proofs is very video game like though, I played with them too late into the night. That constant feedback! The triumph of writing Qed.

2

Moonside OP wrote

I'm doing it in Python and following ~TDD~

Reimplement in Coq and automatically derive it from specification. Actually I've tried to learn proper testing habits in Haskell, but I think that I don't even have a specification atm so yeah haha.

Godot looks pretty good.

I've been meaning to look at the Postmill source code and learn about that too

Me too! I've been itching to Fix a thing or two there.

3

Moonside OP wrote

Arbitrary precision integer arithmetic is just a mouthful for what is in Python long and in Java BigInteger. Just integers that go arbitrarily big in absolute value. I literally had to google for the official name!

It might be that I don't understand enough about the music theory behind it, but why don't you trust ints? Is that distrust just for this application, or more general?

It was a bit of hyperbole, it's mostly that I've gotten a bit bored with the tricks we have to do in software to make things palatable for computers, instead of doing the most straightforwardly correct thing at first and then making it hairy in the name of efficiency. It's like we have a computer brain or binary fog or what you call it!

The big problem was representing notes so that they have correct letter names, the correct amount of accidentals and octave; this is enough to name them correctly and also play the pitch. I wrote convoluted and buggy versions of this, so I was motivated to do it Right. The original version was just storing these directly, but calculating intervals between them was convoluted, but I noticed that each note is some distance (interval) away from middle C. Notes can be represented as rewrapped intervals.

I represented intervals as pairs of integers (I can distinguish between augmented fourths and diminished fifths that way). I defined addition and inverse on them so it turns out that they are isomorphic to the additive group of integer points on a XY-plane, or Z². And as notes are just intervals from middle C in disguise, naming all of them correctly is easy since the bookkeeping is done by underlying presentation. It's about ten lines of code and half of that are signatures.

So it was just an easy thing to do, because the innermost representation really is infinite in two directions. That said, it doesn't matter much, because the largest integer is 9223372036854775807 and basically for my purposes about 1000 is enough, without doing a bunch of renormalizations.

3

Moonside OP wrote

Reply to comment by musou in Computers are bad by Moonside

Linux audio feels like Mordor, I wonder how people ever dare to venture into it. Which is kinda sad, broke musicians could definitely benefit if Linux audio was great.

2

Moonside OP wrote

this sounds really neat! i love making music and i also love haskell (although i am only a hobbyist at either one).

It's nice to see another person in this intersection of interests, I wouldn't have guessed! I'm not a career programmer by any means, so Haskell is a hobby for me too.

have you picked a web framework yet? i've seen a few for haskell but haven't tried any.

No I haven't and this has been a point of procrastination for me. I think I should pick one, make something that outputs on the page the same [e♭,F,g,b♭,e♭,c,e♭,b,E,d] kinda string as my current program does, and refreshes it every time you click a button. Pimintel's app isn't much more fancy than that in the big picture, after all.

A problem is that there are lots of choices, but the situation keeps developing so I can't what's good. Year old blog posts are outdated at this point afaik.

3

Moonside wrote

I have a simpler scheme that probably didn't get read by anyone (hyperbole), because I posted it so late. Justifications, a bit outdated since this is a living site, in original comment: https://www.jstpst.net/f/meta/28/comment/248

  • Arts and entertainment: killallgames, anime4unme, post_music, itookthisphoto, imadethis, just_drawe, Yuri_hut. This could also be named Arts and media.
  • General: general, just_post, ask.

or the former split in two:

  • Crafts and creative pursuits: itookthisphoto, imadethis, just_drawe and (maybe) just_eate. (I'm not entirely sold on the name.)
  • Arts and entertainment: killallgames, anime4unme, post_music, Yuri_hut.

I think these cover your 01 - Main, Doing Things, Learning Things, Media Arts in a better way than your categories.

Also, media arts aren't all arts, I think that Arts and Entertainment is strictly superior replacement for Media arts since not all arts are media arts.

Otherwise, I think that Learning Things and Sharing Things are both premature at this point of time and too vague. And in my book me_irl is memery that ought to go with Sharing Things things, the format is restricted enough not to warrant being in general category.

Politics, tech and support are great categories.

Last thing: I think that arbitrary 01 sorting is bad and shouldn't be done. I'm sure the postmill person could implement sorting by subscribers if we ask nice enough and when there are less than 20 categories, they're all visible enough.

1

Moonside OP wrote (edited )

I suppose it's going to be a bit ironic that I'm kinda announcing my own project to the world here, which isn't as cozy and low stakes I meant this thread to be, but ahem. Feel free to crib my format (introduction, project now, its future, conclusion) if you want to, it helped to make this comment better.

My project

I'm creating an app to generate random notes, chords and scales for musical practice. The closest thing I've found is Bret Pimintel's random note web app, which I recommend you to try out right this second. I'm also using the occasion as an excuse to learn Haskell.

To those not in the know, things that sound exactly the same on when played on the piano may not be the same always. Piano tuning is a compromise and thus augmented seconds and minor thirds sound exactly the same. But when sung, they sound distinct. Theory reflects this too, which matters when you need to name and notate notes. I did some research on how others deal with these issues in web apps and dare I say: badly or hardly not at all. Bret Pimentel has the nicest system, but I'm not sure whether it's extensible beyond it's original purpose. This is where my project comes in.

Where's my project currently

Modelling music theory is essentially complete, but the app lives on the command line without a graphical UI. There are also no options to make drills nor does it care about user input. If I run the program in terminal, it will generate ten random minor or major keys

[g,d,b,B♭,b♭,f♯,d♯,G♭,G♭,g]

where lowercase letter are minor keys, uppercase ones a major keys. It's not obvious from the output, but the program can handle arbitrarily many accidentals with ease, like C𝄪𝄪𝄪𝄪𝄪𝄪𝄪♯, which in a silly way has 15 sharps and corresponds to the C♯/D♭ key on the piano. It's a side-effect of having a principled system. I don't need to deal with special cases, so even ludicrously unlikely cases get treated correctly.

For the nerds in audience, think of it as arbitrary precision integer arithmetic vs using ints. I don't trust ints and dealing with special cases here. Performance doesn't matter, thus the high road is the easiest road.

Where's my project going

The next step is learning to create a web app using Haskell. I've never created a web app before and I'm not exactly sure which way I should go. Ideally something that lives 100% in the browser would be neat, I don't want to create a service that handles user data and log ins and shit. It would be nice updating could be just as easy as uploading some compiled html file and letting users refresh the site.

Conclusion

Somewhere in February I'll publish a pastiche of Pimentel's app. It should be the most principled web app of its kind available, even if not overly ambitious otherwise. Because of its principled modelling of music theory, it should be easy to extend so it could be more than that and I don't have to fight ad hoc logic to implement it. It will probably look like ass at first as I'm not a web designer.

5

Moonside wrote

I'm a bit skeptical myself whether it's really worth it. It's roughly double the effort, but for what gain? For something tutorial like or educational I can see the benefits (well-managed group work is usually beneficial), but the way pair programming discussed is, like, always evidence free, seemingly reflecting aesthetic preference or social style more than anything. Which is not to poopoo either of those completely, it's just rather a beginning than a conclusion.

3