Readit Newsdanidiaz commented on The Closing of the Bulgarian Frontier switchyardmag.com/issue-1... · Posted by u/rubin55
The memoir "Street without a Name: Childhood and Other Misadventures in Bulgaria" by Kapka Kassabova (2008) covers similar ground. https://www.goodreads.com/book/show/3808716-street-without-a...
danidiaz commented on New Wave Sci-Fi: 75 Best Novels of 1964–1983 hilobrow.com/new-wave-sci... · Posted by u/webmaven
I would also recommend the site "Science Fiction Ruminations": https://sciencefictionruminations.com/
Lots of thoughtful sf book reviews with a heavy (but not exclusive) focus on the New Wave.
danidiaz commented on RZK: Experimental proof assistant for synthetic ∞-categories github.com/rzk-lang/rzk... · Posted by u/adamnemecek
what is the substance of this complaint?
if i pull the API for django or react or ...anything else, how much should i be expected to understand without any prior exposure? how is "domain-specific gibberish" any different? you make up words to represent groups of other words in order to capture concepts. it's literally just how language works.
let me translate for you:
proof assistant: program that checks your work (writing a proof) and helps you find new proofs.
synthetic: math where the axioms "represent" the objects instead of the other way around (they're "synthesized" from the objects)
1-category: a collection with objects and functions between them
2-category: a collection with objects, functions between them, and functions between those functions (called homotopies)
k-category: you get the idea
∞-category: the limit as k -> ∞
second-order abstract syntax which is great for lambda extraction: syntax specifically suited for this kind of stuff
and you know what? even though i am not a category theorist i was able to figure this out. you know how? i quickly skimmed the "docs" https://ncatlab.org/nlab/show/synthetic+%28infinity%2C1%29-c...
I'm not a mathematician, but I feel the "syntethic"/"analythic" distinction in mathematics is an interesting and useful concept.
"In modern mathematics, an analytic theory is one whose basic objects are defined in some other theory, whereas a synthetic theory is one whose basic objects are undefined terms given meaning by rules and axioms"—Michael Shulman
In programming terms, I guess "synthetic" mathematics feels a bit like programming to an abstract interface.
https://ncatlab.org/nlab/show/synthetic+mathematics
In the first part of this video Cédric Villani gives (in French) a nice explanation of the distinction: https://youtu.be/xzVk56EKBUI?t=258
Edit: an English explanation, also by Villani: https://www.youtube.com/watch?v=AIrLXbwyYXQ
danidiaz commented on Temporal quality degradation in AI models nannyml.com/blog/91-of-ml... · Posted by u/santiviquez
https://qntm.org/mmacevedo
> However, even for these tasks, its performance has dropped measurably since the early 2060s and is now considered subpar compared to more recent uploads. This is primarily attributed to MMAcevedo's lack of understanding of the technological, social and political changes which have occurred in modern society since its creation in 2031. This phenomenon has also been observed in other uploads created after MMAcevedo, and is now referred to as context drift.
danidiaz commented on Pedagogical Downsides of Haskell ciobaca.substack.com/p/pe... · Posted by u/scscsc
Brilliant write up.
> There is also a school of thought that you should start Haskell by teaching the IO monad first, but I am not convinced: in my experience, if someone gets exposed to IO early on, they will contaminate all their functions with IO. They will essentially end up writing Java in Haskell.
I don't think this is such a bad starting place. Crawling before walking. Purifying an (unnecessarily-) IO function into an ordinary function is a good exercise.
Trying to enforce non-IO from the start would be like enforcing 'no new keyword & factories only' in another language.
> Purifying an (unnecessarily-) IO function into an ordinary function is a good exercise.
Agree! And I would add that you can "purify" a monadic function without having to rewrite it in non-monadic style. You can make it polymorphic over all monads and relegate the "impurity" to monadic functions that you pass as arguments/dependencies. A trivial example:
twice :: IO ()
twice = do
putStrLn "foo"
putStrLn "foo"
twice' :: forall m. m () -> m ()
twice' action = do
action
action
Haskell lets you express the idea of "program logic that only has effects through its dependencies" by being polymorphic over all monads.
From this article about a different emperor: https://www.lrb.co.uk/the-paper/v41/n04/christopher-kelly/a-...