darkkindness

Nice find!

Abstract:

> These notes were originally developed as lecture notes for a category theory course. They should be well-suited to anyone that wants to learn category theory from scratch and has a scientific mind. There is no need to know advanced mathematics, nor any of the disciplines where category theory is traditionally applied, such as algebraic geometry or theoretical computer science. The only knowledge that is assumed from the reader is linear algebra. All concepts are explained by giving concrete examples from different, non-specialized areas of mathematics (such as basic group theory, graph theory, and probability). Not every example is helpful for every reader, but hopefully every reader can find at least one helpful example per concept. The reader is encouraged to read all the examples, this way they may even learn something new about a different field.

> Particular emphasis is given to the Yoneda lemma and its significance, with both intuitive explanations, detailed proofs, and specific examples. Another common theme in these notes is the relationship between categories and directed multigraphs, which is treated in detail. From the applied point of view, this shows why categorical thinking can help whenever some process is taking place on a graph. Form the pure math point of view, this can be seen as the 1-dimensional first step into the theory of simplicial sets. Finally, monads and comonads are treated on an equal footing, differently to most literature in which comonads are often overlooked as "just the dual to monads". Theorems, interpretations and concrete examples are given for monads as well as for comonads.

pdf: https://arxiv.org/pdf/1912.10642

I tried running this a year ago and remember some things which stood out. But again, a year ago -- details are fuzzy, and likely outdated.

pros:

- The no-cost self-hosted setup was easy enough. I didn't have to jump through too many installation-debugging-hoops

- Could easily customize the UI with minimal CSS edits

- The app was pretty responsive in my view, and my view is that web apps are known for clunkiness

- All the things you could do within the app were pretty obvious from the interface ("no manual required")

cons:

- Honestly, the thing that killed it for me was being required to select Male or Female for every person entered. It was ridiculous, so they probably have removed any sex/gender field by now, right?

- To my knowledge it only had a web interface, so I couldn't open up and edit the data in a text editor (personal preference), for instance

Remarkable, I've also been learning J901 for AoC. I'm curious, what resources have you been using to learn?

I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types, which proves guarantees at compiler time. In this case, types are less about documentation, they are literally proofs of properties of the program by construction. In fact, type-level programming is usually unreadable[0] unless the reader has deep knowledge of the specific language implementation of type families, functional dependencies, poly-kinds, etc (whatever permits typelevel programming in that language).

I'm getting that the OP is arguing against these ad-hoc constructs (type families etc) and would much rather write these proofs in the same language as ordinary code (e.g. writing the law "List x where length(x) == 5" in the type rather than "forall a. List (S (S (S (S (S Z))))) a") which, well who can disagree?

In a sense, you and OP both agree on the same thing. Types are good. No types (or unreadable ad-hoc constructs for types) are not good.

[0]: https://aphyr.com/posts/342-typing-the-technical-interview uses type-level programming in Haskell to solve N-queens

That's interesting. Atom (last I checked) shows you profiling of how each package contributes to start-up time, and it's always been slow regardless. It seems like it's been consistently slow for 5.5 years now, which is unfortunate.

Start-up time was the number one reason I was not sold on the Luna language editor -- they were building it on top of Atom! (they are rebuilding it though, or maybe that is already done)

I'm a big fan of Alfred (https://www.alfredapp.com/) however the GUI automation feature called Workflows is paid.

The killer feature for me is being able to create global keybinds or custom Spotlight commands that can be linked control flow blocks to different drag-n-drop blocks of editable shell script / Applescript / Python / whatever. The keybinds themselves and everything else are drag-and-drop blocks, too. The edge over other keybinding software IMO is that you can define variables and do otherwise complex control flow within a workflow without being limited to "define a list of things to run". For example I could have a 'compile this' keybind that detects language, compiles, and displays stdout of whatever code I'm highlighting.

For Android I'm currently using Tasker, which is a "list of things to run" so it suffers from sometimes having to define multiple tasks for one command. But it's better than the drag-n-drop alternative (Automate), which doesn't allow arbitrary shell commands last I checked.

Just inject:

td:nth-child(3) > span.pagetop { color: transparent; }

Hides karma, leaves user and logout intact (as they're links)

The following paragraph is a good summary, I think:

> Anyone who cares about getting good grades has to play this game, or they'll be surpassed by those who do. And at elite universities, that means nearly everyone, since someone who didn't care about getting good grades probably wouldn't be there in the first place. The result is that students compete to maximize the difference between learning and getting good grades.

It's a race to the bottom.

Thanks!

> From the OOP perspective, though, monad is a pattern where you only have one behavior (bind) that you can customize, and you have to do everything through that one behavior. That looks like a straightjacket. Sure, it composes well, but... why limit yourself like that?

That's an excellent question. Thinking of monad as a pattern itself, with bind as its API, made me realize that OOP patterns (as a categorical concept) aren't the best analogy for the different behaviors monads encode, but rather monad is just one of the patterns. Makes sense -- there are obviously behaviors not generalized by monads but are in the realm of OOP patterns. For instance, the visitor pattern is covered by functors.

(At the time of writing I was thinking about how bind can relate seemingly disparate behaviors: error handling, async, state, etc. What other useful structures seem disparate? OOP patterns! And so I fell into the black pits of "Monads are just like <thing>" myself, where thing = OOP patterns.)

As for the question: One could call it a straightjacket but one could also call it "the law". Limiting yourself is exactly how Straightjacketed Sam can ensure correctness properties of the program. Monads force Sam to work within the monad, so they can only write "a depend on b" in a specific and well-defined way. This is analogous to how singleton pattern would force Sam to work with this one instance of an object, or how the factory/smart constructor pattern forces ensures only certain (valid) objects can exist. If any of these restrictions are too limiting, there's no need to use the patterns, but you'll also lose the laws (guarantees)!

> When playing AI Dungeon 2 the player can choose from several possible settings and characters. These choices generate a starting prompt and context sentence. The context sentence is always included as input to the model to help keep it grounded to the chosen setting while the starting prompt is the beginning of the story.... For each action you type the model is fed the context sentence as well as the past N action-result pairs in its memory to generate the result. We found N=8 to be a good amount of memory to feed the model.

from the blog post: https://pcc.cs.byu.edu/2019/11/21/ai-dungeon-2-creating-infi...

I always see monad tutorials like this conflate (1) "understanding using particular monads" with (2) "understanding using monads in general", which are completely different things. Luckily it's easy to not confuse those two with (3) "understanding monads abstractly" which tends to break out the category theory, but some tutorials like jumping on that too.

To demonstrate the differences, suppose now that you're deep diving into a codebase which depends on a Async monad. Your eyes light up and you go aha(!) that means async programming, I've done that before! The point is, you saw "Async", you know it means "make some task's outcome depend on a previous task", which is the behavior of bind for that particular monad. Without (1) the word "monad" is really unnecessary. Why not just refer to bind as some arbitrary async-API function? In summary, you don't need (1), (2), or (3) for this! Monad is just a word.

Okay, when do we need (1)? Let's say you've changed companies, and now you're plugged into another codebase and oh(!) there's that word "monad" again, but this time it's the "Future" monad. Another whole API to learn... but soon you realize that it's again the same old "make some task's outcome depend on a previous task". Except they just call it "Future", and instead of "bind", they say "flatMap" which is the same thing! And you bump into it again and again with different names -- Deferred, Aff, Task -- but in the end it's the same behavior and API. How upsetting that they don't call them all Async and be done with it! But if you have (1) you'll know they are just the same monad, given different names. That's (1): familiarity with the usage of a particular monad. Later on you might collect understanding of the Option/Maybe/Nullable monad, or the Result/Either/Error monad, or the List/Stream/Nondeterministic monad, so now names don't bother you because you know CONCEPTS, but all of this is still (1) if each monad is being treated as an independent API to grok.

That's where (2) comes in. Suppose now that you're deep diving into a codebase which depends on the "Anisotrope" monad. You've never heard of this before[0], but you know monads in general i.e. (2), so you know you can make functions whose output (an Ansiotrope object) depends on some property of a Ansiotrope object, and that all the details about this dependency can be found in the definition of bind for this particular monad. In other words you can use knowledge of (2) to quickly adapt to new monads without having to regard them as a completely new concept. It lets you answer questions like "what's this Probability monad supposed to do? what about this Forkable monad?" in a general way. Conversely, you can now start writing monads of your own by thinking about what bind could mean for your new "Transmogrifying" monad.

Is this useful? Imagine learning all OOP patterns knowing that every pattern is the same concept except for this one thing: bind. That means it's relatively trivial to learn these patterns and make new ones. Except they're not OOP patterns, it's monads, and no, you can't generalize OOP patterns the same way.

Anyways, this is also where "monad is a box"-esque metaphors fall short. It's rather descriptive of particular monads, but doesn't generalize well when you start reaching for many others: Reader(environment-passing), List(nondeterministic computations), Probability(probabilistic programming), or fun ones like parser monads, Amb(backtracking), Tardis(state-access-timeline-specifying)[1].

[0] I hope not, since I made it up. If you have (3) you're probably deriving a working definition already. Have fun! [1] http://hackage.haskell.org/package/tardis-0.4.1.0/docs/Contr...

Someone close to me taught me how to square knot, so my hoodie-tied-around-my-waist would stop slipping, as I was using a double overhand knot before.

I'd also like to add that learning knots is honestly more of a 5-minute commitment to learn than a 1-hour commitment, but it's definitely still a commitment.

I've been trying to get into Notion, but the biggest downside is that I can't edit the markdown source of my documents nor can I use my own editor to edit their documents. I'm not happy with Notion's editor -- for instance, unindenting item 2 out of 5 of a bulleted list will move it down to item 5 for some reason. I guess I could export documents to markdown, edit, and reupload, but at that point I'm just using Notion as cloud data storage.

edit: Didn't mean to criticize so much! I've found Notion is great for taking nice plain text notes on the go that I can instantly access on my other devices. In the past I achieved this with Syncthing, but Notion's syncing is much less finicky, and fast -- it takes less than a second to sync! Plus there's a share menu.

Could you (or someone else) elaborate on Coinbase going beyond KYC requirements?

Yes, yes yes! Encode invariants in your data, don't enforce invariants on your data. I particularly think this point needs to be stressed more, because practicably speaking, not every language has the typechecking faculties of Haskell:

> Sometimes, making an illegal state truly unrepresentable is just plain impractical given the tools Haskell provides, such as ensuring an integer is in a particular range. In that case, use an abstract newtype with a smart constructor to “fake” a parser from a validator.

For instance, few type systems will let you encode prime numbers as datatypes, so you'd have to do something in your language like

    newtype Prime = Integer
    mkPrime :: Integer -> Maybe Prime
    mkPrime | isPrime p = Just (Prime p)
            | otherwise = Nothing

which is parsing!

The author addresses some if not all of these points:

"It's awkward as hell to use and takes way to many brain-cells to achieve simple results."

> Even I find the above [react.js FRP] code hard to read, despite having written it! While this could be seen as a downside of the denotative approach, I see it as a mismatch between the denotative approach and textual syntax. There’s been interesting work visualizing streams, which I hope to build on. Currently, I’m in the mockup phase, but I hope to build a developer tool experience that will automatically generate a live visualization.

My understanding is that right now it certainly does require too much brain to do anything in FRP, but that isn't a downfall of FRP as a concept ("FRP kinda sucks") but rather that making FRP convenient is still today an open research question.

"That if you have some real world problem that involves state, that you want to model that using virtual state and not the high-order time-varying continuous functions that FRP uses."

> Denotative languages better convey the global structure of a program. We can fully understand an expression by its subexpressions, and their subexpressions, recursively. There are no spooky action-at-a-distance side-effects that can manipulate things from afar. We don’t have to read the entire codebase to ensure we understand a single piece; we must merely read its subexpressions, recursively. This allows us to quickly rule out what we do and do not need to read, saving us a lot of time in large codebases.

I don't disagree that using concrete, non-abstracted state is a simpler way to model state-related problems, but this isn't about modeling and solving state-related problems, it's about solving them in a way that's maintainable. It's easy to argue for simplicity now (i.e. when first approaching a problem) and we have many, many tools for using state for that, like ipython notebooks, or pen and paper. But let's point out that simplicity of these initial concrete-state-minded approaches tend to grow into entangled messes, messes that are arguably solved by encapsulation and patterns. Regardless of whether they do solve the problem, having to understand things like inheritance and all their related problems kind of defeats the purpose of using state to make the problem simpler to understand in the long run. Which is what FRP purports to solve. Except we don't have the pen and paper for FRP yet.

"The great irony is that nobody on the planet thinks of spreadsheets as time-varying continuous functions."

True. No one thinks that. The author doesn't think that. Probably not even the folks who made the neat stats-oriented spreadsheet[0] thinks that, and that's data as continuously varying as you can get.

All of this kind of props up the title which is that FRP is grossly misunderstood.

[0] https://news.ycombinator.com/item?id=18785371

Here is another example that is less of an isolated event:

https://www.nytimes.com/2019/07/02/opinion/surveillance-stat...

What I got from the article was that this is the wrong question to ask. Even if there are "right things" to be thinking, always feeding children the "right things" means they don't learn to deal with anything else.

> Of course, it’s not really the boredom itself that’s important; it’s what we do with it. When you reach your breaking point, boredom teaches you to respond constructively, to make something happen for yourself. But unless we are faced with a steady diet of stultifying boredom, we never learn how.

Ah, thanks for the link, that's super neat! I was looking for making changes that would persist across page loads or browser restarts, and this is exactly that. It's a shame that it's not a feature in Firefox's dev tools (not yet anyways)

What's your process of editing client side JS? Is there some method to capture scripts before they load so you can make your modifications?

I used to avoid sci-fi because of non-realism. Not my cup of tea to read insanely powerful tech used in really disappointing ways (e.g. Sophons from Three Body Problem writing timestamps), or for example societies in 2030 that are culturally unchanged from 2010.

Then I tried Blind Date with a Book, which is where the book gets wrapped in brown paper and labelled with some hints about the book, so you know what kind of book you're buying but not the title or author. I ended up unwrapping Chiang's Story of Your Life, the short story collection. Chiang ended up pulling me back into sci-fi. Every story had sci-fi elements that were thought-provoking without being unbelievable, not to mention phenomenal worldbuilding, which I am a real sucker for.

Even if you're not a sci-fi fan I'd recommend several of the stories in Story of Your Life -- Tower of Babylon really left an impression in my friend group, to say the least.

Cheers!

oh my, sure! [email removed]

https://lobste.rs/ is a very similar community to HN. The catch is that registration is invite-only.

By the way, if a lobsters user is reading this, I would love an invite :)

That's also fun up to some point. Whenever I optimized for fewest cycles in Codex it usually turned out to be "work with as many atoms per cycle as you possibly can", or something silly like building a solution on one side and mirroring the solution on the other side to get less cycles. The tedium of adding more and more tends to make least-cycle solutions less rewarding to craft, at least for me. (It's still fun though!)

If you open up a least-symbol solution for Codex you'll find a lot of interesting tricks used to reduce symbols. For example, grab-left-left-release-left-left can be accomplished with just grab-left-release-wait, if you sync it so the released atom is removed by another arm at exactly the right time. It's a nice feeling to successfully shave off even one more symbol using these hacks!

I love that. I've played most Zachtronics games as well as Robot Odyssey at 15, was hooked on Robot Odyssey for a week for the same reasons. The difficulty was a challenge rather than an impediment.

What really got me was that the games encouraged something like hand-optimizing the size of your program. The levels were open-ended and the solution could be anything, but each solution has a cost, for example, least number of gates used in Robot Odyssey. In SpaceChem, it's number of symbols. In The Codex of Alchemical Engineering, cost is measured in total number of instructions, which encouraged solutions involving many different parts moving perfectly in sync. Those solutions were really difficult but rewarding to craft. However, cost in Opus Magnum is measured in total cost of parts (not instructions) used. That's less interesting to optimize, since the 'best' solution is often one part doing all the work (easy to optimize for), which in my opinion makes it a little less fun to play. Similarly, I remember the last few levels of Robot Odyssey didn't have much space in the way of optimizing (there is just one Correct Solution) which was underwhelming.

I guess my point is that the games were fun not because I had so much freedom in how I can finish each level. Rather it was the difficulty of optimizing each solution that attracted me. And it's hard to find games like that outside Zachtronics.

As a future educator interested in how people think about code, I like these submissions! Whenever things like functional style or language syntax pop up on HN, they tend to create a big stink in comment threads, as people defend their (obviously different) tastes, perhaps by providing contrived code examples, or focusing on why Alice's code is "unreadable" to Bob, rather than understanding "that's just what works for Alice." Honest, unprovoked opinions like in this blog post (like "Hey, this works for me!") are a breath of fresh air.

I love this koan but I would replace 'strong' with 'pure'.

The fact that Float32 -> Float32 does not permit IO is due to purity. 'Strong' is kind of an ambiguous term here.

Either and try-catch are basically the same thing, except try-catch is, as you say, baked into the language, while Either is just data, a value you can manipulate however you want. Usually they will have the same functionality, but in some cases Either gives a few distinct advantages (off the top of my head):

- You can work a list of Either values (Lefts and Rights). For example applying a readFile operation on a list of file paths can give you a list of Lefts (errors) or Rights, which you can handle later. I can't imagine doing that cleanly with try-catch (i.e. without building up some intermediate list).

- Can return whatever data you want in the error, rather than just a String message (or, I guess you can if you write some custom CheckedException, but Either saves you from having to do that every time)

Playing with video game economies tells me that any tax on owning money/e-money would simply lead people to deal with an alternative, unpenalized store of wealth. I don't know how plausible that move is for the real world, since we can't all suddenly start pricing things in terms of potions and scrolls, but what's stopping this from making Bitcoin, or any coin as the people's de facto currency?