I never understood what was so special about Clojure's Transducers. Isn't it essentially just applying a transformation on the lambda applied to a fold?
Fundamentally, there are two ways of representing iteration pipelines: source driven, and drain driven. This almost always maps to the idea of _internal_ iteration and _external_ iteration, because the source is wrapped inside the transforms. Transducers are unusual in being source driven but also external iterators.
Most imperative languages choose one of two things, internal iteration that doesn't support composable flow control, and external iteration that does. This is why you see pause/resume style iteration in Python, Rust, Java, and even Javascript. If that's your experience, transducers are a pretty novel place in the trade-off space: you keep most of the composability, but you get to drive it from things like event sources.
But the gap is a bit smaller than it might appear. Rust's iterators are conceptually external iterators, but they actually do support internal iteration through `try_fold`, and even in languages that don't, you can 'just' convert external to internal iterators.
Then all you have to do to recover what transducers give you is pass the object to the source, let it run `try_fold` whenever it has data, and check for early termination via `size_hint`. There's one more trick for the rare case of iterators with buffering, but you don't have to change the Iterator interface for that, you just need to pass one bit of shared state to the objects on construction.
Not all Iterators are strictly valid to be source-driven, and while most do, not everything works nicely when iterated this way (eg. Skip could but doesn't handle this case correctly, because it's not required to), but I don't think transducers can actually do anything this setup can't. It's just an API difference after that point.
I wasn't saying you would have that experience, I was saying that the reason people act like transducers are unique is that transducers are an unconventional place on well worn ground.
Ultimately, yes, everything bottoms out, most special tricks seem less special the more you understand about them, because it's programming and Turing Equivalence is the bedrock the whole field rests on. But the average person learning about transducers is not going to spot how closely related it is to other things that already exist.
I'm happy to elaborate on any part of the terminology if you're curious, but tbh I mostly wrote it for myself because I thought the framing was novel and wanted it noted down somewhere.
Free Monads are a very nice (though not performant) way of creating an embedded domain specific language interpreter.
Once I was building a declarative components library in PHP, using the ideas I've learned from free monads. I'm sure you can't imagine what an attrocity I've built. It did the job, but I had to mentally check out and throw in a couple of goto's in my main evalution loop.
All that to say that elegance of expressivity is tied to the syntax and semantics of languages.
Free Monads are also built on a tower of mathematical structures that come with laws and invariants. I have yet to see such formalization for transducers.
For fish sauce definitely, assuming you also use the guts so you can get the enzymes. If you want to make with a protein source that doesn't have the enzymes present, like mushrooms, you can add them separately. Whole fish just fills the protein and protease slots with a single ingredient.
I've been wanting to make my own fish sauce for years at this point. I even found a huge crock to do it in. I've just never gotten it together to go to the fish market super early and source fish. What species do you use?
I mean you are kinda right but kinda wrong. To get a proof checker you take a typed lambda calculus and extend it with Pi, Sigma, and Indexed Inductive types while maintaining soundness.
Yes haskell's `bottom` breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.
i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.
We have over 60 shows now, rented a studio, and are in talks to security a site for our tower. I'm building out an online store but really need to focus on fundraising.
I actually find Gmail a better editor/grammar check then LLMs. It makes isolated simplifications/corrections that imo have minimal style impact and just focus on clarifying phrasing.
reply